aboutsummaryrefslogtreecommitdiffstats
path: root/Framework
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-07 04:54:42 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-07 04:54:42 +0100
commit9f02e7e2fe8b3e347f3d05e8d0751dec016842cd (patch)
tree6d0c34c617ed51c9c9715f3ec18552425656b3a5 /Framework
parentRemove dreal (diff)
downloadVIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.gz
VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.zst
VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.zip
measurement setup is ready for server
Diffstat (limited to 'Framework')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java35
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java7
2 files changed, 22 insertions, 20 deletions
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{
43 private Map<String, String> curVar2Decl; 43 private Map<String, String> curVar2Decl;
44 44
45 private final int TIMEOUT_DOCKER = 5000; 45 private final int TIMEOUT_DOCKER = 5000;
46 private final int TIMEOUT_LOCAL = 20000; 46 private final int TIMEOUT_LOCAL = 10000;
47 private final boolean DEBUG_PRINT = false;
47 48
48 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { 49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {
49 this.useDocker = useDocker; 50 this.useDocker = useDocker;
@@ -86,8 +87,10 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
86 } 87 }
87 return null; 88 return null;
88 } 89 }
89 double duration = (double) (System.nanoTime() - startTime) / 1000000000; 90 if (DEBUG_PRINT) {
90 System.out.println("Dur = " + duration + " : "); 91 double duration = (double) (System.nanoTime() - startTime) / 1000000000;
92 System.out.println("Dur = " + duration + " : ");
93 }
91 return p; 94 return p;
92 } 95 }
93 96
@@ -397,17 +400,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
397 } 400 }
398 endSolvingProblem = System.nanoTime()-startSolvingProblem; 401 endSolvingProblem = System.nanoTime()-startSolvingProblem;
399 402
400 //DEBUG - Print things 403 if (outputProcess == null) {
401 if (outputProcess == null) {
402
403 System.err.println("TIMEOUT"); 404 System.err.println("TIMEOUT");
404// printOutput(numProbContent); 405// printOutput(numProbContent);
405 } 406 }
406 407 if (DEBUG_PRINT) {
407// printOutput(numProbContent); 408 // printOutput(numProbContent);
408// if (outputs != null) printOutput(outputs.get(0)); 409 // if (outputs != null) printOutput(outputs.get(0));
409 System.out.println(result); 410 System.out.println(result);
410// END DEBUG 411 }
411 412
412 return result; 413 return result;
413 } 414 }
@@ -459,12 +460,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
459 boolean result = getDrealResult(outputProcess.exitValue(), outputs); 460 boolean result = getDrealResult(outputProcess.exitValue(), outputs);
460 endSolvingProblem = System.nanoTime()-startSolvingProblem; 461 endSolvingProblem = System.nanoTime()-startSolvingProblem;
461 462
462 //DEBUG - Print things 463 if (DEBUG_PRINT) {
463 System.out.println("Getting Solution!"); 464 System.out.println("Getting Solution!");
464// printOutput(numProbContent); 465 // printOutput(numProbContent);
465// printOutput(outputs.get(0)); 466 // printOutput(outputs.get(0));
466// System.out.println(result); 467 // System.out.println(result);
467 //END DEBUG 468 }
468 469
469 //GET SOLUTION 470 //GET SOLUTION
470 if (result) { 471 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{
39 public NumericZ3ProblemSolver() { 39 public NumericZ3ProblemSolver() {
40 //FOR LINUX VM 40 //FOR LINUX VM
41 //Not Elegant, but this is working for now 41 //Not Elegant, but this is working for now
42 String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); 42// String root = "/home/models/VIATRA-Generator";
43 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); 43// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
44 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 44// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
45// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
45 //End non-elegance 46 //End non-elegance
46 47
47 HashMap<String, String> cfg = new HashMap<String, String>(); 48 HashMap<String, String> cfg = new HashMap<String, String>();