aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend12
1 files changed, 11 insertions, 1 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index fc1a616b..b8ea25e5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -53,7 +53,17 @@ class NumericSolver {
53 return new NumericDrealProblemSolver(true, null) 53 return new NumericDrealProblemSolver(true, null)
54 if (solverSelection == NumericSolverSelection.DREAL_LOCAL) 54 if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
55 return new NumericDrealProblemSolver(false, drealLocalPath) 55 return new NumericDrealProblemSolver(false, drealLocalPath)
56 if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver 56 if (solverSelection == NumericSolverSelection.Z3) {
57 //TODO THIS IS HARD-CODED for now
58 val root = "/data/viatra/VIATRA-Generator";
59 //END HARD-CODED
60// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
61 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
62 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
63// System.load("libz3.so");
64// System.load("libz3java.so");
65 return new NumericZ3ProblemSolver
66 }
57 } 67 }
58 68
59 def init(ThreadContext context) { 69 def init(ThreadContext context) {