diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu')
2 files changed, 12 insertions, 4 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index b9942a17..1b68fed2 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | |||
@@ -17,7 +17,8 @@ class ExpressionEvaluation2Logic { | |||
17 | var NumericProblemSolver _numericSolver = null //new NumericProblemSolver | 17 | var NumericProblemSolver _numericSolver = null //new NumericProblemSolver |
18 | def getNumericSolver() { | 18 | def getNumericSolver() { |
19 | if(_numericSolver === null) { | 19 | if(_numericSolver === null) { |
20 | _numericSolver = (new NumericTranslator).selectProblemSolver | 20 | // it seems like this getter has no use |
21 | _numericSolver = (new NumericTranslator(null)).selectProblemSolver | ||
21 | } | 22 | } |
22 | return _numericSolver | 23 | return _numericSolver |
23 | } | 24 | } |
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 22ea41bf..3d3f2f4a 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 | |||
@@ -16,7 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall | |||
16 | class NumericTranslator { | 16 | class NumericTranslator { |
17 | 17 | ||
18 | private XExpressionExtractor extractor = new XExpressionExtractor(); | 18 | private XExpressionExtractor extractor = new XExpressionExtractor(); |
19 | private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver(); | 19 | private NumericProblemSolver numericSolver; |
20 | 20 | ||
21 | long formingProblemTime=0; | 21 | long formingProblemTime=0; |
22 | long solvingProblemTime=0; | 22 | long solvingProblemTime=0; |
@@ -28,6 +28,11 @@ class NumericTranslator { | |||
28 | o1.simpleName.compareTo(o2.simpleName) | 28 | o1.simpleName.compareTo(o2.simpleName) |
29 | } | 29 | } |
30 | } | 30 | } |
31 | |||
32 | new(NumericProblemSolver numericProblemSolver){ | ||
33 | this.numericSolver = numericProblemSolver | ||
34 | } | ||
35 | |||
31 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { | 36 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { |
32 | val res = new HashMap | 37 | val res = new HashMap |
33 | for(var i=0; i<tuple.length; i++) { | 38 | for(var i=0; i<tuple.length; i++) { |
@@ -53,7 +58,9 @@ class NumericTranslator { | |||
53 | 58 | ||
54 | def NumericProblemSolver selectProblemSolver() { | 59 | def NumericProblemSolver selectProblemSolver() { |
55 | // return new NumericProblemSolver | 60 | // return new NumericProblemSolver |
56 | return drealSolver; | 61 | // add numeric solver decision procedure here |
62 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | ||
63 | return numericSolver; | ||
57 | } | 64 | } |
58 | 65 | ||
59 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 66 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
@@ -81,5 +88,5 @@ class NumericTranslator { | |||
81 | def getFormingProblemTime() {formingProblemTime} | 88 | def getFormingProblemTime() {formingProblemTime} |
82 | def getSolvingProblemTime() {solvingProblemTime} | 89 | def getSolvingProblemTime() {solvingProblemTime} |
83 | def getFormingSolutionTime() {formingSolutionTime} | 90 | def getFormingSolutionTime() {formingSolutionTime} |
84 | def getDrealSolver(){return drealSolver} | 91 | def getNumericSolver(){numericSolver} |
85 | } \ No newline at end of file | 92 | } \ No newline at end of file |