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 | 19 |
1 files changed, 12 insertions, 7 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 3d3f2f4a..791dd644 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 | |||
| @@ -56,24 +56,29 @@ class NumericTranslator { | |||
| 56 | return res | 56 | return res |
| 57 | } | 57 | } |
| 58 | 58 | ||
| 59 | def NumericProblemSolver selectProblemSolver() { | 59 | def NumericProblemSolver selectProblemSolver(String selection) { |
| 60 | // return new NumericProblemSolver | 60 | // return new NumericProblemSolver |
| 61 | // add numeric solver decision procedure here | 61 | // add numeric solver decision procedure here |
| 62 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | 62 | if (numericSolver instanceof NumericDynamicProblemSolver) { |
| 63 | return numericSolver; | 63 | val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver |
| 64 | return dynamicSolver.selectSolver(selection); | ||
| 65 | } else{ | ||
| 66 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | ||
| 67 | return numericSolver; | ||
| 68 | } | ||
| 64 | } | 69 | } |
| 65 | 70 | ||
| 66 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 71 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) { |
| 67 | val input = formNumericProblemInstance(matches) | 72 | val input = formNumericProblemInstance(matches) |
| 68 | val solver = selectProblemSolver | 73 | val solver = selectProblemSolver(select) |
| 69 | val satisfiability = solver.isSatisfiable(input) | 74 | val satisfiability = solver.isSatisfiable(input) |
| 70 | solver.updateTimes | 75 | solver.updateTimes |
| 71 | return satisfiability | 76 | return satisfiability |
| 72 | } | 77 | } |
| 73 | 78 | ||
| 74 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { | 79 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) { |
| 75 | val input = formNumericProblemInstance(matches) | 80 | val input = formNumericProblemInstance(matches) |
| 76 | val solver = selectProblemSolver | 81 | val solver = selectProblemSolver(select) |
| 77 | val solution = solver.getOneSolution(primitiveElements,input) | 82 | val solution = solver.getOneSolution(primitiveElements,input) |
| 78 | solver.updateTimes | 83 | solver.updateTimes |
| 79 | return solution | 84 | return solution |