fixes for the measurement

4 files changed, 51 insertions, 36 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 293df935..1fe65afe 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
@@ -113,8 +113,9 @@ class ViatraReasoner extends LogicReasoner{
                 

                 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method)

                 viatraConfig.progressMonitor.workedForwardTransformation

+                val transformationFinished = System.nanoTime 

+                val transformationTime = transformationFinished - transformationStartTime

                 

-                val transformationTime = System.nanoTime - transformationStartTime

                 val solverStartTime = System.nanoTime

                 

                 var boolean stoppedByTimeout

@@ -141,6 +142,9 @@ class ViatraReasoner extends LogicReasoner{
                                 ]

                         }

                         it.entries += createIntStatisticEntry => [

+                                it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

                                 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index c4d7e231..24578e7b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -45,6 +45,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
          * Configuration for cutting search space.

          */

          public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

+         

+         public var runIntermediateNumericalConsistencyChecks = true

 }

 

 public class DiversityDescriptor {

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 45dffe7c..75ce7f10 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
@@ -91,6 +91,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private int numberOfPrintedModel = 0;

         private int numberOfSolverCalls = 0;

         

+        public long explorationStarted = 0;

 

         public BestFirstStrategyForModelGeneration(

                         ReasonerWorkspace workspace,

@@ -119,7 +120,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 

 //              ViatraQueryEngine engine = context.getQueryEngine();

 //              // TODO: visualisation

-//              matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();

+//              LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();

 //              for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {

 //                      //System.out.println(p.getSimpleName());

 //                      ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);

@@ -137,13 +138,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                         }

                 };

                 

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

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

 

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

         }

 

         @Override

         public void explore() {

+                this.explorationStarted=System.nanoTime();

                 if (!context.checkGlobalConstraints()) {

                         logger.info("Global contraint is not satisifed in the first state. Terminate.");

                         return;

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 0fb5d702..a012f51b 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
@@ -26,6 +26,7 @@ class NumericSolver {
         val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         NumericTranslator t = new NumericTranslator

         

+        val boolean intermediateConsistencyCheck

         val boolean caching;

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

         

@@ -34,7 +35,7 @@ class NumericSolver {
         var int numberOfSolverCalls = 0

         var int numberOfCachedSolverCalls = 0

         

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

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

                 this.threadContext = threadContext

                 val engine = threadContext.queryEngine

                 for(entry : method.mustUnitPropagationPreconditions.entrySet) {

@@ -49,6 +50,8 @@ class NumericSolver {
                         val matcher = querySpec.getMatcher(engine);

                         constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)

                 }

+                this.intermediateConsistencyCheck = true

+                println()

                 this.caching = caching

         }

         

@@ -70,44 +73,48 @@ class NumericSolver {
         private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {

                 val start = System.nanoTime

                 var boolean finalResult 

-                if(matches.empty){

-                        finalResult=true

-                } else {

-                        val propagatedConstraints = new HashMap

-                        for(entry : matches.entrySet) {

-                                val constraint = entry.key

-                                //println(constraint)

-                                val allMatches = entry.value.allMatches.map[it.toArray]

-                                //println(allMatches.toList)

-                                propagatedConstraints.put(constraint,allMatches)

-                        }

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

+                if(intermediateConsistencyCheck) {

+                        if(matches.empty){

                                 finalResult=true

                         } else {

-                                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

+                                val propagatedConstraints = new HashMap

+                                for(entry : matches.entrySet) {

+                                        val constraint = entry.key

+                                        //println(constraint)

+                                        val allMatches = entry.value.allMatches.map[it.toArray]

+                                        //println(allMatches.toList)

+                                        propagatedConstraints.put(constraint,allMatches)

+                                }

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

+                                        finalResult=true

+                                } else {

+                                        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 {

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

-                                                finalResult=cachedResult

-                                                this.numberOfCachedSolverCalls++

+                                                finalResult= t.delegateIsSatisfiable(propagatedConstraints)

+                                                this.numberOfSolverCalls++

                                         }

-                                } else {

-                                        finalResult= t.delegateIsSatisfiable(propagatedConstraints)

-                                        this.numberOfSolverCalls++

                                 }

                         }

-                }

+                } else {

+                        finalResult = true

+                }               

                 this.runtime+=System.nanoTime-start

                 return finalResult

         }