From 6d5b1d25c162f105a2ba1f5019574943d4a3c0e0 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Thu, 14 May 2020 22:55:31 +0200 Subject: fixes for the measurement --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 6 +- .../reasoner/ViatraReasonerConfiguration.xtend | 2 + .../dse/BestFirstStrategyForModelGeneration.java | 6 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 73 ++++++++++++---------- 4 files changed, 51 insertions(+), 36 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme') 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 @@ -140,6 +141,9 @@ class ViatraReasoner extends LogicReasoner{ it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int ] } + 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 ] 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>(); +// LinkedList> matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { // //System.out.println(p.getSimpleName()); // ViatraQueryMatcher 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(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> NumericTranslator t = new NumericTranslator + val boolean intermediateConsistencyCheck val boolean caching; Map>>,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> 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 } -- cgit v1.2.3-54-g00ecf