diff options
author | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-10 18:37:15 +0200 |
---|---|---|
committer | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-10 18:37:15 +0200 |
commit | 63b95a0b1f9c82e2d07fcee7284cbe138ec0f89a (patch) | |
tree | 5f7627c226298de06600186c40b6c30137496ae2 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | postprocessing time ns->ms (diff) | |
download | VIATRA-Generator-63b95a0b1f9c82e2d07fcee7284cbe138ec0f89a.tar.gz VIATRA-Generator-63b95a0b1f9c82e2d07fcee7284cbe138ec0f89a.tar.zst VIATRA-Generator-63b95a0b1f9c82e2d07fcee7284cbe138ec0f89a.zip |
closing numerical solver
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 | 6 |
1 files changed, 4 insertions, 2 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 0e6e824c..8749a5a8 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 | |||
@@ -90,7 +90,9 @@ public class NumericProblemSolver { | |||
90 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 90 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
91 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 91 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
92 | s.add(problemInstance); | 92 | s.add(problemInstance); |
93 | return s.check() == Status.SATISFIABLE; | 93 | boolean result = (s.check() == Status.SATISFIABLE); |
94 | this.ctx.close(); | ||
95 | return result; | ||
94 | } | 96 | } |
95 | 97 | ||
96 | public Map<PrimitiveElement,Integer> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 98 | public Map<PrimitiveElement,Integer> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
@@ -121,7 +123,7 @@ public class NumericProblemSolver { | |||
121 | } else { | 123 | } else { |
122 | System.out.println("Unsatisfiable"); | 124 | System.out.println("Unsatisfiable"); |
123 | } | 125 | } |
124 | 126 | this.ctx.close(); | |
125 | return sol; | 127 | return sol; |
126 | } | 128 | } |
127 | 129 | ||