diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-14 03:27:43 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-14 03:27:43 -0500 |
commit | 6dfdda9b3a6764cf5e4b5fc4303a49bb80193c5a (patch) | |
tree | 7e014ca5f436110525329b2b745416e026066e49 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |
parent | add numericProblemSolver supertype (diff) | |
download | VIATRA-Generator-6dfdda9b3a6764cf5e4b5fc4303a49bb80193c5a.tar.gz VIATRA-Generator-6dfdda9b3a6764cf5e4b5fc4303a49bb80193c5a.tar.zst VIATRA-Generator-6dfdda9b3a6764cf5e4b5fc4303a49bb80193c5a.zip |
implement isSatisfiable with Dreal integration
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 16 |
1 files changed, 0 insertions, 16 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 a594eb60..ab7f6ddc 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 | |||
@@ -28,22 +28,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
28 | 28 | ||
29 | 29 | ||
30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ | 30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ |
31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
32 | private static final String N_PLUS = "operator_plus"; | ||
33 | private static final String N_MINUS = "operator_minus"; | ||
34 | private static final String N_POWER = "operator_power"; | ||
35 | private static final String N_MULTIPLY = "operator_multiply"; | ||
36 | private static final String N_DIVIDE = "operator_divide"; | ||
37 | private static final String N_MODULO = "operator_modulo"; | ||
38 | private static final String N_LESSTHAN = "operator_lessThan"; | ||
39 | private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
40 | private static final String N_GREATERTHAN = "operator_greaterThan"; | ||
41 | private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
42 | private static final String N_EQUALS = "operator_equals"; | ||
43 | private static final String N_NOTEQUALS = "operator_notEquals"; | ||
44 | private static final String N_EQUALS3 = "operator_tripleEquals"; | ||
45 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
46 | |||
47 | 31 | ||
48 | private Context ctx; | 32 | private Context ctx; |
49 | private Solver s; | 33 | private Solver s; |