From 86518413bed5988092b30d1139bb72ef302ae09c Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Sun, 17 Jan 2021 01:16:26 -0500
Subject: complete queries for lane structure

---
 .../viatra2logic/NumericDrealProblemSolver.java    | 34 ++++++++++++----------
 1 file changed, 19 insertions(+), 15 deletions(-)

(limited to 'Framework')

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 f410cc6d..f6c0bc71 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
@@ -7,13 +7,11 @@ import java.io.FileInputStream;
 import java.io.IOException;
 import java.io.InputStream;
 import java.io.InputStreamReader;
-import java.io.PrintWriter;
 import java.util.ArrayList;
 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;
@@ -25,9 +23,6 @@ import org.eclipse.xtext.xbase.XExpression;
 import org.eclipse.xtext.xbase.XFeatureCall;
 import org.eclipse.xtext.xbase.XNumberLiteral;
 
-import com.microsoft.z3.IntExpr;
-import com.microsoft.z3.RealExpr;
-
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
@@ -168,6 +163,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 				}
 			} else {
 				//TODO unsure what it means if something gets in here
+				System.err.println("Reached weird place");
 				if (isInt) {
 					expr = Integer.toString(((IntegerElement) matchedObj).getValue());
 				} else {
@@ -342,20 +338,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
 		if (result) {
 			long startFormingSolution = System.nanoTime();
 			Map<String, String> solMap = parseDrealOutput(outputs.get(0));
+			
+//			//DEBUG
+//			System.out.println("RESULT");
+//			solMap.entrySet().forEach(System.out::println);
+//			System.out.println("SOLMAP");
+//			varMap.forEach((k, v) -> System.out.println(v + "=" + k));
+//			//END DEBUG
+			
 			for (PrimitiveElement obj: objs) {
 				if(varMap.containsKey(obj)) {
-					if (obj instanceof IntegerElement) {
-						String varName = varMap.get(obj);
-						String value = solMap.get(varName);
-						sol.put(obj, Integer.parseInt(value));
-					} else {
-						String varName = varMap.get(obj);
-						String value = solMap.get(varName);
-						sol.put(obj, Double.parseDouble(value));
+					String varName = varMap.get(obj);
+					String value = solMap.get(varName);
+					if (value != null) {
+						//this means that dreal actually worked on this and found a value for it
+						if (obj instanceof IntegerElement) {
+							sol.put(obj, Integer.parseInt(value));
+						} else {
+							sol.put(obj, Double.parseDouble(value));
+						}
 					}
-
 				} else {
-//					System.out.println(("variable " + obj + " is not used from Dreal");
+//					System.err.println("variable " + obj + " is not used from Dreal");
 				}
 			}
 			endFormingSolution = System.nanoTime() - startFormingSolution;
-- 
cgit v1.2.3-54-g00ecf