diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | 11 |
1 files changed, 8 insertions, 3 deletions
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 b9eda7b3..21fbe589 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 | |||
@@ -50,9 +50,14 @@ class NumericTranslator { | |||
50 | return res | 50 | return res |
51 | } | 51 | } |
52 | 52 | ||
53 | def selectProblemSolver() { | ||
54 | // return new NumericProblemSolver | ||
55 | return new DrealProblemSolver | ||
56 | } | ||
57 | |||
53 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 58 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
54 | val input = formNumericProblemInstance(matches) | 59 | val input = formNumericProblemInstance(matches) |
55 | val solver = new NumericProblemSolver | 60 | val solver = selectProblemSolver |
56 | val satisfiability = solver.isSatisfiable(input) | 61 | val satisfiability = solver.isSatisfiable(input) |
57 | solver.updateTimes | 62 | solver.updateTimes |
58 | return satisfiability | 63 | return satisfiability |
@@ -60,13 +65,13 @@ class NumericTranslator { | |||
60 | 65 | ||
61 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { | 66 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { |
62 | val input = formNumericProblemInstance(matches) | 67 | val input = formNumericProblemInstance(matches) |
63 | val solver = new NumericProblemSolver | 68 | val solver = selectProblemSolver |
64 | val solution = solver.getOneSolution(primitiveElements,input) | 69 | val solution = solver.getOneSolution(primitiveElements,input) |
65 | solver.updateTimes | 70 | solver.updateTimes |
66 | return solution | 71 | return solution |
67 | } | 72 | } |
68 | 73 | ||
69 | private def updateTimes(NumericProblemSolver s) { | 74 | private def updateTimes(DrealProblemSolver s) { |
70 | this.formingProblemTime += s.getEndformingProblem | 75 | this.formingProblemTime += s.getEndformingProblem |
71 | this.solvingProblemTime += s.getEndSolvingProblem | 76 | this.solvingProblemTime += s.getEndSolvingProblem |
72 | this.formingSolutionTime += s.getEndFormingSolution | 77 | this.formingSolutionTime += s.getEndFormingSolution |