measurement time statistics + activation selection strategies

7 files changed, 176 insertions, 18 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index cb73f4e8..bafe78f6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -155,6 +155,21 @@ class ViatraReasoner extends LogicReasoner{
                         it.entries += createIntStatisticEntry => [

                                 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int

                         ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "NumericalSolverTime" it.value = (strategy.numericSolver.runtime/1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls

+                        ]

                         if(strategy.solutionStoreWithDiversityDescriptor.isActive) {

                                 it.entries += createIntStatisticEntry => [

                                         it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend
new file mode 100644
index 00000000..65f9814c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend
@@ -0,0 +1,24 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

+

+import java.util.ArrayList

+import java.util.Collection

+import java.util.Random

+

+abstract class ActivationSelector {

+        long runtime = 0

+        protected val Random r

+        new(Random r) {

+                this.r = r

+        }

+        

+        def randomizeActivationIDs(Collection<Object> activationIDs) {

+                val startTime = System.nanoTime

+                val res = internalRandomizationOfActivationIDs(activationIDs)

+                runtime+= System.nanoTime-startTime

+                return res

+        }

+        def protected ArrayList<Object> internalRandomizationOfActivationIDs(Collection<Object> activationIDs);

+        def getRuntime(){

+                return runtime

+        }

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend
new file mode 100644
index 00000000..2df9957b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend
@@ -0,0 +1,51 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

+

+import java.util.Collection

+import java.util.HashMap

+import java.util.Map

+import java.util.List

+import java.util.Random

+import java.util.ArrayList

+import java.util.LinkedList

+import java.util.Collections

+

+class BalancedActivationSelector extends ActivationSelector{

+        val Random r = new Random

+        

+        new(Random r) {

+                super(r)

+        }

+        

+        override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {

+                val Map<String,List<Object>> urns = new HashMap

+                val res = new ArrayList(activationIDs.size)

+                for(activationID : activationIDs) {

+                        val pair = activationID as Pair<String,? extends Object>

+                        val name = pair.key

+                        val selectedUrn = urns.get(name)

+                        if(selectedUrn!==null) {

+                                selectedUrn.add(activationID)

+                        } else {

+                                val collection = new LinkedList

+                                collection.add(activationID)

+                                urns.put(name,collection)

+                        }

+                }

+                

+                for(list:urns.values) {

+                        Collections.shuffle(list,r)

+                }

+                

+                while(!urns.empty) {

+                        val randomEntry = urns.entrySet.get(r.nextInt(urns.size))

+                        val list = randomEntry.value

+                        val removedLast = list.remove(list.size-1)

+                        res.add(removedLast)

+                        if(list.empty) {

+                                urns.remove(randomEntry.key)

+                        }

+                }

+                return res

+        }

+        

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 1cd61e9a..18fe94e4 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -84,13 +84,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private ModelResult modelResultByInternalSolver = null;

         private Random random = new Random();

         //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

-        

+        public ActivationSelector activationSelector = new EvenActivationSelector(random);

+        public NumericSolver numericSolver = null;

         // Statistics

         private int numberOfStatecoderFail = 0;

         private int numberOfPrintedModel = 0;

         private int numberOfSolverCalls = 0;

         

-        private NumericSolver numericSolver = null;

 

         public BestFirstStrategyForModelGeneration(

                         ReasonerWorkspace workspace,

@@ -137,7 +137,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                         }

                 };

                 

-                this.numericSolver = new NumericSolver(context, method);

+                this.numericSolver = new NumericSolver(context, method, false);

 

                 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);

         }

@@ -273,8 +273,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private List<Object> selectActivation() {

                 List<Object> activationIds;

                 try {

-                        activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());

-                        Collections.shuffle(activationIds);

+                        activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());

                 } catch (NullPointerException e) {

                         numberOfStatecoderFail++;

                         activationIds = Collections.emptyList();

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend
new file mode 100644
index 00000000..82a5f32d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend
@@ -0,0 +1,20 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

+

+import java.util.Random

+import java.util.Collection

+import java.util.Collections

+import java.util.ArrayList

+

+class EvenActivationSelector extends ActivationSelector {

+        

+        new(Random r) {

+                super(r)

+        }

+        

+        override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {

+                val toShuffle = new ArrayList<Object>(activationIDs);

+                Collections.shuffle(toShuffle);

+                return toShuffle

+        }

+        

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
index 2489c751..a75ddf76 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -50,20 +50,22 @@ class ModelGenerationCompositeObjective implements IObjective{
         

         override getComparator() { Comparators.LOWER_IS_BETTER }

         override getFitness(ThreadContext context) {

-                var sum = 0.0

+                

                 val scopeFitnes = scopeObjective.getFitness(context)

                 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]

                 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)

                 

-                sum+=scopeFitnes

+                

                 var multiplicity = 0.0

                 for(multiplicityObjective : unfinishedMultiplicityObjectives) {

-                        multiplicity+=multiplicityObjective.getFitness(context)//*0.5

+                        multiplicity+=multiplicityObjective.getFitness(context)

                 }

-                sum+=multiplicity

+                var sum = 0.0

+                sum += scopeFitnes

+                sum +=Math.sqrt(multiplicity *0.1)

                 sum += unfinishedWFsFitness//*0.5

                 

-                //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')

+                println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')

                 

                 return sum

         }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index e1745854..71793aa6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -19,13 +19,23 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement

 import java.util.List

 import java.math.BigDecimal

+import java.util.LinkedHashSet

+import java.util.LinkedHashMap

 

 class NumericSolver {

         val ThreadContext threadContext;

         val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         NumericTranslator t = new NumericTranslator

         

-        new(ThreadContext threadContext, ModelGenerationMethod method) {

+        val boolean caching;

+        Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap

+        

+        var long runtime = 0

+        var long cachingTime = 0 

+        var int numberOfSolverCalls = 0

+        var int numberOfCachedSolverCalls = 0

+        

+        new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) {

                 this.threadContext = threadContext

                 val engine = threadContext.queryEngine

                 for(entry : method.unitPropagationPreconditions.entrySet) {

@@ -34,11 +44,20 @@ class NumericSolver {
                         val matcher = querySpec.getMatcher(engine);

                         constraint2UnitPropagationPrecondition.put(constraint,matcher)

                 }

+                this.caching = caching

         }

         

+        def getRuntime(){runtime}

+        def getCachingTime(){cachingTime}

+        def getNumberOfSolverCalls(){numberOfSolverCalls}

+        def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}

+        

         def boolean isSatisfiable() {

-                if(constraint2UnitPropagationPrecondition.empty) return true

-                else {

+                val start = System.nanoTime

+                var boolean finalResult 

+                if(constraint2UnitPropagationPrecondition.empty){

+                        finalResult=true

+                } else {

                         val propagatedConstraints = new HashMap

                         for(entry : constraint2UnitPropagationPrecondition.entrySet) {

                                 val constraint = entry.key

@@ -47,15 +66,43 @@ class NumericSolver {
                                 //println(allMatches.toList)

                                 propagatedConstraints.put(constraint,allMatches)

                         }

-                        

                         if(propagatedConstraints.values.forall[empty]) {

-                                return true

+                                finalResult=true

                         } else {

-                                val res = t.delegateIsSatisfiable(propagatedConstraints)

-                                //println(res)

-                                return res

+                                if(caching) {

+                                        val code = getCode(propagatedConstraints)

+                                        val cachedResult = satisfiabilityCache.get(code)

+                                        if(cachedResult === null) {

+        //                                      println('''new problem, call solver''')

+        //                                      for(entry : code.entrySet) {

+        //                                              println('''«entry.key» -> «entry.value»''')

+        //                                      }

+                                                //println(code.hashCode)

+                                                this.numberOfSolverCalls++

+                                                val res = t.delegateIsSatisfiable(propagatedConstraints)

+                                                satisfiabilityCache.put(code,res)

+                                                finalResult=res

+                                        } else {

+                                                //println('''similar problem, answer from cache''')

+                                                finalResult=cachedResult

+                                                this.numberOfCachedSolverCalls++

+                                        }

+                                } else {

+                                        finalResult= t.delegateIsSatisfiable(propagatedConstraints)

+                                        this.numberOfSolverCalls++

+                                }

                         }

                 }

+                this.runtime+=System.nanoTime-start

+                return finalResult

+        }

+        

+        def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {

+                val start = System.nanoTime

+                val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList

+                val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]])

+                this.cachingTime += System.nanoTime-start

+                return res

         }

         

         def fillSolutionCopy(Map<EObject, EObject> trace) {