From 88f90f0f78ab94ab67c8aaa882023d059a31b385 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Wed, 3 Feb 2021 02:34:15 +0100
Subject: fix derived feature handling + impove dreal calling

---
 .../viatra2logic/NumericDrealProblemSolver.java    | 36 ++++++++++++++++++----
 1 file changed, 30 insertions(+), 6 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 0105d985..4fef6448 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
@@ -42,8 +42,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 	private Map<Object, String> varMap;
 	private Map<String, String> curVar2Decl;
 	
-	private final int TIMEOUT_DOCKER = 5;
-	private final int TIMEOUT_LOCAL = 2;
+	private final int TIMEOUT_DOCKER = 5000;
+	private final int TIMEOUT_LOCAL = 20000;
 
 	public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {
 		this.useDocker = useDocker;
@@ -68,14 +68,26 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 	}
 	
 	private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException {
-		String s = String.join(" ", cmd);
-		Process p = Runtime.getRuntime().exec(s);
+//		String s = String.join(" ", cmd);
+//		Process p = Runtime.getRuntime().exec(s);
+		Process p = (new ProcessBuilder(cmd)).start();
 //		p.waitFor();
 		//TODO timeout if needed
-		if (!p.waitFor(timeout, TimeUnit.SECONDS)) {
+		long startTime = System.nanoTime();
+		if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) {
 			p.destroy();
+			if (p.isAlive()) {
+			    p.destroyForcibly();
+			    if (p.isAlive()) {
+					//Platform-specific but fine for now
+				    Runtime.getRuntime().exec("killall -9 dreal").waitFor();
+				    if (p.isAlive()) System.out.println("dreal process not closed");
+			    }
+			}
 			return null;
 		}
+		double duration = (double) (System.nanoTime() - startTime) / 1000000000;
+		System.out.println("Dur = " + duration + " : ");
 		return p;
 	}
 	
@@ -371,18 +383,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 		if (outputProcess != null) { 
 			outputs = getProcessOutput(outputProcess);
 			result = getDrealResult(outputProcess.exitValue(), outputs);
+//		} else {
+//			System.err.print("Timeout, RETRYING...");
+//			if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false);
+//			else outputProcess = callDrealLocal(numProbContent, false);
+//			if (outputProcess != null) { 
+//				outputs = getProcessOutput(outputProcess);
+//				result = getDrealResult(outputProcess.exitValue(), outputs);
+//				System.out.println("pass");
+//			} else {
+//				System.out.println("fail");
+//			}
 		}
 		endSolvingProblem = System.nanoTime()-startSolvingProblem;
 		
 		//DEBUG - Print things
 		if (outputProcess == null) {
+			
 			System.err.println("TIMEOUT");
 //			printOutput(numProbContent);
 		}
 		
 //		printOutput(numProbContent);
 //		if (outputs != null) printOutput(outputs.get(0));
-//		System.out.println(result);
+		System.out.println(result);
 //		END DEBUG
 		
 		return result;
-- 
cgit v1.2.3-70-g09d2