diff options
author | anqili426 <mollisterkl@outlook.com> | 2020-04-15 01:24:14 -0400 |
---|---|---|
committer | anqili426 <mollisterkl@outlook.com> | 2020-04-15 01:24:14 -0400 |
commit | d8f9e9d3863255f367caa3098a4fd7c87f81b841 (patch) | |
tree | 98d9a72b195ec77233b8a0731fe1db90388ac4ee /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | Updated logic that creates a numeric problem using matches (diff) | |
download | VIATRA-Generator-d8f9e9d3863255f367caa3098a4fd7c87f81b841.tar.gz VIATRA-Generator-d8f9e9d3863255f367caa3098a4fd7c87f81b841.tar.zst VIATRA-Generator-d8f9e9d3863255f367caa3098a4fd7c87f81b841.zip |
Added logic to get a solution
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 23 |
1 files changed, 13 insertions, 10 deletions
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 834cc2f0..b9532c46 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 | |||
@@ -16,8 +16,10 @@ import com.microsoft.z3.BoolExpr; | |||
16 | import com.microsoft.z3.Context; | 16 | import com.microsoft.z3.Context; |
17 | import com.microsoft.z3.Expr; | 17 | import com.microsoft.z3.Expr; |
18 | import com.microsoft.z3.IntExpr; | 18 | import com.microsoft.z3.IntExpr; |
19 | import com.microsoft.z3.Model; | ||
19 | import com.microsoft.z3.Solver; | 20 | import com.microsoft.z3.Solver; |
20 | import com.microsoft.z3.Status; | 21 | import com.microsoft.z3.Status; |
22 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | ||
21 | 23 | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
@@ -42,14 +44,15 @@ public class NumericProblemSolver { | |||
42 | 44 | ||
43 | private Context ctx; | 45 | private Context ctx; |
44 | private Solver s; | 46 | private Solver s; |
45 | private Map<XExpression, Map<Object, Expr>> bindings; | 47 | private Map<Object, Expr> varMap; |
46 | 48 | ||
47 | public NumericProblemSolver() { | 49 | public NumericProblemSolver() { |
48 | HashMap<String, String> cfg = new HashMap<String, String>(); | 50 | HashMap<String, String> cfg = new HashMap<String, String>(); |
49 | cfg.put("model", "true"); | 51 | cfg.put("model", "true"); |
50 | ctx = new Context(cfg); | 52 | ctx = new Context(cfg); |
53 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); | ||
51 | s = ctx.mkSolver(); | 54 | s = ctx.mkSolver(); |
52 | bindings = new HashMap<XExpression, Map<Object, Expr>>(); | 55 | varMap = new HashMap<Object, Expr>(); |
53 | } | 56 | } |
54 | 57 | ||
55 | public Context getNumericProblemContext() { | 58 | public Context getNumericProblemContext() { |
@@ -80,7 +83,13 @@ public class NumericProblemSolver { | |||
80 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 83 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
81 | s.add(problemInstance); | 84 | s.add(problemInstance); |
82 | if (s.check() == Status.SATISFIABLE) { | 85 | if (s.check() == Status.SATISFIABLE) { |
83 | //TODO: Form the solution here | 86 | Model m = s.getModel(); |
87 | Set<Object> allObj = varMap.keySet(); | ||
88 | for (Object o: allObj) { | ||
89 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | ||
90 | Integer oSol = Integer.parseInt(val.toString()); | ||
91 | sol.put(o, oSol); | ||
92 | } | ||
84 | } | 93 | } |
85 | return sol; | 94 | return sol; |
86 | } | 95 | } |
@@ -117,6 +126,7 @@ public class NumericProblemSolver { | |||
117 | throw new Exception ("Unsupported binary operation " + name); | 126 | throw new Exception ("Unsupported binary operation " + name); |
118 | } | 127 | } |
119 | 128 | ||
129 | System.out.println(constraint.toString()); | ||
120 | return constraint; | 130 | return constraint; |
121 | } | 131 | } |
122 | 132 | ||
@@ -181,13 +191,6 @@ public class NumericProblemSolver { | |||
181 | BoolExpr constraintInstances = ctx.mkTrue(); | 191 | BoolExpr constraintInstances = ctx.mkTrue(); |
182 | for (XExpression e: matches.keySet()) { | 192 | for (XExpression e: matches.keySet()) { |
183 | Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 193 | Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
184 | Map<Object, Expr> varMap = bindings.get(e); | ||
185 | |||
186 | if (varMap == null) { | ||
187 | varMap = new HashMap<Object, Expr>(); | ||
188 | bindings.put(e, varMap); | ||
189 | } | ||
190 | |||
191 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 194 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
192 | BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); | 195 | BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); |
193 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); | 196 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); |