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