From 9f02e7e2fe8b3e347f3d05e8d0751dec016842cd Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 7 Feb 2021 04:54:42 +0100 Subject: measurement setup is ready for server --- .../viatra2logic/NumericDrealProblemSolver.java | 35 +++++++++++----------- .../viatra2logic/NumericZ3ProblemSolver.java | 7 +++-- 2 files changed, 22 insertions(+), 20 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index 4fef6448..e0ebcb6b 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java @@ -43,7 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Map curVar2Decl; private final int TIMEOUT_DOCKER = 5000; - private final int TIMEOUT_LOCAL = 20000; + private final int TIMEOUT_LOCAL = 10000; + private final boolean DEBUG_PRINT = false; public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { this.useDocker = useDocker; @@ -86,8 +87,10 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } return null; } - double duration = (double) (System.nanoTime() - startTime) / 1000000000; - System.out.println("Dur = " + duration + " : "); + if (DEBUG_PRINT) { + double duration = (double) (System.nanoTime() - startTime) / 1000000000; + System.out.println("Dur = " + duration + " : "); + } return p; } @@ -397,17 +400,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } endSolvingProblem = System.nanoTime()-startSolvingProblem; - //DEBUG - Print things - if (outputProcess == null) { - + if (outputProcess == null) { System.err.println("TIMEOUT"); // printOutput(numProbContent); } - -// printOutput(numProbContent); -// if (outputs != null) printOutput(outputs.get(0)); - System.out.println(result); -// END DEBUG + if (DEBUG_PRINT) { + // printOutput(numProbContent); + // if (outputs != null) printOutput(outputs.get(0)); + System.out.println(result); + } return result; } @@ -459,12 +460,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; - //DEBUG - Print things - System.out.println("Getting Solution!"); -// printOutput(numProbContent); -// printOutput(outputs.get(0)); -// System.out.println(result); - //END DEBUG + if (DEBUG_PRINT) { + System.out.println("Getting Solution!"); + // printOutput(numProbContent); + // printOutput(outputs.get(0)); + // System.out.println(result); + } //GET SOLUTION if (result) { 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 0e47e820..612e93a6 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 @@ -39,9 +39,10 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ public NumericZ3ProblemSolver() { //FOR LINUX VM //Not Elegant, but this is working for now - String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); - System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); - System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); +// String root = "/home/models/VIATRA-Generator"; +// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); +// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); +// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); //End non-elegance HashMap cfg = new HashMap(); -- cgit v1.2.3-54-g00ecf