diff options
author | 2021-07-30 10:04:27 +0200 | |
---|---|---|
committer | 2021-07-30 10:04:27 +0200 | |
commit | aaa67b0ef8840d97b062a4f1383bf93410984af3 (patch) | |
tree | 2c07208bb6b5ab27b47bd477dfbcc6e77b50d623 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | |
parent | Config updated and createSharedVersionedMapStores service (diff) | |
download | VIATRA-Generator-V4transformation.tar.gz VIATRA-Generator-V4transformation.tar.zst VIATRA-Generator-V4transformation.zip |
Numeric solver dreal hardcoding -> configV4transformation
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 | ||