aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-14 08:01:00 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-14 08:01:00 +0100
commita8eb346fb97b54b6ee693da4840abd8be8b43843 (patch)
tree7f63b8432cd50150bff6509e3ff985a40b8763fb
parentadd cs scalability case study artifacts (diff)
downloadVIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.tar.gz
VIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.tar.zst
VIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.zip
Add strategy flag + implement alost working crossingScenarioStrategy
Diffstat
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend16
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java46
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java41
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend19
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend319
8 files changed, 416 insertions, 49 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 da8ca0eb..045387a0 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
@@ -1,5 +1,6 @@
1package hu.bme.mit.inf.dslreasoner.application.execution 1package hu.bme.mit.inf.dslreasoner.application.execution
2 2
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver 4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 5import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
5import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction 6import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction
@@ -16,6 +17,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePro
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration 17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration 18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor 19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.PunishSizeStrategy 22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.PunishSizeStrategy
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner 23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
@@ -28,9 +31,6 @@ import java.util.Optional
28import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel 31import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel
29import org.eclipse.xtext.EcoreUtil2 32import org.eclipse.xtext.EcoreUtil2
30import org.eclipse.xtext.xbase.lib.Functions.Function1 33import org.eclipse.xtext.xbase.lib.Functions.Function1
31import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection
33import java.util.HashMap
34 34
35class SolverLoader { 35class SolverLoader {
36 def loadSolver(Solver solver, Map<String, String> config) { 36 def loadSolver(Solver solver, Map<String, String> config) {
@@ -171,6 +171,16 @@ class SolverLoader {
171 val stringValue = config.get("ignored-attributes") 171 val stringValue = config.get("ignored-attributes")
172 c.ignoredAttributesMap = parseIgnoredAttributes(stringValue) 172 c.ignoredAttributesMap = parseIgnoredAttributes(stringValue)
173 } 173 }
174 if (config.containsKey("strategy")) {
175 val stringValue = config.get("strategy")
176 c.strategy = switch (stringValue) {
177 case "none": ExplorationStrategy.None
178 case "crossingScenario": ExplorationStrategy.CrossingScenario
179 case "cs-hacker": ExplorationStrategy.CSHacker
180 default: throw new IllegalArgumentException("Unknown strategy: " + stringValue)
181 }
182 }
183
174 for (objectiveEntry : objectiveEntries) { 184 for (objectiveEntry : objectiveEntries) {
175 val costObjectiveConfig = new CostObjectiveConfiguration 185 val costObjectiveConfig = new CostObjectiveConfiguration
176 switch (objectiveEntry) { 186 switch (objectiveEntry) {
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index 9e11d2cf..ae94c327 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic {
21 def getNumericSolver() { 21 def getNumericSolver() {
22 if(_numericSolver === null) { 22 if(_numericSolver === null) {
23 // it seems like this getter has no use 23 // it seems like this getter has no use
24 _numericSolver = (new NumericTranslator(null)).selectProblemSolver 24 _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3")
25 } 25 }
26 return _numericSolver 26 return _numericSolver
27 } 27 }
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 e0ebcb6b..36ea64aa 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
@@ -43,8 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
43 private Map<String, String> curVar2Decl; 43 private Map<String, String> curVar2Decl;
44 44
45 private final int TIMEOUT_DOCKER = 5000; 45 private final int TIMEOUT_DOCKER = 5000;
46 private final int TIMEOUT_LOCAL = 10000; 46 private final int TIMEOUT_LOCAL = 100000;
47 private final boolean DEBUG_PRINT = false; 47 private final int DEBUG_PRINT = 3;
48 48
49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { 49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {
50 this.useDocker = useDocker; 50 this.useDocker = useDocker;
@@ -87,7 +87,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
87 } 87 }
88 return null; 88 return null;
89 } 89 }
90 if (DEBUG_PRINT) { 90 if (DEBUG_PRINT > 1) {
91 double duration = (double) (System.nanoTime() - startTime) / 1000000000; 91 double duration = (double) (System.nanoTime() - startTime) / 1000000000;
92 System.out.println("Dur = " + duration + " : "); 92 System.out.println("Dur = " + duration + " : ");
93 } 93 }
@@ -404,11 +404,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
404 System.err.println("TIMEOUT"); 404 System.err.println("TIMEOUT");
405// printOutput(numProbContent); 405// printOutput(numProbContent);
406 } 406 }
407 if (DEBUG_PRINT) { 407 if (DEBUG_PRINT > 1) {
408 // printOutput(numProbContent);
409 // if (outputs != null) printOutput(outputs.get(0));
410 System.out.println(result); 408 System.out.println(result);
411 } 409 }
410 if (DEBUG_PRINT > 2) {
411 printOutput(numProbContent);
412 if (outputs != null) printOutput(outputs.get(0));
413 }
412 414
413 return result; 415 return result;
414 } 416 }
@@ -455,16 +457,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
455 Process outputProcess; 457 Process outputProcess;
456 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); 458 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true);
457 else outputProcess = callDrealLocal(numProbContent, true); 459 else outputProcess = callDrealLocal(numProbContent, true);
458 460
459 List<List<String>> outputs = getProcessOutput(outputProcess); 461 boolean result = false;
460 boolean result = getDrealResult(outputProcess.exitValue(), outputs); 462 List<List<String>> outputs = null;
463 if (outputProcess != null) {
464 outputs = getProcessOutput(outputProcess);
465 result = getDrealResult(outputProcess.exitValue(), outputs);
466 }
467
461 endSolvingProblem = System.nanoTime()-startSolvingProblem; 468 endSolvingProblem = System.nanoTime()-startSolvingProblem;
462 469
463 if (DEBUG_PRINT) { 470 if (outputProcess == null) {
464 System.out.println("Getting Solution!"); 471 System.err.println("TIMEOUT");
465 // printOutput(numProbContent); 472// printOutput(numProbContent);
466 // printOutput(outputs.get(0)); 473 } else {
467 // System.out.println(result); 474 if (DEBUG_PRINT > 0) {
475 System.out.println("Getting Solution!");
476 }
477 }
478 if (DEBUG_PRINT > 1) {
479 System.out.println(result);
480 }
481 if (DEBUG_PRINT > 2) {
482 printOutput(numProbContent);
483 if (outputs != null) printOutput(outputs.get(0));
468 } 484 }
469 485
470 //GET SOLUTION 486 //GET SOLUTION
@@ -498,7 +514,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
498 endFormingSolution = System.nanoTime() - startFormingSolution; 514 endFormingSolution = System.nanoTime() - startFormingSolution;
499 } 515 }
500 else { 516 else {
501 System.out.println("Unsatisfiable numerical problem"); 517 System.out.println("Unsatisfiable numerical problem (trying to get solution...)");
502 } 518 }
503 return sol; 519 return sol;
504 } 520 }
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
new file mode 100644
index 00000000..bd4a10ff
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
@@ -0,0 +1,41 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.io.IOException;
4import java.util.List;
5import java.util.Map;
6
7import org.eclipse.xtext.common.types.JvmIdentifiableElement;
8import org.eclipse.xtext.xbase.XExpression;
9
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
11
12public class NumericDynamicProblemSolver extends NumericProblemSolver{
13
14// private NumericZ3ProblemSolver z3Solver;
15 private NumericDrealProblemSolver drealSolver;
16
17 public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException {
18// this.z3Solver = new NumericZ3ProblemSolver();
19 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath);
20 }
21
22 public NumericProblemSolver selectSolver(String selection) {
23 switch (selection) {
24 case "z3":
25 return new NumericZ3ProblemSolver();
26 case "dreal":
27 return this.drealSolver;
28 default:
29 throw new IllegalArgumentException("Unknown numeric solver selection: " + selection);
30 }
31 }
32
33 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches)
34 throws Exception {
35 throw new Exception("Should not reach here - isSatisfiable");
36 }
37
38 public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs,
39 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
40 throw new Exception("Should not reach here - getOneSolution");
41 }}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
index 3d3f2f4a..791dd644 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -56,24 +56,29 @@ class NumericTranslator {
56 return res 56 return res
57 } 57 }
58 58
59 def NumericProblemSolver selectProblemSolver() { 59 def NumericProblemSolver selectProblemSolver(String selection) {
60// return new NumericProblemSolver 60// return new NumericProblemSolver
61// add numeric solver decision procedure here 61// add numeric solver decision procedure here
62 if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver 62 if (numericSolver instanceof NumericDynamicProblemSolver) {
63 return numericSolver; 63 val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver
64 return dynamicSolver.selectSolver(selection);
65 } else{
66 if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
67 return numericSolver;
68 }
64 } 69 }
65 70
66 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { 71 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) {
67 val input = formNumericProblemInstance(matches) 72 val input = formNumericProblemInstance(matches)
68 val solver = selectProblemSolver 73 val solver = selectProblemSolver(select)
69 val satisfiability = solver.isSatisfiable(input) 74 val satisfiability = solver.isSatisfiable(input)
70 solver.updateTimes 75 solver.updateTimes
71 return satisfiability 76 return satisfiability
72 } 77 }
73 78
74 def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { 79 def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) {
75 val input = formNumericProblemInstance(matches) 80 val input = formNumericProblemInstance(matches)
76 val solver = selectProblemSolver 81 val solver = selectProblemSolver(select)
77 val solution = solver.getOneSolution(primitiveElements,input) 82 val solution = solver.getOneSolution(primitiveElements,input)
78 solver.updateTimes 83 solver.updateTimes
79 return solution 84 return solution
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 338a9af2..0c9612e8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -11,6 +11,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
12 12
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
14 15
15class RelationDefinitionIndexer { 16class RelationDefinitionIndexer {
16 public val PatternGenerator base; 17 public val PatternGenerator base;
@@ -70,6 +71,19 @@ class RelationDefinitionIndexer {
70 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { 71 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) {
71 try { 72 try {
72 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies 73 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
74
75 //TODO ISSUE if a structural and numeric constraint are ORed in the same pattern
76 var boolean isCheck = false
77 for (body : bodies) {
78 for (constraint : body.constraints) {
79 if (constraint instanceof ExpressionEvaluation) {
80 // below not working
81// return ""
82 isCheck = true
83 }
84 }
85 }
86
73 return ''' 87 return '''
74 private pattern «relationDefinitionName(relation,modality)»( 88 private pattern «relationDefinitionName(relation,modality)»(
75 problem:LogicProblem, interpretation:PartialInterpretation, 89 problem:LogicProblem, interpretation:PartialInterpretation,
@@ -79,6 +93,7 @@ class RelationDefinitionIndexer {
79 «FOR constraint : body.constraints» 93 «FOR constraint : body.constraints»
80 «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 94 «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
81 «ENDFOR» 95 «ENDFOR»
96 «IF isCheck»1 == 0;«ENDIF»
82 }«ENDFOR» 97 }«ENDFOR»
83 ''' 98 '''
84 } catch(UnsupportedOperationException e) { 99 } catch(UnsupportedOperationException e) {
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 61a2ac41..74388706 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
@@ -40,6 +40,12 @@ enum NumericSolverSelection {
40 Z3 40 Z3
41} 41}
42 42
43enum ExplorationStrategy {
44 None,
45 CrossingScenario,
46 CSHacker
47}
48
43class ViatraReasonerConfiguration extends LogicSolverConfiguration { 49class ViatraReasonerConfiguration extends LogicSolverConfiguration {
44 // public var Iterable<PQuery> existingQueries 50 // public var Iterable<PQuery> existingQueries
45 public var nameNewElements = false 51 public var nameNewElements = false
@@ -80,6 +86,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
80 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 86 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3
81 public var drealLocalPath = "<path-to-dreal>"; 87 public var drealLocalPath = "<path-to-dreal>";
82 public var Map<String, Map<String, String>> ignoredAttributesMap = null; 88 public var Map<String, Map<String, String>> ignoredAttributesMap = null;
89 public var ExplorationStrategy strategy = ExplorationStrategy.None
83 90
84 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( 91 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
85 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) 92 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
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 b8ea25e5..b8fcb6a0 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
@@ -1,14 +1,19 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver 3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver
4import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver
4import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator 5import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
5import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver 6import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement 8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement 12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement 13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement 15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy
12import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod 17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
13import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection 18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection
14import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
@@ -22,6 +27,7 @@ import org.eclipse.viatra.dse.base.ThreadContext
22import org.eclipse.viatra.query.runtime.api.IPatternMatch 27import org.eclipse.viatra.query.runtime.api.IPatternMatch
23import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 28import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
24import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint 29import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
30import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
25 31
26class NumericSolver { 32class NumericSolver {
27 val ModelGenerationMethod method 33 val ModelGenerationMethod method
@@ -34,6 +40,7 @@ class NumericSolver {
34 val boolean caching; 40 val boolean caching;
35 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap 41 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
36 val String drealLocalPath; 42 val String drealLocalPath;
43 val ExplorationStrategy strategy;
37 44
38 var long runtime = 0 45 var long runtime = 0
39 var long cachingTime = 0 46 var long cachingTime = 0
@@ -45,24 +52,43 @@ class NumericSolver {
45 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks 52 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
46 this.caching = caching 53 this.caching = caching
47 this.drealLocalPath = config.drealLocalPath 54 this.drealLocalPath = config.drealLocalPath
48 this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) 55 this.strategy = config.strategy
56 this.t = new NumericTranslator(createNumericTranslator(config))
49 } 57 }
50 58
51 def createNumericTranslator(NumericSolverSelection solverSelection) { 59 def createNumericTranslator(ViatraReasonerConfiguration config) {
52 if (solverSelection == NumericSolverSelection.DREAL_DOCKER) 60 val solverSelection = config.numericSolverSelection
53 return new NumericDrealProblemSolver(true, null) 61 val strategy = config.strategy
54 if (solverSelection == NumericSolverSelection.DREAL_LOCAL) 62 if (strategy == ExplorationStrategy.None) {
55 return new NumericDrealProblemSolver(false, drealLocalPath) 63 //initialise the specified
56 if (solverSelection == NumericSolverSelection.Z3) { 64 if (solverSelection == NumericSolverSelection.DREAL_DOCKER)
65 return new NumericDrealProblemSolver(true, null)
66 if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
67 return new NumericDrealProblemSolver(false, drealLocalPath)
68 if (solverSelection == NumericSolverSelection.Z3) {
69 //TODO THIS IS HARD-CODED for now
70// val root = "/data/viatra/VIATRA-Generator";
71 val root = "/home/models/VIATRA-Generator";
72 //END HARD-CODED
73 // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
74 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
75 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
76 // System.load("libz3.so");
77 // System.load("libz3java.so");
78 return new NumericZ3ProblemSolver
79 }
80 }
81 else {
82 //initialise both dreal-local and z3
83
57 //TODO THIS IS HARD-CODED for now 84 //TODO THIS IS HARD-CODED for now
58 val root = "/data/viatra/VIATRA-Generator"; 85// val root = "/data/viatra/VIATRA-Generator";
86 val root = "/home/models/VIATRA-Generator";
59 //END HARD-CODED 87 //END HARD-CODED
60// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); 88// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
61 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); 89 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
62 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 90 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
63// System.load("libz3.so"); 91 return new NumericDynamicProblemSolver(drealLocalPath)
64// System.load("libz3java.so");
65 return new NumericZ3ProblemSolver
66 } 92 }
67 } 93 }
68 94
@@ -95,31 +121,49 @@ class NumericSolver {
95 def getNumericSolverSelection(){this.t.numericSolver} 121 def getNumericSolverSelection(){this.t.numericSolver}
96 122
97 def boolean maySatisfiable() { 123 def boolean maySatisfiable() {
124 val int phase = determinePhase()
125
98 if(intermediateConsistencyCheck) { 126 if(intermediateConsistencyCheck) {
99 return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) 127 return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase)
100 } else { 128 } else {
101 return true 129 return true
102 } 130 }
103 } 131 }
104 def boolean currentSatisfiable() { 132 def boolean currentSatisfiable() {
105 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) 133 val int phase = determinePhase()
134 //TODO generalize this
135 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase)
106 } 136 }
107 137
108 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { 138 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) {
109 val start = System.nanoTime 139 val start = System.nanoTime
110 var boolean finalResult 140 var boolean finalResult
141 val boolean needsFilling = needsFilling
142 val model = threadContext.getModel as PartialInterpretation
143 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
144
111 if(matches.empty){ 145 if(matches.empty){
112 finalResult=true 146 finalResult=true
113 } else { 147 } else {
114 val propagatedConstraints = new HashMap 148 val propagatedConstraints = new HashMap
115// println("<<<<START-STEP>>>>") 149 //Filter constraints if there are phase-related restricutions
150 //null whitelist means accept everything
151 val whitelist = getConstraintWhitelist(phase)
152 println("<<<<START-STEP>>>> (" + phase + ")")
116 for(entry : matches.entrySet) { 153 for(entry : matches.entrySet) {
117 val constraint = entry.key 154 if (entry.value !== null){
118// println("--match?-- " + constraint) 155 val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName
119 val allMatches = entry.value.allMatches.map[it.toArray] 156 if (whitelist === null || whitelist.contains(name)) {
120// println("---------- " + entry.value.allMatches) 157// println(name)
121 propagatedConstraints.put(constraint,allMatches) 158 val constraint = entry.key
159// println("--match?-- " + constraint)
160 val allMatches = entry.value.allMatches.map[it.toArray]
161 // println("---------- " + entry.value.allMatches)
162 propagatedConstraints.put(constraint,allMatches)
163 }
164 }
122 } 165 }
166 //check numeric problem
123 if(propagatedConstraints.values.forall[empty]) { 167 if(propagatedConstraints.values.forall[empty]) {
124 finalResult=true 168 finalResult=true
125 } else { 169 } else {
@@ -133,16 +177,35 @@ class NumericSolver {
133 // } 177 // }
134 //println(code.hashCode) 178 //println(code.hashCode)
135 this.numberOfSolverCalls++ 179 this.numberOfSolverCalls++
136 val res = t.delegateIsSatisfiable(propagatedConstraints) 180 var boolean res = false
181 if (needsFilling){
182 //TODO ASSUME Always True
183 //GET LIST OF VARS TO FILL
184 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
185 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
186 res = true
187 } else {
188 res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
189 }
190 //TODO FIX CACHING
137 satisfiabilityCache.put(code,res) 191 satisfiabilityCache.put(code,res)
138 finalResult=res 192 finalResult=res
139 } else { 193 } else {
140 //println('''similar problem, answer from cache''') 194 //println('''similar problem, answer from cache''')
195 println('''potential issue, answer from cache''')
141 finalResult=cachedResult 196 finalResult=cachedResult
142 this.numberOfCachedSolverCalls++ 197 this.numberOfCachedSolverCalls++
143 } 198 }
144 } else { 199 } else {
145 finalResult= t.delegateIsSatisfiable(propagatedConstraints) 200 if (needsFilling){
201 //TODO ASSUME Always True
202 //GET LIST OF VARS TO FILL
203 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
204 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
205 finalResult = true
206 } else {
207 finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
208 }
146 this.numberOfSolverCalls++ 209 this.numberOfSolverCalls++
147 } 210 }
148 } 211 }
@@ -151,6 +214,201 @@ class NumericSolver {
151 return finalResult 214 return finalResult
152 } 215 }
153 216
217 def selectSolver(int phase) {
218 if (strategy === ExplorationStrategy.CrossingScenario){
219 if (phase == 1) return "dreal"
220 else return "dreal"
221 }
222 return "irrelevant"
223 }
224
225 def int determinePhase() {
226 // >= 0 : an actual phase
227 // -1 : take all numeric constraints
228 // -2 : SKIP (take no numeric constraints)
229 if (strategy == ExplorationStrategy.CrossingScenario) {
230 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
231 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
232 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
233 var boolean foundActorWithDefinedPos = false;
234 for (PartialRelationInterpretation rel : relations) {
235 if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) {
236 for (RelationLink link : rel.getRelationlinks()) {
237 val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement;
238 if (param2.isValueSet()) {
239 foundActorWithDefinedPos = true;
240 }
241 }
242 }
243
244 if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) {
245 if (!rel.getRelationlinks().isEmpty()) {
246 return 3;
247 }
248 }
249 }
250 //it means that there is no blockedBy
251 //so we are at most at phase 2
252 if (foundActorWithDefinedPos) return 2;
253 return 1;
254 }
255 return -1;
256 }
257
258 def getConstraintWhitelist(int phase) {
259 val List<String> wl = newArrayList
260 //null return means accept everything
261 if (strategy === ExplorationStrategy.None){
262 return null
263 } else if (strategy === ExplorationStrategy.CrossingScenario){
264 /*
265 "define_placedOn_actorOnVerticalLane",
266 "define_placedOn_actorOnHorizLane",
267
268 "define_actor_maxXp",
269 "define_actor_minXp",
270 "define_actor_maxYp",
271 "define_actor_minYp",
272
273 "define_actor_wrtLane",
274
275 "define_actor_minimumDistance",
276
277 "define_actor_actorOnVertLaneHasxSpeed0",
278 "define_actor_actorOnVertLaneMinYs",
279 "define_actor_actorOnVertLaneMaxYs",
280 "define_actor_actorOnHorizLaneHasySpeed0",
281 "define_actor_actorOnHorizLaneMinXs",
282 "define_actor_actorOnHorizLaneMaxXs",
283
284 "define_actor_pedestrianWidth",
285 "define_actor_pedestrianLength",
286 "define_actor_vehicleWidth",
287 "define_actor_vehicleWidth",
288 "define_actor_vehicleLength",
289 "define_actor_vehicleLength",
290
291 "collisionExists_timeWithinBound",
292 "collisionExists_timeNotNegative",
293 "collisionExists_defineCollision_y1",
294 "collisionExists_defineCollision_y2",
295 "collisionExists_defineCollision_x1",
296 "collisionExists_defineCollision_x2",
297
298 "visionBlocked_ites_notOnSameVertLine",
299 "visionBlocked_ites_top",
300 "visionBlocked_ites_bottom",
301 "visionBlocked_xdistBSlargerThanxdistTS",
302 "visionBlocked_xdistBTlargerThanxdistST",
303 "visionBlocked_ydistBSlargerThanydistTS",
304 "visionBlocked_ydistBTlargerThanydistST"
305 */
306
307 //HINTS:
308 //define_actor_wrtLane
309 //28.5 is structural hint
310 switch (phase) {
311 case 1: {
312 wl.addAll(#[
313 "define_placedOn_actorOnVerticalLane",
314 "define_placedOn_actorOnHorizLane",
315
316 "define_actor_maxXp",
317 "define_actor_minXp",
318 "define_actor_maxYp",
319 "define_actor_minYp",
320
321 "define_actor_pedestrianWidth",
322 "define_actor_pedestrianLength",
323 "define_actor_vehicleWidth",
324 "define_actor_vehicleWidth",
325 "define_actor_vehicleLength",
326 "define_actor_vehicleLength"
327
328 ])
329 }
330 case 2: {
331 wl.addAll(#[
332
333 "define_placedOn_actorOnVerticalLane",
334 "define_placedOn_actorOnHorizLane",
335
336 "define_actor_maxXp",
337 "define_actor_minXp",
338 "define_actor_maxYp",
339 "define_actor_minYp",
340
341 "define_actor_minimumDistance",
342
343 "define_actor_pedestrianWidth",
344 "define_actor_pedestrianLength",
345 "define_actor_vehicleWidth",
346 "define_actor_vehicleWidth",
347 "define_actor_vehicleLength",
348 "define_actor_vehicleLength",
349
350 "visionBlocked_ites_notOnSameVertLine",
351 "visionBlocked_ites_top",
352 "visionBlocked_ites_bottom",
353 "visionBlocked_xdistBSlargerThanxdistTS",
354 "visionBlocked_xdistBTlargerThanxdistST",
355 "visionBlocked_ydistBSlargerThanydistTS",
356 "visionBlocked_ydistBTlargerThanydistST"
357 ])
358 }
359 case 3: {
360 wl.addAll(#[
361
362 "define_placedOn_actorOnVerticalLane",
363 "define_placedOn_actorOnHorizLane",
364
365 "define_actor_maxXp",
366 "define_actor_minXp",
367 "define_actor_maxYp",
368 "define_actor_minYp",
369
370 "define_actor_minimumDistance",
371
372 "define_actor_actorOnVertLaneHasxSpeed0",
373 "define_actor_actorOnVertLaneMinYs",
374 "define_actor_actorOnVertLaneMaxYs",
375 "define_actor_actorOnHorizLaneHasySpeed0",
376 "define_actor_actorOnHorizLaneMinXs",
377 "define_actor_actorOnHorizLaneMaxXs",
378
379 "define_actor_pedestrianWidth",
380 "define_actor_pedestrianLength",
381 "define_actor_vehicleWidth",
382 "define_actor_vehicleWidth",
383 "define_actor_vehicleLength",
384 "define_actor_vehicleLength",
385
386 "collisionExists_timeWithinBound",
387 "collisionExists_timeNotNegative",
388 "collisionExists_defineCollision_y1",
389 "collisionExists_defineCollision_y2",
390 "collisionExists_defineCollision_x1",
391 "collisionExists_defineCollision_x2"
392 ])
393 }
394 default: {
395 //this is for 3 if we implement 4
396// bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7])
397
398 //this is for 4 if we do it
399 wl.addAll(#[])
400 return null
401 }
402 }
403 }
404 return wl
405 }
406
407 def getNeedsFilling(){
408 if (strategy == ExplorationStrategy.CrossingScenario) return true
409 return false
410 }
411
154 def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { 412 def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
155 val start = System.nanoTime 413 val start = System.nanoTime
156 val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList 414 val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
@@ -175,7 +433,7 @@ class NumericSolver {
175 if(propagatedConstraints.values.forall[empty]) { 433 if(propagatedConstraints.values.forall[empty]) {
176 fillWithDefaultValues(dataObjects,trace) 434 fillWithDefaultValues(dataObjects,trace)
177 } else { 435 } else {
178 val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) 436 val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal")
179 fillWithSolutions(dataObjects,solution,trace) 437 fillWithSolutions(dataObjects,solution,trace)
180 } 438 }
181 } 439 }
@@ -215,4 +473,19 @@ class NumericSolver {
215 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} 473 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
216 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } 474 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double }
217 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} 475 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
476
477 def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) {
478 for(element : elements) {
479 //we allow overwriting of already set variables
480 if(solution.containsKey(element)) {
481 val value = solution.get(element)
482 if (value !== null){
483 element.fillWithValue(value)
484 println("<" + element + "> is filled")
485 } else {
486 println("<" + element + "> is unfilled")
487 }
488 }
489 }
490 }
218} \ No newline at end of file 491} \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-19 05:07:56 +0000