From 2fd7b130fe5d05137e162ede499d5cc661d83424 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Thu, 7 Jan 2021 23:23:37 -0500
Subject: fix dup decl bug + adjust famTree case study

---
 .../dslreasoner/viatra2logic/NumericDrealProblemSolver.java  | 12 +++++++-----
 .../case.study.familyTree.run/inputs/familytreeGen.vsconfig  |  7 ++++---
 .../queries/familyTreeConstraints.vql                        | 10 +++++-----
 3 files changed, 16 insertions(+), 13 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 d7268bb9..7dedfaeb 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
@@ -13,6 +13,7 @@ import java.util.Arrays;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Map.Entry;
 import java.util.UUID;
 import java.util.concurrent.TimeUnit;
 import java.util.regex.Matcher;
@@ -35,7 +36,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 
 	private final String containerName;
 	private Map<Object, String> varMap;
-	private List<String> curVars;
+	private Map<String, String> curVar2Decl;
 
 	public NumericDrealProblemSolver() throws IOException, InterruptedException {		
 		//setup docker
@@ -64,6 +65,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 		//TODO timeout if needed
 		if (!p.waitFor(5, TimeUnit.SECONDS)) {
 			p.destroy();
+			System.err.println("TIMEOUT");
 		}
 		return p;
 	}
@@ -171,11 +173,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 				varMap.put(matchedObj, expr);
 			}
 			//Add variable declarations
-			if(! curVars.contains(expr)) {
+			if(! curVar2Decl.keySet().contains(expr)) {
 				String varDecl = "(declare-fun " + expr + " () ";
 				if (isInt) {varDecl += "Int)";}
 				else {varDecl += "Real)";}
-				curVars.add(varDecl);
+				curVar2Decl.put(expr, varDecl);
 			}
 		} 
 		// Constants
@@ -227,7 +229,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 		String tempFileName = tempFile.getName();
 		
 		//STM2 FILE CONTENT CREATION
-		curVars = new ArrayList<String>();
+		curVar2Decl = new HashMap<String, String>();
 		List<String> curConstraints = new ArrayList<String>();
 		
 		PrintWriter printer = new PrintWriter(tempFile);
@@ -242,7 +244,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 			}
 		}
 		//Add Content to SMT2 file
-		for (String varDecl : curVars) {printer.println(varDecl);}
+		for (String varDecl : curVar2Decl.values()) {printer.println(varDecl);}
 		for (String negAssert : curConstraints) {printer.println(negAssert);}
 		printer.println("(check-sat)");
 		printer.close();
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig
index 01b7f040..7ead54af 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig
@@ -6,7 +6,7 @@ generate {
 	constraints = { package queries}
 	solver = ViatraSolver
 	scope = {
-		#node = 6..15,
+		#node = 10..30,
 		#int = {}
 	}
 	
@@ -20,6 +20,7 @@ generate {
 	runs = 1
 	
 	debug =			"outputs/debug"
-	log =			"outputs/log.txt"
-	output =		"outputs/models"
+	log =			"outputs/debug/log.txt"
+	output =		"outputs/models"	
+	statistics =	"outputs/statistics.csv"
 }
\ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql
index f8650073..450107d4 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql
+++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql
@@ -26,11 +26,11 @@ pattern negativeAge(m: Member) {
 	check(mage<0);
 }
 
-@Constraint(message="realisticAge", severity="error",key={m})
-pattern realisticAge(m: Member) {
-	Member.age(m,mage);
-	check(mage>120);
-}
+//@Constraint(message="realisticAge", severity="error",key={m})
+//pattern realisticAge(m: Member) {
+//	Member.age(m,mage);
+//	check(mage>120);
+//}
 
 @Constraint(message="parentTooYoung", severity="error", key={c, p})
 pattern parentTooYoung(c: Member, p: Member) = {
-- 
cgit v1.2.3-54-g00ecf