diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-17 03:13:47 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-17 03:13:47 -0500 |
commit | 6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f (patch) | |
tree | 2fcb033ee2cf34506b9550a9939c421babfae7dd /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | complete queries for lane structure (diff) | |
download | VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.tar.gz VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.tar.zst VIATRA-Generator-6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f.zip |
add some actor-related queries, solve minor Z3 issue
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index db33804e..0b093859 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |||
@@ -4,6 +4,8 @@ import java.util.ArrayList; | |||
4 | import java.util.HashMap; | 4 | import java.util.HashMap; |
5 | import java.util.List; | 5 | import java.util.List; |
6 | import java.util.Map; | 6 | import java.util.Map; |
7 | import java.util.regex.Matcher; | ||
8 | import java.util.regex.Pattern; | ||
7 | 9 | ||
8 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 10 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
9 | import org.eclipse.xtext.xbase.XBinaryOperation; | 11 | import org.eclipse.xtext.xbase.XBinaryOperation; |
@@ -98,7 +100,21 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
98 | sol.put(o, oSol); | 100 | sol.put(o, oSol); |
99 | } else { | 101 | } else { |
100 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | 102 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); |
101 | Double oSol = Double.parseDouble(val.toString()); | 103 | Double oSol = 0.0; |
104 | if (val.toString().contains("/")) { | ||
105 | String re = "([0-9]+)/([0-9]+)"; | ||
106 | Pattern p = Pattern.compile(re); | ||
107 | Matcher ma = p.matcher(val.toString()); | ||
108 | if (ma.matches()) { | ||
109 | int numerator = Integer.parseInt(ma.group(1)); | ||
110 | int denominator = Integer.parseInt(ma.group(2)); | ||
111 | oSol = (double) numerator / denominator; | ||
112 | } else { | ||
113 | System.err.println("Problem converting string: " + val.toString()); | ||
114 | } | ||
115 | } else { | ||
116 | oSol = Double.parseDouble(val.toString()); | ||
117 | } | ||
102 | sol.put(o, oSol); | 118 | sol.put(o, oSol); |
103 | } | 119 | } |
104 | //System.out.println("Solution:" + o + "->" + oSol); | 120 | //System.out.println("Solution:" + o + "->" + oSol); |