aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-14 22:55:31 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-14 22:55:31 +0200
commit6d5b1d25c162f105a2ba1f5019574943d4a3c0e0 (patch)
treed2a333650e454649501f4104690a026495a31a0a
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.tar.gz
VIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.tar.zst
VIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.zip
fixes for the measurement
Diffstat
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend114
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend73
6 files changed, 115 insertions, 93 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
index 3f0ba03f..ca272381 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -87,6 +87,13 @@ class SolverLoader {
87 ] 87 ]
88 } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} 88 } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')}
89 } 89 }
90 if(config.containsKey("numeric-solver-at-end")) {
91 val stringValue = config.get("numeric-solver-at-end")
92 if(stringValue.equals("true")) {
93 println("numeric-solver-at-end")
94 c.runIntermediateNumericalConsistencyChecks= false
95 }
96 }
90 ] 97 ]
91 } else { 98 } else {
92 throw new UnsupportedOperationException('''Unknown solver: «solver»''') 99 throw new UnsupportedOperationException('''Unknown solver: «solver»''')
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index d92f2e30..677170b8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -215,42 +215,42 @@ class PatternGenerator {
215 find mayExist(problem,interpretation,a); 215 find mayExist(problem,interpretation,a);
216 find mayExist(problem,interpretation,b); 216 find mayExist(problem,interpretation,b);
217 a == b; 217 a == b;
218 } or { 218««« } or {
219 find mayExist(problem,interpretation,a); 219««« find mayExist(problem,interpretation,a);
220 find mayExist(problem,interpretation,b); 220««« find mayExist(problem,interpretation,b);
221 IntegerElement(a); 221««« IntegerElement(a);
222 IntegerElement(b); 222««« IntegerElement(b);
223 PrimitiveElement.valueSet(a,false); 223««« PrimitiveElement.valueSet(a,false);
224 } or { 224««« } or {
225 find mayExist(problem,interpretation,a); 225««« find mayExist(problem,interpretation,a);
226 find mayExist(problem,interpretation,b); 226««« find mayExist(problem,interpretation,b);
227 IntegerElement(a); 227««« IntegerElement(a);
228 IntegerElement(b); 228««« IntegerElement(b);
229 PrimitiveElement.valueSet(b,false); 229««« PrimitiveElement.valueSet(b,false);
230 } or { 230««« } or {
231 find mayExist(problem,interpretation,a); 231««« find mayExist(problem,interpretation,a);
232 find mayExist(problem,interpretation,b); 232««« find mayExist(problem,interpretation,b);
233 RealElement(a); 233««« RealElement(a);
234 RealElement(b); 234««« RealElement(b);
235 PrimitiveElement.valueSet(a,false); 235««« PrimitiveElement.valueSet(a,false);
236 } or { 236««« } or {
237 find mayExist(problem,interpretation,a); 237««« find mayExist(problem,interpretation,a);
238 find mayExist(problem,interpretation,b); 238««« find mayExist(problem,interpretation,b);
239 RealElement(a); 239««« RealElement(a);
240 RealElement(b); 240««« RealElement(b);
241 PrimitiveElement.valueSet(b,false); 241««« PrimitiveElement.valueSet(b,false);
242 } or { 242««« } or {
243 find mayExist(problem,interpretation,a); 243««« find mayExist(problem,interpretation,a);
244 find mayExist(problem,interpretation,b); 244««« find mayExist(problem,interpretation,b);
245 StringElement(a); 245««« StringElement(a);
246 StringElement(b); 246««« StringElement(b);
247 PrimitiveElement.valueSet(a,false); 247««« PrimitiveElement.valueSet(a,false);
248 } or { 248««« } or {
249 find mayExist(problem,interpretation,a); 249««« find mayExist(problem,interpretation,a);
250 find mayExist(problem,interpretation,b); 250««« find mayExist(problem,interpretation,b);
251 StringElement(a); 251««« StringElement(a);
252 StringElement(b); 252««« StringElement(b);
253 PrimitiveElement.valueSet(b,false); 253««« PrimitiveElement.valueSet(b,false);
254 } 254 }
255 255
256 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 256 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
@@ -258,27 +258,27 @@ class PatternGenerator {
258 find mustExist(problem,interpretation,a); 258 find mustExist(problem,interpretation,a);
259 find mustExist(problem,interpretation,b); 259 find mustExist(problem,interpretation,b);
260 a == b; 260 a == b;
261 } or { 261««« } or {
262 find mustExist(problem,interpretation,a); 262««« find mustExist(problem,interpretation,a);
263 find mustExist(problem,interpretation,b); 263««« find mustExist(problem,interpretation,b);
264 PrimitiveElement.valueSet(a,true); 264««« PrimitiveElement.valueSet(a,true);
265 PrimitiveElement.valueSet(b,true); 265««« PrimitiveElement.valueSet(b,true);
266 IntegerElement.value(a,value); 266««« IntegerElement.value(a,value);
267 IntegerElement.value(b,value); 267««« IntegerElement.value(b,value);
268 } or { 268««« } or {
269 find mustExist(problem,interpretation,a); 269««« find mustExist(problem,interpretation,a);
270 find mustExist(problem,interpretation,b); 270««« find mustExist(problem,interpretation,b);
271 PrimitiveElement.valueSet(a,true); 271««« PrimitiveElement.valueSet(a,true);
272 PrimitiveElement.valueSet(b,true); 272««« PrimitiveElement.valueSet(b,true);
273 RealElement.value(a,value); 273««« RealElement.value(a,value);
274 RealElement.value(b,value); 274««« RealElement.value(b,value);
275 } or { 275««« } or {
276 find mustExist(problem,interpretation,a); 276««« find mustExist(problem,interpretation,a);
277 find mustExist(problem,interpretation,b); 277««« find mustExist(problem,interpretation,b);
278 PrimitiveElement.valueSet(a,true); 278««« PrimitiveElement.valueSet(a,true);
279 PrimitiveElement.valueSet(b,true); 279««« PrimitiveElement.valueSet(b,true);
280 StringElement.value(a,value); 280««« StringElement.value(a,value);
281 StringElement.value(b,value); 281««« StringElement.value(b,value);
282 } 282 }
283 283
284 ////////// 284 //////////
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{
113 113
114 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) 114 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method)
115 viatraConfig.progressMonitor.workedForwardTransformation 115 viatraConfig.progressMonitor.workedForwardTransformation
116 val transformationFinished = System.nanoTime
117 val transformationTime = transformationFinished - transformationStartTime
116 118
117 val transformationTime = System.nanoTime - transformationStartTime
118 val solverStartTime = System.nanoTime 119 val solverStartTime = System.nanoTime
119 120
120 var boolean stoppedByTimeout 121 var boolean stoppedByTimeout
@@ -141,6 +142,9 @@ class ViatraReasoner extends LogicReasoner{
141 ] 142 ]
142 } 143 }
143 it.entries += createIntStatisticEntry => [ 144 it.entries += createIntStatisticEntry => [
145 it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int
146 ]
147 it.entries += createIntStatisticEntry => [
144 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int 148 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int
145 ] 149 ]
146 it.entries += createIntStatisticEntry => [ 150 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{
45 * Configuration for cutting search space. 45 * Configuration for cutting search space.
46 */ 46 */
47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint 47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
48
49 public var runIntermediateNumericalConsistencyChecks = true
48} 50}
49 51
50public class DiversityDescriptor { 52public 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 {
91 private int numberOfPrintedModel = 0; 91 private int numberOfPrintedModel = 0;
92 private int numberOfSolverCalls = 0; 92 private int numberOfSolverCalls = 0;
93 93
94 public long explorationStarted = 0;
94 95
95 public BestFirstStrategyForModelGeneration( 96 public BestFirstStrategyForModelGeneration(
96 ReasonerWorkspace workspace, 97 ReasonerWorkspace workspace,
@@ -119,7 +120,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
119 120
120// ViatraQueryEngine engine = context.getQueryEngine(); 121// ViatraQueryEngine engine = context.getQueryEngine();
121// // TODO: visualisation 122// // TODO: visualisation
122// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); 123// LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
123// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { 124// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
124// //System.out.println(p.getSimpleName()); 125// //System.out.println(p.getSimpleName());
125// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); 126// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
@@ -137,13 +138,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
137 } 138 }
138 }; 139 };
139 140
140 this.numericSolver = new NumericSolver(context, method, false); 141 this.numericSolver = new NumericSolver(context, method, false,this.configuration.runIntermediateNumericalConsistencyChecks);
141 142
142 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); 143 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
143 } 144 }
144 145
145 @Override 146 @Override
146 public void explore() { 147 public void explore() {
148 this.explorationStarted=System.nanoTime();
147 if (!context.checkGlobalConstraints()) { 149 if (!context.checkGlobalConstraints()) {
148 logger.info("Global contraint is not satisifed in the first state. Terminate."); 150 logger.info("Global contraint is not satisifed in the first state. Terminate.");
149 return; 151 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 {
26 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 26 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
27 NumericTranslator t = new NumericTranslator 27 NumericTranslator t = new NumericTranslator
28 28
29 val boolean intermediateConsistencyCheck
29 val boolean caching; 30 val boolean caching;
30 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap 31 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
31 32
@@ -34,7 +35,7 @@ class NumericSolver {
34 var int numberOfSolverCalls = 0 35 var int numberOfSolverCalls = 0
35 var int numberOfCachedSolverCalls = 0 36 var int numberOfCachedSolverCalls = 0
36 37
37 new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { 38 new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {
38 this.threadContext = threadContext 39 this.threadContext = threadContext
39 val engine = threadContext.queryEngine 40 val engine = threadContext.queryEngine
40 for(entry : method.mustUnitPropagationPreconditions.entrySet) { 41 for(entry : method.mustUnitPropagationPreconditions.entrySet) {
@@ -49,6 +50,8 @@ class NumericSolver {
49 val matcher = querySpec.getMatcher(engine); 50 val matcher = querySpec.getMatcher(engine);
50 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) 51 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
51 } 52 }
53 this.intermediateConsistencyCheck = true
54 println()
52 this.caching = caching 55 this.caching = caching
53 } 56 }
54 57
@@ -70,44 +73,48 @@ class NumericSolver {
70 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { 73 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
71 val start = System.nanoTime 74 val start = System.nanoTime
72 var boolean finalResult 75 var boolean finalResult
73 if(matches.empty){ 76 if(intermediateConsistencyCheck) {
74 finalResult=true 77 if(matches.empty){
75 } else {
76 val propagatedConstraints = new HashMap
77 for(entry : matches.entrySet) {
78 val constraint = entry.key
79 //println(constraint)
80 val allMatches = entry.value.allMatches.map[it.toArray]
81 //println(allMatches.toList)
82 propagatedConstraints.put(constraint,allMatches)
83 }
84 if(propagatedConstraints.values.forall[empty]) {
85 finalResult=true 78 finalResult=true
86 } else { 79 } else {
87 if(caching) { 80 val propagatedConstraints = new HashMap
88 val code = getCode(propagatedConstraints) 81 for(entry : matches.entrySet) {
89 val cachedResult = satisfiabilityCache.get(code) 82 val constraint = entry.key
90 if(cachedResult === null) { 83 //println(constraint)
91 // println('''new problem, call solver''') 84 val allMatches = entry.value.allMatches.map[it.toArray]
92 // for(entry : code.entrySet) { 85 //println(allMatches.toList)
93 // println('''«entry.key» -> «entry.value»''') 86 propagatedConstraints.put(constraint,allMatches)
94 // } 87 }
95 //println(code.hashCode) 88 if(propagatedConstraints.values.forall[empty]) {
96 this.numberOfSolverCalls++ 89 finalResult=true
97 val res = t.delegateIsSatisfiable(propagatedConstraints) 90 } else {
98 satisfiabilityCache.put(code,res) 91 if(caching) {
99 finalResult=res 92 val code = getCode(propagatedConstraints)
93 val cachedResult = satisfiabilityCache.get(code)
94 if(cachedResult === null) {
95 // println('''new problem, call solver''')
96 // for(entry : code.entrySet) {
97 // println('''«entry.key» -> «entry.value»''')
98 // }
99 //println(code.hashCode)
100 this.numberOfSolverCalls++
101 val res = t.delegateIsSatisfiable(propagatedConstraints)
102 satisfiabilityCache.put(code,res)
103 finalResult=res
104 } else {
105 //println('''similar problem, answer from cache''')
106 finalResult=cachedResult
107 this.numberOfCachedSolverCalls++
108 }
100 } else { 109 } else {
101 //println('''similar problem, answer from cache''') 110 finalResult= t.delegateIsSatisfiable(propagatedConstraints)
102 finalResult=cachedResult 111 this.numberOfSolverCalls++
103 this.numberOfCachedSolverCalls++
104 } 112 }
105 } else {
106 finalResult= t.delegateIsSatisfiable(propagatedConstraints)
107 this.numberOfSolverCalls++
108 } 113 }
109 } 114 }
110 } 115 } else {
116 finalResult = true
117 }
111 this.runtime+=System.nanoTime-start 118 this.runtime+=System.nanoTime-start
112 return finalResult 119 return finalResult
113 } 120 }
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-03 07:39:00 +0000