aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-14 10:34:21 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-14 10:34:21 +0100
commit803429243a248aef91bc8696c0da5924278e1cb6 (patch)
tree203e8eda42f6b96a45aca2ab5d623b2793b7b2e8
parentAdd strategy flag + implement alost working crossingScenarioStrategy (diff)
downloadVIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.tar.gz
VIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.tar.zst
VIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.zip
finished first impl that works sometimes (issue w/ SAT in Dreal rerun)
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend54
3 files changed, 48 insertions, 14 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index 36ea64aa..d7e0b20c 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -8,6 +8,7 @@ import java.io.IOException;
8import java.io.InputStream; 8import java.io.InputStream;
9import java.io.InputStreamReader; 9import java.io.InputStreamReader;
10import java.io.PrintWriter; 10import java.io.PrintWriter;
11import java.text.DecimalFormat;
11import java.util.ArrayList; 12import java.util.ArrayList;
12import java.util.Arrays; 13import java.util.Arrays;
13import java.util.HashMap; 14import java.util.HashMap;
@@ -504,7 +505,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
504 if (obj instanceof IntegerElement) { 505 if (obj instanceof IntegerElement) {
505 sol.put(obj, Integer.parseInt(value)); 506 sol.put(obj, Integer.parseInt(value));
506 } else { 507 } else {
507 sol.put(obj, Double.parseDouble(value)); 508 double fullVal = Double.parseDouble(value);
509 double trimmed = Math.round(fullVal * 1000.0) / 1000.0;
510 sol.put(obj, trimmed);
508 } 511 }
509 } 512 }
510 } else { 513 } else {
@@ -515,6 +518,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
515 } 518 }
516 else { 519 else {
517 System.out.println("Unsatisfiable numerical problem (trying to get solution...)"); 520 System.out.println("Unsatisfiable numerical problem (trying to get solution...)");
521 //null means no soln found
522 return null;
518 } 523 }
519 return sol; 524 return sol;
520 } 525 }
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 ed04ae4a..5ad78506 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
@@ -156,6 +156,7 @@ class ViatraReasoner extends LogicReasoner {
156 val transformationTime = transformationFinished - transformationStartTime 156 val transformationTime = transformationFinished - transformationStartTime
157 val solverStartTime = System.nanoTime 157 val solverStartTime = System.nanoTime
158 158
159 println(">>begin exploration")
159 var boolean stoppedByTimeout 160 var boolean stoppedByTimeout
160 try { 161 try {
161 stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); 162 stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
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 b8fcb6a0..bb2c7dbf 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
@@ -148,8 +148,14 @@ class NumericSolver {
148 val propagatedConstraints = new HashMap 148 val propagatedConstraints = new HashMap
149 //Filter constraints if there are phase-related restricutions 149 //Filter constraints if there are phase-related restricutions
150 //null whitelist means accept everything 150 //null whitelist means accept everything
151 val whitelist = getConstraintWhitelist(phase) 151
152 println("<<<<START-STEP>>>> (" + phase + ")") 152 println("<<<<START-STEP>>>> (" + phase + ")")
153 if (phase == -2) {
154 println("Skipping numeric check")
155 //TODO Big assumption
156 return true
157 }
158 val whitelist = getConstraintWhitelist(phase)
153 for(entry : matches.entrySet) { 159 for(entry : matches.entrySet) {
154 if (entry.value !== null){ 160 if (entry.value !== null){
155 val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName 161 val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName
@@ -182,8 +188,11 @@ class NumericSolver {
182 //TODO ASSUME Always True 188 //TODO ASSUME Always True
183 //GET LIST OF VARS TO FILL 189 //GET LIST OF VARS TO FILL
184 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) 190 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
185 fillWithPartialSolutionsDirectly(dataObjects, fillMap) 191 if (fillMap === null) res = false
186 res = true 192 else {
193 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
194 res = true
195 }
187 } else { 196 } else {
188 res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) 197 res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
189 } 198 }
@@ -201,8 +210,11 @@ class NumericSolver {
201 //TODO ASSUME Always True 210 //TODO ASSUME Always True
202 //GET LIST OF VARS TO FILL 211 //GET LIST OF VARS TO FILL
203 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) 212 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
204 fillWithPartialSolutionsDirectly(dataObjects, fillMap) 213 if (fillMap === null) finalResult = false
205 finalResult = true 214 else {
215 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
216 finalResult = true
217 }
206 } else { 218 } else {
207 finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) 219 finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
208 } 220 }
@@ -211,6 +223,7 @@ class NumericSolver {
211 } 223 }
212 } 224 }
213 this.runtime+=System.nanoTime-start 225 this.runtime+=System.nanoTime-start
226 if (phase == 2) finalResult = isSatisfiable(matches, 3)
214 return finalResult 227 return finalResult
215 } 228 }
216 229
@@ -230,27 +243,43 @@ class NumericSolver {
230 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors 243 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
231 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; 244 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
232 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); 245 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
233 var boolean foundActorWithDefinedPos = false; 246 var boolean foundBlockedBy = false;
247
248 var int numActors;
249 var int numPlacedOn;
250 var int numPlacements = 0;
251
234 for (PartialRelationInterpretation rel : relations) { 252 for (PartialRelationInterpretation rel : relations) {
253 if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) {
254 numActors = rel.relationlinks.size
255 }
256
257 if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) {
258 numPlacedOn = rel.relationlinks.size
259 }
260
235 if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { 261 if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) {
236 for (RelationLink link : rel.getRelationlinks()) { 262 for (RelationLink link : rel.getRelationlinks()) {
237 val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; 263 val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement;
238 if (param2.isValueSet()) { 264 if (param2.isValueSet()) {
239 foundActorWithDefinedPos = true; 265 numPlacements++
240 } 266 }
241 } 267 }
242 } 268 }
243 269
244 if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { 270 if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) {
245 if (!rel.getRelationlinks().isEmpty()) { 271 if (!rel.getRelationlinks().isEmpty()) {
246 return 3; 272 foundBlockedBy = true
247 } 273 }
248 } 274 }
249 } 275 }
276 val boolean unplacedActorExists = numPlacements < numActors
250 //it means that there is no blockedBy 277 //it means that there is no blockedBy
251 //so we are at most at phase 2 278 //so we are at most at phase 2
252 if (foundActorWithDefinedPos) return 2; 279 if (numPlacedOn == 1 && numPlacements == 0) return 1
253 return 1; 280 if (foundBlockedBy && unplacedActorExists) return 2
281 if (numPlacements == numActors) return 3;
282 return -2;
254 } 283 }
255 return -1; 284 return -1;
256 } 285 }
@@ -418,6 +447,8 @@ class NumericSolver {
418 } 447 }
419 448
420 def fillSolutionCopy(Map<EObject, EObject> trace) { 449 def fillSolutionCopy(Map<EObject, EObject> trace) {
450 //No need to do a final check to fill if we are using a strategy
451 if (strategy === ExplorationStrategy.CrossingScenario) return
421 val model = threadContext.getModel as PartialInterpretation 452 val model = threadContext.getModel as PartialInterpretation
422 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList 453 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
423 if(constraint2CurrentUnitPropagationPrecondition.empty) { 454 if(constraint2CurrentUnitPropagationPrecondition.empty) {
@@ -481,9 +512,6 @@ class NumericSolver {
481 val value = solution.get(element) 512 val value = solution.get(element)
482 if (value !== null){ 513 if (value !== null){
483 element.fillWithValue(value) 514 element.fillWithValue(value)
484 println("<" + element + "> is filled")
485 } else {
486 println("<" + element + "> is unfilled")
487 } 515 }
488 } 516 }
489 } 517 }