Add (check-sat) to preprocess context before proving goal

kframework · Nov 17, 2017 · 199a476 · 199a476
1 parent 1b4fb8e
commit 199a476
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 6 deletions.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java
@@ -195,9 +195,9 @@ public static String translateImplication(
         sb.append(leftTransformer.getConstantDeclarations(Sets.difference(
                 Sets.union(leftTransformer.variables(), rightTransformer.variables()),
                 rightHandSideOnlyVariables)));
-        sb.append("(assert (and ");
+        sb.append("(assert ");
         sb.append(leftExpression);
-        sb.append(" (not ");
+        sb.append(")\n(check-sat)\n(assert (not ");
         rightHandSideOnlyVariables = Sets.intersection(
                 rightTransformer.variables(),
                 rightHandSideOnlyVariables);
@@ -210,7 +210,7 @@ public static String translateImplication(
         if (!rightHandSideOnlyVariables.isEmpty()) {
             sb.append(")");
         }
-        sb.append(")))");
+        sb.append("))");
         return sb.toString();
     }
 

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java
@@ -55,7 +55,7 @@ public boolean impliesSMT(
             Set<Variable> rightOnlyVariables) {
         if (smtOptions.smt == SMTSolver.Z3) {
             try {
-                return z3.isUnsat(
+                return z3.isImplication(
                         KILtoSMTLib.translateImplication(left, right, rightOnlyVariables),
                         smtOptions.z3ImplTimeout);
             } catch (UnsupportedOperationException e) {

diff --git a/java-backend/src/main/java/org/kframework/backend/java/util/Z3Wrapper.java b/java-backend/src/main/java/org/kframework/backend/java/util/Z3Wrapper.java
@@ -49,7 +49,15 @@ public Z3Wrapper(
 
     public synchronized boolean isUnsat(String query, int timeout) {
         if (options.z3Executable) {
-            return checkQueryWithExternalProcess(query, timeout);
+            return checkQueryWithExternalProcess(query, 0, timeout);
+        } else {
+            return checkQueryWithLibrary(query, timeout);
+        }
+    }
+
+    public synchronized boolean isImplication(String query, int timeout) {
+        if (options.z3Executable) {
+            return checkQueryWithExternalProcess(query, 1, timeout);
         } else {
             return checkQueryWithLibrary(query, timeout);
         }
@@ -76,7 +84,7 @@ private boolean checkQueryWithLibrary(String query, int timeout) {
         return result;
     }
 
-    private boolean checkQueryWithExternalProcess(String query, int timeout) {
+    private boolean checkQueryWithExternalProcess(String query, int intermediateCheckSatCalls, int timeout) {
         String result = "";
         try {
             for (int i = 0; i < Z3_RESTART_LIMIT; i++) {
@@ -94,6 +102,16 @@ private boolean checkQueryWithExternalProcess(String query, int timeout) {
                     z3Process.getInputStream()));
                 input.write(SMT_PRELUDE + query + "(check-sat)\n");
                 input.flush();
+                input.close();
+                for (int ignores = 0; ignores < intermediateCheckSatCalls; ++ignores) {
+                    result = output.readLine();
+                    if (result == null) {
+                        break;
+                    }
+                    if (globalOptions.debug && !Z3_QUERY_RESULTS.contains(result)) {
+                        break;
+                    }
+                }
                 result = output.readLine();
                 z3Process.destroy();
                 if (result != null) {