From 8fd50f7d4a979117a1e643f5384b76f4a3e36801 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Mon, 14 Dec 2020 03:27:43 -0500 Subject: implement isSatisfiable with Dreal integration --- .../dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java') 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 public class NumericZ3ProblemSolver extends NumericProblemSolver{ - private static final String N_Base = "org.eclipse.xtext.xbase.lib."; - private static final String N_PLUS = "operator_plus"; - private static final String N_MINUS = "operator_minus"; - private static final String N_POWER = "operator_power"; - private static final String N_MULTIPLY = "operator_multiply"; - private static final String N_DIVIDE = "operator_divide"; - private static final String N_MODULO = "operator_modulo"; - private static final String N_LESSTHAN = "operator_lessThan"; - private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; - private static final String N_GREATERTHAN = "operator_greaterThan"; - private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; - private static final String N_EQUALS = "operator_equals"; - private static final String N_NOTEQUALS = "operator_notEquals"; - private static final String N_EQUALS3 = "operator_tripleEquals"; - private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; - private Context ctx; private Solver s; -- cgit v1.2.3-54-g00ecf