aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <semerath@mit.bme.hu>2021-07-30 10:04:27 +0200
committerLibravatar OszkarSemerath <semerath@mit.bme.hu>2021-07-30 10:04:27 +0200
commitaaa67b0ef8840d97b062a4f1383bf93410984af3 (patch)
tree2c07208bb6b5ab27b47bd477dfbcc6e77b50d623
parentConfig updated and createSharedVersionedMapStores service (diff)
downloadVIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.tar.gz
VIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.tar.zst
VIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.zip
Numeric solver dreal hardcoding -> configV4transformation
Diffstat
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/plugin.xml2
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java169
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java28
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java (renamed from Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java)24
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java22
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend21
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java60
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF2
-rw-r--r--Solvers/SMT-Solver/com.microsoft.z3/com.microsoft.z3.jar_GoesHere.txt0
-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.xtend3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend (renamed from Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend)1056
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend6
-rw-r--r--Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java2
19 files changed, 660 insertions, 753 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/plugin.xml b/Application/hu.bme.mit.inf.dslreasoner.application/plugin.xml
index 9b66071c..956abc6e 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/plugin.xml
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/plugin.xml
@@ -6,5 +6,5 @@
6 uri = "http://www.bme.hu/mit/inf/dslreasoner/application/ApplicationConfiguration" 6 uri = "http://www.bme.hu/mit/inf/dslreasoner/application/ApplicationConfiguration"
7 class = "hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ApplicationConfigurationPackage" 7 class = "hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ApplicationConfigurationPackage"
8 genModel = "model/generated/ApplicationConfiguration.genmodel" /> 8 genModel = "model/generated/ApplicationConfiguration.genmodel" />
9 </extension> 9 </extension>
10</plugin> 10</plugin>
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 ac4f29a9..f8147598 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
@@ -158,7 +158,7 @@ class SolverLoader {
158 } 158 }
159 if (config.containsKey("dreal-timeout")) { 159 if (config.containsKey("dreal-timeout")) {
160 val stringValue = config.get("dreal-timeout") 160 val stringValue = config.get("dreal-timeout")
161 c.drealTimeout = Integer.parseInt(stringValue) 161 c.numericSolverTimeout = Integer.parseInt(stringValue)
162 } 162 }
163 if (config.containsKey("scopePropagator")) { 163 if (config.containsKey("scopePropagator")) {
164 val stringValue = config.get("scopePropagator") 164 val stringValue = config.get("scopePropagator")
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
index 23fba304..d8e9608d 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
@@ -21,7 +21,7 @@ Require-Bundle: com.google.guava,
21 org.eclipse.xtext, 21 org.eclipse.xtext,
22 org.eclipse.xtext.xbase;bundle-version="2.18.0", 22 org.eclipse.xtext.xbase;bundle-version="2.18.0",
23 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", 23 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
24 com.microsoft.z3 24 com.microsoft.z3;bundle-version="4.8.8"
25Bundle-ActivationPolicy: lazy 25Bundle-ActivationPolicy: lazy
26Export-Package: 26Export-Package:
27 hu.bme.mit.inf.dslreasoner.viatra2logic, 27 hu.bme.mit.inf.dslreasoner.viatra2logic,
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java
deleted file mode 100644
index 7b8634c4..00000000
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java
+++ /dev/null
@@ -1,169 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.lang.reflect.InvocationTargetException;
4
5import org.eclipse.emf.common.notify.Adapter;
6import org.eclipse.emf.common.notify.Notification;
7import org.eclipse.emf.common.util.EList;
8import org.eclipse.emf.common.util.TreeIterator;
9import org.eclipse.emf.ecore.EClass;
10import org.eclipse.emf.ecore.EObject;
11import org.eclipse.emf.ecore.EOperation;
12import org.eclipse.emf.ecore.EReference;
13import org.eclipse.emf.ecore.EStructuralFeature;
14import org.eclipse.emf.ecore.resource.Resource;
15
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
18
19public class FakeIntegerElement implements PrimitiveElement{
20
21 public FakeIntegerElement() {
22
23 }
24
25 @Override
26 public EList<TypeDefinition> getDefinedInType() {
27 // TODO Auto-generated method stub
28 return null;
29 }
30
31 @Override
32 public String getName() {
33 // TODO Auto-generated method stub
34 return null;
35 }
36
37 @Override
38 public void setName(String value) {
39 // TODO Auto-generated method stub
40
41 }
42
43 @Override
44 public EClass eClass() {
45 // TODO Auto-generated method stub
46 return null;
47 }
48
49 @Override
50 public Resource eResource() {
51 // TODO Auto-generated method stub
52 return null;
53 }
54
55 @Override
56 public EObject eContainer() {
57 // TODO Auto-generated method stub
58 return null;
59 }
60
61 @Override
62 public EStructuralFeature eContainingFeature() {
63 // TODO Auto-generated method stub
64 return null;
65 }
66
67 @Override
68 public EReference eContainmentFeature() {
69 // TODO Auto-generated method stub
70 return null;
71 }
72
73 @Override
74 public EList<EObject> eContents() {
75 // TODO Auto-generated method stub
76 return null;
77 }
78
79 @Override
80 public TreeIterator<EObject> eAllContents() {
81 // TODO Auto-generated method stub
82 return null;
83 }
84
85 @Override
86 public boolean eIsProxy() {
87 // TODO Auto-generated method stub
88 return false;
89 }
90
91 @Override
92 public EList<EObject> eCrossReferences() {
93 // TODO Auto-generated method stub
94 return null;
95 }
96
97 @Override
98 public Object eGet(EStructuralFeature feature) {
99 // TODO Auto-generated method stub
100 return null;
101 }
102
103 @Override
104 public Object eGet(EStructuralFeature feature, boolean resolve) {
105 // TODO Auto-generated method stub
106 return null;
107 }
108
109 @Override
110 public void eSet(EStructuralFeature feature, Object newValue) {
111 // TODO Auto-generated method stub
112
113 }
114
115 @Override
116 public boolean eIsSet(EStructuralFeature feature) {
117 // TODO Auto-generated method stub
118 return false;
119 }
120
121 @Override
122 public void eUnset(EStructuralFeature feature) {
123 // TODO Auto-generated method stub
124
125 }
126
127 @Override
128 public Object eInvoke(EOperation operation, EList<?> arguments) throws InvocationTargetException {
129 // TODO Auto-generated method stub
130 return null;
131 }
132
133 @Override
134 public EList<Adapter> eAdapters() {
135 // TODO Auto-generated method stub
136 return null;
137 }
138
139 @Override
140 public boolean eDeliver() {
141 // TODO Auto-generated method stub
142 return false;
143 }
144
145 @Override
146 public void eSetDeliver(boolean deliver) {
147 // TODO Auto-generated method stub
148
149 }
150
151 @Override
152 public void eNotify(Notification notification) {
153 // TODO Auto-generated method stub
154
155 }
156
157 @Override
158 public boolean isValueSet() {
159 // TODO Auto-generated method stub
160 return false;
161 }
162
163 @Override
164 public void setValueSet(boolean value) {
165 // TODO Auto-generated method stub
166
167 }
168
169}
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 cecd3623..f30e390b 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
@@ -365,8 +365,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
365 Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); 365 Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);
366 for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { 366 for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {
367 String constraint = formNumericConstraint(e, aMatch); 367 String constraint = formNumericConstraint(e, aMatch);
368 if (constraint != null) { 368 if (constraint != null) {
369 String negAssert = "(assert " + constraint + ")"; 369 String negAssert = "(assert " + constraint + ")";
370 curConstraints.add(negAssert); 370 curConstraints.add(negAssert);
371 } 371 }
372 } 372 }
@@ -426,8 +426,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
426 426
427 boolean result = false; 427 boolean result = false;
428 List<List<String>> outputs = null; 428 List<List<String>> outputs = null;
429 if (outputProcess != null) { 429 if (outputProcess != null) {
430 outputs = getProcessOutput(outputProcess); 430 outputs = getProcessOutput(outputProcess);
431 result = getDrealResult(outputProcess.exitValue(), outputs); 431 result = getDrealResult(outputProcess.exitValue(), outputs);
432// } else { 432// } else {
433// System.err.print("Timeout, RETRYING..."); 433// System.err.print("Timeout, RETRYING...");
@@ -575,4 +575,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
575 //TODO Check if above went well? 575 //TODO Check if above went well?
576 } 576 }
577 577
578 @Override
579 protected void initialize() {
580 // TODO Auto-generated method stub
581
582 }
583
584 @Override
585 protected boolean internalIsSatisfiable(
586 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
587 // TODO Auto-generated method stub
588 return false;
589 }
590
591 @Override
592 protected Map<PrimitiveElement, Number> internalGetOneSolution(List<PrimitiveElement> objs,
593 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
594 // TODO Auto-generated method stub
595 return null;
596 }
597
578} 598}
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/NumericDynamicProblemSolverXXX.java
index e8c20138..199c089b 100644
--- 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/NumericDynamicProblemSolverXXX.java
@@ -9,13 +9,13 @@ import org.eclipse.xtext.xbase.XExpression;
9 9
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
11 11
12public class NumericDynamicProblemSolver extends NumericProblemSolver{ 12public class NumericDynamicProblemSolverXXX extends NumericProblemSolver{
13 13
14// private NumericZ3ProblemSolver z3Solver; 14// private NumericZ3ProblemSolver z3Solver;
15 private NumericDrealProblemSolver drealSolver; 15 private NumericDrealProblemSolver drealSolver;
16 private int timeout; 16 private int timeout;
17 17
18 public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { 18 public NumericDynamicProblemSolverXXX(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
19// this.z3Solver = new NumericZ3ProblemSolver(); 19// this.z3Solver = new NumericZ3ProblemSolver();
20 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); 20 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout);
21 this.timeout = drealTimeout; 21 this.timeout = drealTimeout;
@@ -40,4 +40,24 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{
40 public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs, 40 public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs,
41 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { 41 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
42 throw new Exception("Should not reach here - getOneSolution"); 42 throw new Exception("Should not reach here - getOneSolution");
43 }
44
45 @Override
46 protected void initialize() {
47 // TODO Auto-generated method stub
48
49 }
50
51 @Override
52 protected boolean internalIsSatisfiable(
53 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
54 // TODO Auto-generated method stub
55 return false;
56 }
57
58 @Override
59 protected Map<PrimitiveElement, Number> internalGetOneSolution(List<PrimitiveElement> objs,
60 Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
61 // TODO Auto-generated method stub
62 return null;
43 }} 63 }}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java
index 5e823d9d..8f57e40c 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java
@@ -35,6 +35,24 @@ public abstract class NumericProblemSolver {
35 public long getEndSolvingProblem() {return endSolvingProblem;} 35 public long getEndSolvingProblem() {return endSolvingProblem;}
36 public long getEndFormingSolution() {return endFormingSolution;} 36 public long getEndFormingSolution() {return endFormingSolution;}
37 37
38 public abstract boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; 38 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
39 public abstract Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; 39 if(!initialized) {
40 this.initialize();
41 this.initialized=true;
42 }
43 return this.internalIsSatisfiable(matches);
44 }
45 public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception{
46 if(!initialized) {
47 this.initialize();
48 this.initialized=true;
49 }
50 return this.internalGetOneSolution(objs, matches);
51 }
52
53 boolean initialized = false;
54 protected abstract void initialize();
55
56 protected abstract boolean internalIsSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception;
57 protected abstract Map<PrimitiveElement,Number> internalGetOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception;
40} 58}
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 a11ae8a8..9ae36a6d 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
@@ -58,31 +58,18 @@ class NumericTranslator {
58 return res 58 return res
59 } 59 }
60 60
61 def NumericProblemSolver selectProblemSolver(String selection) {
62// return new NumericProblemSolver
63// add numeric solver decision procedure here
64 if (numericSolver instanceof NumericDynamicProblemSolver) {
65 val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver
66 return dynamicSolver.selectSolver(selection);
67 } else{
68 if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout)
69 return numericSolver;
70 }
71 }
72 61
73 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) { 62 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) {
74 val input = formNumericProblemInstance(matches) 63 val input = formNumericProblemInstance(matches)
75 val solver = selectProblemSolver(select) 64 val satisfiability = numericSolver.isSatisfiable(input)
76 val satisfiability = solver.isSatisfiable(input) 65 numericSolver.updateTimes
77 solver.updateTimes
78 return satisfiability 66 return satisfiability
79 } 67 }
80 68
81 def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) { 69 def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) {
82 val input = formNumericProblemInstance(matches) 70 val input = formNumericProblemInstance(matches)
83 val solver = selectProblemSolver(select) 71 val solution = numericSolver.getOneSolution(primitiveElements,input)
84 val solution = solver.getOneSolution(primitiveElements,input) 72 numericSolver.updateTimes
85 solver.updateTimes
86 return solution 73 return solution
87 } 74 }
88 75
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
index 0799953f..5b4f6de1 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
@@ -35,24 +35,18 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
35 private Context ctx; 35 private Context ctx;
36 private Solver s; 36 private Solver s;
37 private Map<Object, Expr> varMap; 37 private Map<Object, Expr> varMap;
38 private int timeout;
38 39
39 public NumericZ3ProblemSolver(int timeout) { 40 public NumericZ3ProblemSolver(int timeout) {
40 //FOR LINUX VM 41 this.timeout=timeout;
41 //Not Elegant, but this is working for now
42// String root = "/home/models/VIATRA-Generator";
43// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
44// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
45// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
46 //End non-elegance
47
48 HashMap<String, String> cfg = new HashMap<String, String>(); 42 HashMap<String, String> cfg = new HashMap<String, String>();
49 cfg.put("model", "true"); 43 cfg.put("model", "true");
50 ctx = new Context(cfg); 44 ctx = new Context(cfg);
51 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); 45 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
52 s = ctx.mkSolver(); 46 s = ctx.mkSolver();
53 if (timeout != -1) { 47 if (timeout != -1) {
54 Params p = ctx.mkParams(); 48 Params p = ctx.mkParams();
55 p.add("timeout", timeout); 49 p.add("timeout", timeout);
56 s.setParameters(p); 50 s.setParameters(p);
57 } 51 }
58 varMap = new HashMap<Object, Expr>(); 52 varMap = new HashMap<Object, Expr>();
@@ -62,7 +56,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
62 return ctx; 56 return ctx;
63 } 57 }
64 58
65 private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { 59 private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(final XExpression expression) {
66 ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); 60 ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
67 XExpression left = ((XBinaryOperation) expression).getLeftOperand(); 61 XExpression left = ((XBinaryOperation) expression).getLeftOperand();
68 XExpression right = ((XBinaryOperation) expression).getRightOperand(); 62 XExpression right = ((XBinaryOperation) expression).getRightOperand();
@@ -80,8 +74,36 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
80 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); 74 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
81 } 75 }
82 } 76 }
83 77
84 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { 78 @Override
79 protected void initialize() {
80 // TODO Auto-generated method stub
81
82 }
83
84 private void start() {
85 HashMap<String, String> cfg = new HashMap<String, String>();
86 cfg.put("model", "true");
87 ctx = new Context(cfg);
88 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
89 s = ctx.mkSolver();
90 if (timeout != -1) {
91 Params p = ctx.mkParams();
92 p.add("timeout", timeout);
93 s.setParameters(p);
94 }
95 varMap = new HashMap<Object, Expr>();
96 }
97 private void stop() {
98 ctx=null;
99 s=null;
100 varMap=null;
101 }
102
103 @Override
104 protected boolean internalIsSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
105 start();
106
85 long startformingProblem = System.nanoTime(); 107 long startformingProblem = System.nanoTime();
86 BoolExpr problemInstance = formNumericProblemInstance(matches); 108 BoolExpr problemInstance = formNumericProblemInstance(matches);
87 s.add(problemInstance); 109 s.add(problemInstance);
@@ -94,10 +116,15 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
94// System.out.println("end"); 116// System.out.println("end");
95 endSolvingProblem = System.nanoTime()-startSolvingProblem; 117 endSolvingProblem = System.nanoTime()-startSolvingProblem;
96 this.ctx.close(); 118 this.ctx.close();
119
120 stop();
97 return result; 121 return result;
98 } 122 }
99 123
100 public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { 124 @Override
125 protected Map<PrimitiveElement,Number> internalGetOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
126 start();
127
101 Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); 128 Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>();
102 long startformingProblem = System.nanoTime(); 129 long startformingProblem = System.nanoTime();
103 BoolExpr problemInstance = formNumericProblemInstance(matches); 130 BoolExpr problemInstance = formNumericProblemInstance(matches);
@@ -147,6 +174,9 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
147 System.out.println("Unsatisfiable numerical problem"); 174 System.out.println("Unsatisfiable numerical problem");
148 } 175 }
149 this.ctx.close(); 176 this.ctx.close();
177
178 stop();
179
150 return sol; 180 return sol;
151 } 181 }
152 182
@@ -271,6 +301,8 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
271 } 301 }
272 302
273 303
304
305
274 /* 306 /*
275 public void testIsSat(XExpression expression, Term t) throws Exception { 307 public void testIsSat(XExpression expression, Term t) throws Exception {
276 int count = 10000; 308 int count = 10000;
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
index 75581def..1055dd6d 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
@@ -22,6 +22,6 @@ Require-Bundle: com.google.guava,
22 org.eclipse.viatra.query.runtime;bundle-version="2.0.0" 22 org.eclipse.viatra.query.runtime;bundle-version="2.0.0"
23Bundle-RequiredExecutionEnvironment: JavaSE-1.8 23Bundle-RequiredExecutionEnvironment: JavaSE-1.8
24Bundle-ActivationPolicy: lazy 24Bundle-ActivationPolicy: lazy
25Bundle-NativeCode: libminisat.so;osname=Linux;processor=x86_64 25Bundle-NativeCode: libminisat.so;osname=Linux;processor=x86_64,*
26Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner 26Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
27Import-Package: org.apache.log4j;version="1.2.15" 27Import-Package: org.apache.log4j;version="1.2.15"
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/com.microsoft.z3.jar_GoesHere.txt b/Solvers/SMT-Solver/com.microsoft.z3/com.microsoft.z3.jar_GoesHere.txt
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/com.microsoft.z3.jar_GoesHere.txt
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 a692e1e5..98d07069 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
@@ -22,7 +22,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyFor
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint 22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler 23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver
26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation 25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective 26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
@@ -39,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
39import org.eclipse.viatra.dse.solutionstore.SolutionStore 38import org.eclipse.viatra.dse.solutionstore.SolutionStore
40import org.eclipse.viatra.dse.statecode.IStateCoderFactory 39import org.eclipse.viatra.dse.statecode.IStateCoderFactory
41import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver 40import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver
41import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericRefinementUnit
42 42
43class ViatraReasoner extends LogicReasoner { 43class ViatraReasoner extends LogicReasoner {
44 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() 44 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
@@ -110,7 +110,7 @@ class ViatraReasoner extends LogicReasoner {
110 new SolutionStore(numberOfRequiredSolutions) 110 new SolutionStore(numberOfRequiredSolutions)
111 } 111 }
112 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) 112 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
113 val numericSolver = new NumericSolver(method, viatraConfig, false)//was formerly hard-coded to false for caching 113 val numericSolver = new NumericRefinementUnit(method, viatraConfig, false)//was formerly hard-coded to false for caching
114 val solutionSaver = method.solutionSaver 114 val solutionSaver = method.solutionSaver
115 solutionSaver.numericSolver = numericSolver 115 solutionSaver.numericSolver = numericSolver
116 val solutionCopier = solutionSaver.solutionCopier 116 val solutionCopier = solutionSaver.solutionCopier
@@ -156,7 +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 //println(">>begin exploration")
160 var boolean stoppedByTimeout 160 var boolean stoppedByTimeout
161 try { 161 try {
162 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/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index 923c847e..fc1fadf7 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
@@ -84,8 +84,9 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
84 public var unfinishedWFWeight = 1 84 public var unfinishedWFWeight = 1
85 public var calculateObjectCreationCosts = false 85 public var calculateObjectCreationCosts = false
86 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 86 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3
87 public var NumericSolverPath = "<path-to-numeric-solver>"
87 public var drealLocalPath = "<path-to-dreal>"; 88 public var drealLocalPath = "<path-to-dreal>";
88 public var drealTimeout = 10000; 89 public var numericSolverTimeout = 10000;
89 public var Map<String, Map<String, String>> ignoredAttributesMap = null; 90 public var Map<String, Map<String, String>> ignoredAttributesMap = null;
90 public var ExplorationStrategy strategy = ExplorationStrategy.None 91 public var ExplorationStrategy strategy = ExplorationStrategy.None
91 92
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 c62d124a..1ac12914 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
@@ -79,7 +79,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
79// private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; 79// private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
80 public ActivationSelector activationSelector = new EvenActivationSelector(random); 80 public ActivationSelector activationSelector = new EvenActivationSelector(random);
81 public ViatraReasonerSolutionSaver solutionSaver; 81 public ViatraReasonerSolutionSaver solutionSaver;
82 public NumericSolver numericSolver; 82 public NumericRefinementUnit numericSolver;
83 // Statistics 83 // Statistics
84 private int numberOfStatecoderFail = 0; 84 private int numberOfStatecoderFail = 0;
85 private int numberOfPrintedModel = 0; 85 private int numberOfPrintedModel = 0;
@@ -94,7 +94,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
94 ViatraReasonerConfiguration configuration, 94 ViatraReasonerConfiguration configuration,
95 ModelGenerationMethod method, 95 ModelGenerationMethod method,
96 ViatraReasonerSolutionSaver solutionSaver, 96 ViatraReasonerSolutionSaver solutionSaver,
97 NumericSolver numericSolver) { 97 NumericRefinementUnit numericSolver) {
98 this.workspace = workspace; 98 this.workspace = workspace;
99 this.configuration = configuration; 99 this.configuration = configuration;
100 this.method = method; 100 this.method = method;
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/NumericRefinementUnit.xtend
index a228afc6..b3e2d78d 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/NumericRefinementUnit.xtend
@@ -1,533 +1,531 @@
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 6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink 7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement 8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation 11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement 12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement 13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink 14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement 15import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy 16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod 17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection
18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection 18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 19import java.util.HashMap
20import java.util.HashMap 20import java.util.LinkedHashMap
21import java.util.LinkedHashMap 21import java.util.LinkedHashSet
22import java.util.LinkedHashSet 22import java.util.List
23import java.util.List 23import java.util.Map
24import java.util.Map 24import org.eclipse.emf.ecore.EObject
25import org.eclipse.emf.ecore.EObject 25import org.eclipse.viatra.dse.base.ThreadContext
26import org.eclipse.viatra.dse.base.ThreadContext 26import org.eclipse.viatra.dse.objectives.Fitness
27import org.eclipse.viatra.dse.objectives.Fitness 27import org.eclipse.viatra.query.runtime.api.IPatternMatch
28import org.eclipse.viatra.query.runtime.api.IPatternMatch 28import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
29import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 29import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint 30import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
31import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation 31import org.eclipse.viatra.dse.objectives.IObjective
32import org.eclipse.viatra.dse.objectives.IObjective 32
33 33class NumericRefinementUnit {
34class NumericSolver { 34 val ModelGenerationMethod method
35 val ModelGenerationMethod method 35 var ThreadContext threadContext
36 var ThreadContext threadContext 36 val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
37 val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 37 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
38 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 38 var NumericTranslator translator = null;
39 NumericTranslator t 39
40 40
41 val boolean intermediateConsistencyCheck 41 val boolean intermediateConsistencyCheck
42 val boolean caching; 42 val boolean caching;
43 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap 43 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
44 val String drealLocalPath; 44 val ExplorationStrategy strategy;
45 val ExplorationStrategy strategy; 45
46 46 var long runtime = 0
47 var long runtime = 0 47 var long cachingTime = 0
48 var long cachingTime = 0 48 var int numberOfSolverCalls = 0
49 var int numberOfSolverCalls = 0 49 var int numberOfCachedSolverCalls = 0
50 var int numberOfCachedSolverCalls = 0 50
51 51 new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) {
52 new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { 52 this.method = method
53 this.method = method 53 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks
54 this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks 54 this.caching = caching
55 this.caching = caching 55 this.strategy = config.strategy
56 this.drealLocalPath = config.drealLocalPath 56 this.translator = new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout)
57 this.strategy = config.strategy 57 }
58 this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) 58
59 } 59 def createNumericTranslator(ViatraReasonerConfiguration config) {
60 60 val solverSelection = config.numericSolverSelection
61 def createNumericTranslator(ViatraReasonerConfiguration config) { 61 val strategy = config.strategy
62 val solverSelection = config.numericSolverSelection 62// if (strategy == ExplorationStrategy.None) {
63 val strategy = config.strategy 63 // initialise the specified
64 if (strategy == ExplorationStrategy.None) { 64 if (solverSelection == NumericSolverSelection.DREAL_DOCKER)
65 //initialise the specified 65 return new NumericDrealProblemSolver(true, null, config.numericSolverTimeout)
66 if (solverSelection == NumericSolverSelection.DREAL_DOCKER) 66 if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
67 return new NumericDrealProblemSolver(true, null, config.drealTimeout) 67 return new NumericDrealProblemSolver(false, config.drealLocalPath, config.numericSolverTimeout)
68 if (solverSelection == NumericSolverSelection.DREAL_LOCAL) 68 if (solverSelection == NumericSolverSelection.Z3) {
69 return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout) 69 // TODO THIS IS HARD-CODED for now
70 if (solverSelection == NumericSolverSelection.Z3) { 70// val root = "/data/viatra/VIATRA-Generator";
71 //TODO THIS IS HARD-CODED for now 71// val root = "/home/models/VIATRA-Generator";
72// val root = "/data/viatra/VIATRA-Generator"; 72 // END HARD-CODED
73 val root = "/home/models/VIATRA-Generator"; 73 // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
74 //END HARD-CODED 74// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
75 // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); 75// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
76 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); 76 // System.load("libz3.so");
77 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 77 // System.load("libz3java.so");
78 // System.load("libz3.so"); 78 return new NumericZ3ProblemSolver(config.numericSolverTimeout)
79 // System.load("libz3java.so"); 79// }
80 return new NumericZ3ProblemSolver(config.drealTimeout) 80 }
81 } 81// else {
82 } 82// //initialise both dreal-local and z3
83 else { 83//
84 //initialise both dreal-local and z3 84// //TODO THIS IS HARD-CODED for now
85 85//// val root = "/data/viatra/VIATRA-Generator";
86 //TODO THIS IS HARD-CODED for now 86// val root = "/home/models/VIATRA-Generator";
87// val root = "/data/viatra/VIATRA-Generator"; 87// //END HARD-CODED
88 val root = "/home/models/VIATRA-Generator"; 88//// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
89 //END HARD-CODED 89// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
90// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); 90// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
91 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); 91// return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout)
92 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 92// }
93 return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) 93 }
94 } 94
95 } 95 def init(ThreadContext context) {
96 96 // This makes the NumericSolver single-threaded,
97 def init(ThreadContext context) { 97 // but that's not a problem, because we only use the solver on a single thread anyways.
98 // This makes the NumericSolver single-threaded, 98 this.threadContext = context
99 // but that's not a problem, because we only use the solver on a single thread anyways. 99 val engine = threadContext.queryEngine
100 this.threadContext = context 100 for(entry : method.mustUnitPropagationPreconditions.entrySet) {
101 val engine = threadContext.queryEngine 101 val constraint = entry.key
102 for(entry : method.mustUnitPropagationPreconditions.entrySet) { 102 val querySpec = entry.value
103 val constraint = entry.key 103 val matcher = querySpec.getMatcher(engine);
104 val querySpec = entry.value 104 constraint2MustUnitPropagationPrecondition.put(constraint,matcher)
105 val matcher = querySpec.getMatcher(engine); 105 }
106 constraint2MustUnitPropagationPrecondition.put(constraint,matcher) 106 for(entry : method.currentUnitPropagationPreconditions.entrySet) {
107 } 107 val constraint = entry.key
108 for(entry : method.currentUnitPropagationPreconditions.entrySet) { 108 val querySpec = entry.value
109 val constraint = entry.key 109 val matcher = querySpec.getMatcher(engine);
110 val querySpec = entry.value 110 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
111 val matcher = querySpec.getMatcher(engine); 111 }
112 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) 112 }
113 } 113
114 } 114 def getRuntime(){runtime}
115 115 def getCachingTime(){cachingTime}
116 def getRuntime(){runtime} 116 def getNumberOfSolverCalls(){numberOfSolverCalls}
117 def getCachingTime(){cachingTime} 117 def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
118 def getNumberOfSolverCalls(){numberOfSolverCalls} 118 def getSolverFormingProblem(){this.translator.formingProblemTime}
119 def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} 119 def getSolverSolvingProblem(){this.translator.solvingProblemTime}
120 def getSolverFormingProblem(){this.t.formingProblemTime} 120 def getSolverSolution(){this.translator.formingSolutionTime}
121 def getSolverSolvingProblem(){this.t.solvingProblemTime} 121 def getNumericSolverSelection(){this.translator.numericSolver}
122 def getSolverSolution(){this.t.formingSolutionTime} 122
123 def getNumericSolverSelection(){this.t.numericSolver} 123 def boolean maySatisfiable() {
124 124 val int phase = determinePhase()
125 def boolean maySatisfiable() { 125
126 val int phase = determinePhase() 126 if(intermediateConsistencyCheck) {
127 127 return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase)
128 if(intermediateConsistencyCheck) { 128 } else {
129 return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) 129 return true
130 } else { 130 }
131 return true 131 }
132 } 132 def boolean currentSatisfiable() {
133 } 133 val int phase = determinePhase()
134 def boolean currentSatisfiable() { 134 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase)
135 val int phase = determinePhase() 135 }
136 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) 136
137 } 137 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) {
138 138 val start = System.nanoTime
139 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { 139 var boolean finalResult
140 val start = System.nanoTime 140 val boolean needsFilling = needsFilling
141 var boolean finalResult 141 val model = threadContext.getModel as PartialInterpretation
142 val boolean needsFilling = needsFilling 142 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
143 val model = threadContext.getModel as PartialInterpretation 143
144 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList 144 if(matches.empty){
145 145 finalResult=true
146 if(matches.empty){ 146 } else {
147 finalResult=true 147 val propagatedConstraints = new HashMap
148 } else { 148 //Filter constraints if there are phase-related restricutions
149 val propagatedConstraints = new HashMap 149 //null whitelist means accept everything
150 //Filter constraints if there are phase-related restricutions 150
151 //null whitelist means accept everything 151// println("<<<<START-STEP>>>> (" + phase + ")")
152 152 if (phase == -2) {
153// println("<<<<START-STEP>>>> (" + phase + ")") 153// println("Skipping numeric check")
154 if (phase == -2) { 154 //TODO Big assumption
155// println("Skipping numeric check") 155 return true
156 //TODO Big assumption 156 }
157 return true 157 val whitelist = getConstraintWhitelist(phase)
158 } 158 for(entry : matches.entrySet) {
159 val whitelist = getConstraintWhitelist(phase) 159 if (entry.value !== null){
160 for(entry : matches.entrySet) { 160 val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName
161 if (entry.value !== null){ 161 if (whitelist === null || whitelist.contains(name)) {
162 val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName 162// println(name)
163 if (whitelist === null || whitelist.contains(name)) { 163 val constraint = entry.key
164// println(name) 164// println("--match?-- " + constraint)
165 val constraint = entry.key 165 val allMatches = entry.value.allMatches.map[it.toArray]
166// println("--match?-- " + constraint) 166 // println("---------- " + entry.value.allMatches)
167 val allMatches = entry.value.allMatches.map[it.toArray] 167 propagatedConstraints.put(constraint,allMatches)
168 // println("---------- " + entry.value.allMatches) 168 }
169 propagatedConstraints.put(constraint,allMatches) 169 }
170 } 170 }
171 } 171 //check numeric problem
172 } 172 if(propagatedConstraints.values.forall[empty]) {
173 //check numeric problem 173 finalResult=true
174 if(propagatedConstraints.values.forall[empty]) { 174 } else {
175 finalResult=true 175 if(caching) {
176 } else { 176 val code = getCode(propagatedConstraints)
177 if(caching) { 177 val cachedResult = satisfiabilityCache.get(code)
178 val code = getCode(propagatedConstraints) 178 if(cachedResult === null) {
179 val cachedResult = satisfiabilityCache.get(code) 179 // println('''new problem, call solver''')
180 if(cachedResult === null) { 180 // for(entry : code.entrySet) {
181 // println('''new problem, call solver''') 181 // println('''«entry.key» -> «entry.value»''')
182 // for(entry : code.entrySet) { 182 // }
183 // println('''«entry.key» -> «entry.value»''') 183 //println(code.hashCode)
184 // } 184 this.numberOfSolverCalls++
185 //println(code.hashCode) 185 var boolean res = false
186 this.numberOfSolverCalls++ 186 if (needsFilling){
187 var boolean res = false 187 //TODO ASSUME Always True
188 if (needsFilling){ 188 //GET LIST OF VARS TO FILL
189 //TODO ASSUME Always True 189 val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
190 //GET LIST OF VARS TO FILL 190 if (fillMap === null) res = false
191 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
192 if (fillMap === null) res = false
193 else { 191 else {
194 fillWithPartialSolutionsDirectly(dataObjects, fillMap) 192 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
195 res = true 193 res = true
196 } 194 }
197 } else { 195 } else {
198 res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) 196 res = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
199 } 197 }
200 //TODO FIX CACHING 198 //TODO FIX CACHING
201 satisfiabilityCache.put(code,res) 199 satisfiabilityCache.put(code,res)
202 finalResult=res 200 finalResult=res
203 } else { 201 } else {
204 //println('''similar problem, answer from cache''') 202 //println('''similar problem, answer from cache''')
205 println('''potential issue, answer from cache''') 203 println('''potential issue, answer from cache''')
206 finalResult=cachedResult 204 finalResult=cachedResult
207 this.numberOfCachedSolverCalls++ 205 this.numberOfCachedSolverCalls++
208 } 206 }
209 } else { 207 } else {
210 if (needsFilling){ 208 if (needsFilling){
211 //GET LIST OF VARS TO FILL 209 //GET LIST OF VARS TO FILL
212 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) 210 val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
213 if (fillMap === null) finalResult = false 211 if (fillMap === null) finalResult = false
214 else { 212 else {
215 fillWithPartialSolutionsDirectly(dataObjects, fillMap) 213 fillWithPartialSolutionsDirectly(dataObjects, fillMap)
216 finalResult = true 214 finalResult = true
217 } 215 }
218 } else { 216 } else {
219 finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) 217 finalResult = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase))
220 } 218 }
221 this.numberOfSolverCalls++ 219 this.numberOfSolverCalls++
222 } 220 }
223 } 221 }
224 } 222 }
225 this.runtime+=System.nanoTime-start 223 this.runtime+=System.nanoTime-start
226 //STRATEGY 224 //STRATEGY
227 if (phase == 2) { 225 if (phase == 2) {
228 if (!finalResult) return finalResult 226 if (!finalResult) return finalResult
229 else { 227 else {
230 finalResult = isSatisfiable(matches, 3) 228 finalResult = isSatisfiable(matches, 3)
231 } 229 }
232 } 230 }
233 return finalResult 231 return finalResult
234 } 232 }
235 233
236 def selectSolver(int phase) { 234 def selectSolver(int phase) {
237 if (strategy === ExplorationStrategy.CrossingScenario){ 235 if (strategy === ExplorationStrategy.CrossingScenario){
238 if (phase == 1) return "z3" 236 if (phase == 1) return "z3"
239 else return "dreal" 237 else return "dreal"
240 } 238 }
241 return "irrelevant" 239 return "irrelevant"
242 } 240 }
243 241
244 def int determinePhase() { 242 def int determinePhase() {
245 // >= 0 : an actual phase 243 // >= 0 : an actual phase
246 // -1 : take all numeric constraints 244 // -1 : take all numeric constraints
247 // -2 : SKIP (take no numeric constraints) 245 // -2 : SKIP (take no numeric constraints)
248 if (strategy == ExplorationStrategy.CrossingScenario) { 246 if (strategy == ExplorationStrategy.CrossingScenario) {
249// //if has structural (non-WF) fitness issues, skip numeric handling 247// //if has structural (non-WF) fitness issues, skip numeric handling
250// val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) 248// val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0)
251// val compo = ob as ModelGenerationCompositeObjective 249// val compo = ob as ModelGenerationCompositeObjective
252// if (compo.getNonWFFitness(threadContext) > 0) { 250// if (compo.getNonWFFitness(threadContext) > 0) {
253// println("bootleg numeric-skip") 251// println("bootleg numeric-skip")
254// return -2; 252// return -2;
255// } 253// }
256 254
257 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors 255 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
258 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; 256 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
259 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); 257 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
260 var boolean foundBlockedBy = false; 258 var boolean foundBlockedBy = false;
261 259
262 var int numActors; 260 var int numActors;
263 var int numPlacedOn; 261 var int numPlacedOn;
264 var int numPlacements = 0; 262 var int numPlacements = 0;
265 263
266 for (PartialRelationInterpretation rel : relations) { 264 for (PartialRelationInterpretation rel : relations) {
267 if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { 265 if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) {
268 numActors = rel.relationlinks.size 266 numActors = rel.relationlinks.size
269 } 267 }
270 268
271 if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { 269 if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) {
272 numPlacedOn = rel.relationlinks.size 270 numPlacedOn = rel.relationlinks.size
273 } 271 }
274 272
275 if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { 273 if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) {
276 for (RelationLink link : rel.getRelationlinks()) { 274 for (RelationLink link : rel.getRelationlinks()) {
277 val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; 275 val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement;
278 if (param2.isValueSet()) { 276 if (param2.isValueSet()) {
279 numPlacements++ 277 numPlacements++
280 } 278 }
281 } 279 }
282 } 280 }
283 281
284 if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { 282 if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) {
285 if (!rel.getRelationlinks().isEmpty()) { 283 if (!rel.getRelationlinks().isEmpty()) {
286 foundBlockedBy = true 284 foundBlockedBy = true
287 } 285 }
288 } 286 }
289 } 287 }
290 val boolean unplacedActorExists = numPlacements < numActors 288 val boolean unplacedActorExists = numPlacements < numActors
291 //it means that there is no blockedBy 289 //it means that there is no blockedBy
292 //so we are at most at phase 2 290 //so we are at most at phase 2
293 if (numPlacedOn == 1 && numPlacements == 0) return 1 291 if (numPlacedOn == 1 && numPlacements == 0) return 1
294 if (foundBlockedBy && unplacedActorExists) return 2 292 if (foundBlockedBy && unplacedActorExists) return 2
295 if (numPlacements == numActors) return 3; 293 if (numPlacements == numActors) return 3;
296 return -2; 294 return -2;
297 } 295 }
298 return -1; 296 return -1;
299 } 297 }
300 298
301 def getConstraintWhitelist(int phase) { 299 def getConstraintWhitelist(int phase) {
302 val List<String> wl = newArrayList 300 val List<String> wl = newArrayList
303 //null return means accept everything 301 //null return means accept everything
304 if (strategy === ExplorationStrategy.None){ 302 if (strategy === ExplorationStrategy.None){
305 return null 303 return null
306 } else if (strategy === ExplorationStrategy.CrossingScenario){ 304 } else if (strategy === ExplorationStrategy.CrossingScenario){
307 /* 305 /*
308 "define_placedOn_actorOnVerticalLane", 306 "define_placedOn_actorOnVerticalLane",
309 "define_placedOn_actorOnHorizLane", 307 "define_placedOn_actorOnHorizLane",
310 308
311 "define_actor_maxXp", 309 "define_actor_maxXp",
312 "define_actor_minXp", 310 "define_actor_minXp",
313 "define_actor_maxYp", 311 "define_actor_maxYp",
314 "define_actor_minYp", 312 "define_actor_minYp",
315 313
316 "define_actor_wrtLane", 314 "define_actor_wrtLane",
317 315
318 "define_actor_minimumDistance", 316 "define_actor_minimumDistance",
319 317
320 "define_actor_actorOnVertLaneHasxSpeed0", 318 "define_actor_actorOnVertLaneHasxSpeed0",
321 "define_actor_actorOnVertLaneMinYs", 319 "define_actor_actorOnVertLaneMinYs",
322 "define_actor_actorOnVertLaneMaxYs", 320 "define_actor_actorOnVertLaneMaxYs",
323 "define_actor_actorOnHorizLaneHasySpeed0", 321 "define_actor_actorOnHorizLaneHasySpeed0",
324 "define_actor_actorOnHorizLaneMinXs", 322 "define_actor_actorOnHorizLaneMinXs",
325 "define_actor_actorOnHorizLaneMaxXs", 323 "define_actor_actorOnHorizLaneMaxXs",
326 324
327 "define_actor_pedestrianWidth", 325 "define_actor_pedestrianWidth",
328 "define_actor_pedestrianLength", 326 "define_actor_pedestrianLength",
329 "define_actor_vehicleWidth", 327 "define_actor_vehicleWidth",
330 "define_actor_vehicleWidth", 328 "define_actor_vehicleWidth",
331 "define_actor_vehicleLength", 329 "define_actor_vehicleLength",
332 "define_actor_vehicleLength", 330 "define_actor_vehicleLength",
333 331
334 "collisionExists_timeWithinBound", 332 "collisionExists_timeWithinBound",
335 "collisionExists_timeNotNegative", 333 "collisionExists_timeNotNegative",
336 "collisionExists_defineCollision_y1", 334 "collisionExists_defineCollision_y1",
337 "collisionExists_defineCollision_y2", 335 "collisionExists_defineCollision_y2",
338 "collisionExists_defineCollision_x1", 336 "collisionExists_defineCollision_x1",
339 "collisionExists_defineCollision_x2", 337 "collisionExists_defineCollision_x2",
340 338
341 "visionBlocked_ites_notOnSameVertLine", 339 "visionBlocked_ites_notOnSameVertLine",
342 "visionBlocked_ites_top", 340 "visionBlocked_ites_top",
343 "visionBlocked_ites_bottom", 341 "visionBlocked_ites_bottom",
344 "visionBlocked_xdistBSlargerThanxdistTS", 342 "visionBlocked_xdistBSlargerThanxdistTS",
345 "visionBlocked_xdistBTlargerThanxdistST", 343 "visionBlocked_xdistBTlargerThanxdistST",
346 "visionBlocked_ydistBSlargerThanydistTS", 344 "visionBlocked_ydistBSlargerThanydistTS",
347 "visionBlocked_ydistBTlargerThanydistST" 345 "visionBlocked_ydistBTlargerThanydistST"
348 */ 346 */
349 347
350 //HINTS: 348 //HINTS:
351 //define_actor_wrtLane 349 //define_actor_wrtLane
352 //28.5 is structural hint 350 //28.5 is structural hint
353 switch (phase) { 351 switch (phase) {
354 case 1: { 352 case 1: {
355 wl.addAll(#[ 353 wl.addAll(#[
356 "define_placedOn_actorOnVerticalLane", 354 "define_placedOn_actorOnVerticalLane",
357 "define_placedOn_actorOnHorizLane", 355 "define_placedOn_actorOnHorizLane",
358 356
359 "define_actor_maxXp", 357 "define_actor_maxXp",
360 "define_actor_minXp", 358 "define_actor_minXp",
361 "define_actor_maxYp", 359 "define_actor_maxYp",
362 "define_actor_minYp", 360 "define_actor_minYp",
363 361
364 "define_actor_pedestrianWidth", 362 "define_actor_pedestrianWidth",
365 "define_actor_pedestrianLength", 363 "define_actor_pedestrianLength",
366 "define_actor_vehicleWidth", 364 "define_actor_vehicleWidth",
367 "define_actor_vehicleWidth", 365 "define_actor_vehicleWidth",
368 "define_actor_vehicleLength", 366 "define_actor_vehicleLength",
369 "define_actor_vehicleLength" 367 "define_actor_vehicleLength"
370 368
371 ]) 369 ])
372 } 370 }
373 case 2: { 371 case 2: {
374 wl.addAll(#[ 372 wl.addAll(#[
375 373
376 "define_placedOn_actorOnVerticalLane", 374 "define_placedOn_actorOnVerticalLane",
377 "define_placedOn_actorOnHorizLane", 375 "define_placedOn_actorOnHorizLane",
378 376
379 "define_actor_maxXp", 377 "define_actor_maxXp",
380 "define_actor_minXp", 378 "define_actor_minXp",
381 "define_actor_maxYp", 379 "define_actor_maxYp",
382 "define_actor_minYp", 380 "define_actor_minYp",
383 381
384 "define_actor_minimumDistance", 382 "define_actor_minimumDistance",
385 383
386 "define_actor_pedestrianWidth", 384 "define_actor_pedestrianWidth",
387 "define_actor_pedestrianLength", 385 "define_actor_pedestrianLength",
388 "define_actor_vehicleWidth", 386 "define_actor_vehicleWidth",
389 "define_actor_vehicleWidth", 387 "define_actor_vehicleWidth",
390 "define_actor_vehicleLength", 388 "define_actor_vehicleLength",
391 "define_actor_vehicleLength", 389 "define_actor_vehicleLength",
392 390
393 "visionBlocked_ites_notOnSameVertLine", 391 "visionBlocked_ites_notOnSameVertLine",
394 "visionBlocked_ites_top", 392 "visionBlocked_ites_top",
395 "visionBlocked_ites_bottom", 393 "visionBlocked_ites_bottom",
396 "visionBlocked_xdistBSlargerThanxdistTS", 394 "visionBlocked_xdistBSlargerThanxdistTS",
397 "visionBlocked_xdistBTlargerThanxdistST", 395 "visionBlocked_xdistBTlargerThanxdistST",
398 "visionBlocked_ydistBSlargerThanydistTS", 396 "visionBlocked_ydistBSlargerThanydistTS",
399 "visionBlocked_ydistBTlargerThanydistST" 397 "visionBlocked_ydistBTlargerThanydistST"
400 ]) 398 ])
401 } 399 }
402 case 3: { 400 case 3: {
403 wl.addAll(#[ 401 wl.addAll(#[
404 402
405 "define_placedOn_actorOnVerticalLane", 403 "define_placedOn_actorOnVerticalLane",
406 "define_placedOn_actorOnHorizLane", 404 "define_placedOn_actorOnHorizLane",
407 405
408 "define_actor_maxXp", 406 "define_actor_maxXp",
409 "define_actor_minXp", 407 "define_actor_minXp",
410 "define_actor_maxYp", 408 "define_actor_maxYp",
411 "define_actor_minYp", 409 "define_actor_minYp",
412 410
413 "define_actor_minimumDistance", 411 "define_actor_minimumDistance",
414 412
415 "define_actor_actorOnVertLaneHasxSpeed0", 413 "define_actor_actorOnVertLaneHasxSpeed0",
416 "define_actor_actorOnVertLaneMinYs", 414 "define_actor_actorOnVertLaneMinYs",
417 "define_actor_actorOnVertLaneMaxYs", 415 "define_actor_actorOnVertLaneMaxYs",
418 "define_actor_actorOnHorizLaneHasySpeed0", 416 "define_actor_actorOnHorizLaneHasySpeed0",
419 "define_actor_actorOnHorizLaneMinXs", 417 "define_actor_actorOnHorizLaneMinXs",
420 "define_actor_actorOnHorizLaneMaxXs", 418 "define_actor_actorOnHorizLaneMaxXs",
421 419
422 "define_actor_pedestrianWidth", 420 "define_actor_pedestrianWidth",
423 "define_actor_pedestrianLength", 421 "define_actor_pedestrianLength",
424 "define_actor_vehicleWidth", 422 "define_actor_vehicleWidth",
425 "define_actor_vehicleWidth", 423 "define_actor_vehicleWidth",
426 "define_actor_vehicleLength", 424 "define_actor_vehicleLength",
427 "define_actor_vehicleLength", 425 "define_actor_vehicleLength",
428 426
429 "collisionExists_timeWithinBound", 427 "collisionExists_timeWithinBound",
430 "collisionExists_timeNotNegative", 428 "collisionExists_timeNotNegative",
431 "collisionExists_defineCollision_y1", 429 "collisionExists_defineCollision_y1",
432 "collisionExists_defineCollision_y2", 430 "collisionExists_defineCollision_y2",
433 "collisionExists_defineCollision_x1", 431 "collisionExists_defineCollision_x1",
434 "collisionExists_defineCollision_x2" 432 "collisionExists_defineCollision_x2"
435 ]) 433 ])
436 } 434 }
437 default: { 435 default: {
438 //this is for 3 if we implement 4 436 //this is for 3 if we implement 4
439// bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) 437// bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7])
440 438
441 //this is for 4 if we do it 439 //this is for 4 if we do it
442 wl.addAll(#[]) 440 wl.addAll(#[])
443 return null 441 return null
444 } 442 }
445 } 443 }
446 } 444 }
447 return wl 445 return wl
448 } 446 }
449 447
450 def getNeedsFilling(){ 448 def getNeedsFilling(){
451 if (strategy == ExplorationStrategy.CrossingScenario) return true 449 if (strategy == ExplorationStrategy.CrossingScenario) return true
452 return false 450 return false
453 } 451 }
454 452
455 def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { 453 def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
456 val start = System.nanoTime 454 val start = System.nanoTime
457 val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList 455 val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
458 val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) 456 val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]])
459 this.cachingTime += System.nanoTime-start 457 this.cachingTime += System.nanoTime-start
460 return res 458 return res
461 } 459 }
462 460
463 def fillSolutionCopy(Map<EObject, EObject> trace) { 461 def fillSolutionCopy(Map<EObject, EObject> trace) {
464 //No need to do a final check to fill if we are using a strategy 462 //No need to do a final check to fill if we are using a strategy
465 if (strategy === ExplorationStrategy.CrossingScenario) return 463 if (strategy === ExplorationStrategy.CrossingScenario) return
466 val model = threadContext.getModel as PartialInterpretation 464 val model = threadContext.getModel as PartialInterpretation
467 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList 465 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
468 if(constraint2CurrentUnitPropagationPrecondition.empty) { 466 if(constraint2CurrentUnitPropagationPrecondition.empty) {
469 fillWithDefaultValues(dataObjects,trace) 467 fillWithDefaultValues(dataObjects,trace)
470 } else { 468 } else {
471 val propagatedConstraints = new HashMap 469 val propagatedConstraints = new HashMap
472 for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { 470 for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {
473 val constraint = entry.key 471 val constraint = entry.key
474 val allMatches = entry.value.allMatches.map[it.toArray] 472 val allMatches = entry.value.allMatches.map[it.toArray]
475 propagatedConstraints.put(constraint,allMatches) 473 propagatedConstraints.put(constraint,allMatches)
476 } 474 }
477 475
478 if(propagatedConstraints.values.forall[empty]) { 476 if(propagatedConstraints.values.forall[empty]) {
479 fillWithDefaultValues(dataObjects,trace) 477 fillWithDefaultValues(dataObjects,trace)
480 } else { 478 } else {
481 val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") 479 val solution = translator.delegateGetSolution(dataObjects,propagatedConstraints, "dreal")
482 fillWithSolutions(dataObjects,solution,trace) 480 fillWithSolutions(dataObjects,solution,trace)
483 } 481 }
484 } 482 }
485 } 483 }
486 484
487 def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { 485 def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
488 for(element : elements) { 486 for(element : elements) {
489 if(element.valueSet==false) { 487 if(element.valueSet==false) {
490 val value = getDefaultValue(element) 488 val value = getDefaultValue(element)
491 val target = trace.get(element) as PrimitiveElement 489 val target = trace.get(element) as PrimitiveElement
492 target.fillWithValue(value) 490 target.fillWithValue(value)
493 } 491 }
494 } 492 }
495 } 493 }
496 494
497 def protected dispatch getDefaultValue(BooleanElement e) {false} 495 def protected dispatch getDefaultValue(BooleanElement e) {false}
498 def protected dispatch getDefaultValue(IntegerElement e) {0} 496 def protected dispatch getDefaultValue(IntegerElement e) {0}
499 def protected dispatch getDefaultValue(RealElement e) {0.0} 497 def protected dispatch getDefaultValue(RealElement e) {0.0}
500 def protected dispatch getDefaultValue(StringElement e) {""} 498 def protected dispatch getDefaultValue(StringElement e) {""}
501 499
502 def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { 500 def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) {
503 for(element : elements) { 501 for(element : elements) {
504 if(element.valueSet==false) { 502 if(element.valueSet==false) {
505 if(solution.containsKey(element)) { 503 if(solution.containsKey(element)) {
506 val value = solution.get(element) 504 val value = solution.get(element)
507 val target = trace.get(element) as PrimitiveElement 505 val target = trace.get(element) as PrimitiveElement
508 target.fillWithValue(value) 506 target.fillWithValue(value)
509 } else { 507 } else {
510 val target = trace.get(element) as PrimitiveElement 508 val target = trace.get(element) as PrimitiveElement
511 target.fillWithValue(target.defaultValue) 509 target.fillWithValue(target.defaultValue)
512 } 510 }
513 } 511 }
514 } 512 }
515 } 513 }
516 514
517 def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} 515 def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
518 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} 516 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
519 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } 517 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double }
520 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} 518 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
521 519
522 def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { 520 def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) {
523 for(element : elements) { 521 for(element : elements) {
524 //we allow overwriting of already set variables 522 //we allow overwriting of already set variables
525 if(solution.containsKey(element)) { 523 if(solution.containsKey(element)) {
526 val value = solution.get(element) 524 val value = solution.get(element)
527 if (value !== null){ 525 if (value !== null){
528 element.fillWithValue(value) 526 element.fillWithValue(value)
529 } 527 }
530 } 528 }
531 } 529 }
532 } 530 }
533} \ No newline at end of file 531} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
index 4484052d..0c170c2f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -222,4 +222,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
222 } 222 }
223 builder 223 builder
224 } 224 }
225} 225}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
index 33b69436..7c30bbb5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -28,7 +28,7 @@ class CopiedSolution {
28class SolutionCopier { 28class SolutionCopier {
29 val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> 29 val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
30 30
31 @Accessors NumericSolver numericSolver 31 @Accessors NumericRefinementUnit numericSolver
32 long startTime = System.nanoTime 32 long startTime = System.nanoTime
33 @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 33 @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
34 34
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
index e00f76ff..ac29c4ce 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -33,7 +33,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro
33 val ObjectiveComparatorHelper comparatorHelper 33 val ObjectiveComparatorHelper comparatorHelper
34 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap 34 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
35 35
36 @Accessors var NumericSolver numericSolver 36 @Accessors var NumericRefinementUnit numericSolver
37 @Accessors var Map<Object, Solution> solutionsCollection 37 @Accessors var Map<Object, Solution> solutionsCollection
38 38
39 new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { 39 new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
@@ -45,7 +45,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro
45 this.solutionCopier = new SolutionCopier 45 this.solutionCopier = new SolutionCopier
46 } 46 }
47 47
48 def setNumericSolver(NumericSolver numericSolver) { 48 def setNumericSolver(NumericRefinementUnit numericSolver) {
49 this.numericSolver = numericSolver 49 this.numericSolver = numericSolver
50 solutionCopier.numericSolver = numericSolver 50 solutionCopier.numericSolver = numericSolver
51 } 51 }
@@ -63,7 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro
63 if (!shouldSaveSolution(fitness, context)) { 63 if (!shouldSaveSolution(fitness, context)) {
64 return false 64 return false
65 } 65 }
66 println("Found: " + fitness) 66 //println("Found: " + fitness)
67 val dominatedTrajectories = newArrayList 67 val dominatedTrajectories = newArrayList
68 for (entry : trajectories.entrySet) { 68 for (entry : trajectories.entrySet) {
69 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) 69 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
index 6e0abd0b..5448d61a 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java
@@ -212,7 +212,7 @@ public class SolutionStore {
212 unsavedSolutionCallbacks(context, solutionTrajectory); 212 unsavedSolutionCallbacks(context, solutionTrajectory);
213 return; 213 return;
214 } 214 }
215 System.out.println("SAVING SOLUTION"); 215// System.out.println("SAVING SOLUTION");
216 boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory); 216 boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory);
217 217
218 if (solutionSaved) { 218 if (solutionSaved) {
generated by cgit v1.2.3-54-g00ecf (git 2.44.0) at 2024-05-02 07:42:58 +0000