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 |