Z3 option change (runtimeverification#199)

denis-bogdanas · web-flow · commit eee7ca5fcaf9 · 2018-11-22T22:32:50.000+02:00
1. SMT options: replaced --z3-executable with --z3-jni which is the opposite. Executable is now the default.
2. Fixed a bug in simplifyModuloPatternFolding that can lead to AssertionError.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java b/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java
@@ -149,8 +149,12 @@ public ConjunctiveFormula matchImplies(ConstrainedTerm constrainedTerm, boolean
 
         /* apply pattern folding */
         constraint = constraint.simplifyModuloPatternFolding(context)
-                .add(constrainedTerm.data.constraint)
-                .simplifyModuloPatternFolding(context);
+                .add(constrainedTerm.data.constraint);
+        if (constraint.isFalse()) {
+            return null;
+        }
+
+        constraint = constraint.simplifyModuloPatternFolding(context);
         if (constraint.isFalse()) {
             return null;
         }
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,10 +49,10 @@ public Z3Wrapper(
     }
 
     public synchronized boolean isUnsat(CharSequence query, int timeout, Z3Profiler timer) {
-        if (options.z3Executable) {
-            return checkQueryWithExternalProcess(query, timeout, timer);
-        } else {
+        if (options.z3JNI) {
             return checkQueryWithLibrary(query, timeout);
+        } else {
+            return checkQueryWithExternalProcess(query, timeout, timer);
         }
     }
 
diff --git a/k-distribution/include/ktest-keq.mak b/k-distribution/include/ktest-keq.mak
@@ -23,7 +23,7 @@ $(DEF2)/$(DEF2)-kompiled/timestamp: $(DEF2).k
 	$(KOMPILE) $< -d $(DEF2) --backend java
 
 keq: $(SPEC1) $(SPEC2) kompile
-	$(KEQ) -d $(DEF0) -d1 $(DEF1) -d2 $(DEF2) -s1 $(SPEC1) -s2 $(SPEC2) -sm1 $(MODULE1) -sm2 $(MODULE2) --smt_prelude $(BASIC_SMT) --z3-executable
+	$(KEQ) -d $(DEF0) -d1 $(DEF1) -d2 $(DEF2) -s1 $(SPEC1) -s2 $(SPEC2) -sm1 $(MODULE1) -sm2 $(MODULE2) --smt_prelude $(BASIC_SMT)
 
 clean:
 	rm -rf $(DEF0) $(DEF1) $(DEF2)
diff --git a/k-distribution/include/ktest.mak b/k-distribution/include/ktest.mak
@@ -49,7 +49,7 @@ else
 endif
 
 %-spec.k: kompile
-	$(KPROVE) $(KPROVE_FLAGS) -d $(DEFDIR) --z3-executable $@ $(CHECK) $@.out
+	$(KPROVE) $(KPROVE_FLAGS) -d $(DEFDIR) $@ $(CHECK) $@.out
 
 clean:
 	rm -rf $(DEFDIR)/$(DEF)-kompiled
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
@@ -41,8 +41,9 @@ public Class<SMTSolver> enumClass() {
     @Parameter(names={"--smt-prelude", "--smt_prelude"}, description="Path to the SMT prelude file.")
     public String smtPrelude;
 
-    @Parameter(names="--z3-executable", description="Invokes Z3 as an external process.")
-    public boolean z3Executable = false;
+    @Parameter(names="--z3-jni", description="Invokes Z3 as JNI library. Default is external process. " +
+            "JNI is slightly faster, but can potentially lead to JVM crash.")
+    public boolean z3JNI = false;
 
     @Parameter(names="--z3-cnstr-timeout", description="The default soft timeout (in milli seconds) of Z3 for checking constraint satisfiability.")
     public int z3CnstrTimeout = 50;

Original file line number	Diff line number	Diff line change
`@@ -49,10 +49,10 @@ public Z3Wrapper(`
`49`	`49`	`}`
`50`	`50`
`51`	`51`	`public synchronized boolean isUnsat(CharSequence query, int timeout, Z3Profiler timer) {`
`52`		`- if (options.z3Executable) {`
`53`		`- return checkQueryWithExternalProcess(query, timeout, timer);`
`54`		`- } else {`
	`52`	`+ if (options.z3JNI) {`
`55`	`53`	`return checkQueryWithLibrary(query, timeout);`
	`54`	`+ } else {`
	`55`	`+ return checkQueryWithExternalProcess(query, timeout, timer);`
`56`	`56`	`}`
`57`	`57`	`}`
`58`	`58`