SMTOperations, GlobalContext: only print missing SMTLib warning with …

…--debug - Requires passing the `GlobalOptions` to `SMTOperations`. - More informative output regarding why SMT solver could not prove something.
kframework · Nov 18, 2017 · a1ee3ec · a1ee3ec
1 parent 8aff58f
commit a1ee3ec
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 9 deletions.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/GlobalContext.java b/java-backend/src/main/java/org/kframework/backend/java/kil/GlobalContext.java
@@ -52,7 +52,7 @@ public GlobalContext(
         this.hookProvider = hookProvider;
         this.files = files;
         this.equalityOps = new EqualityOperations(() -> def);
-        this.constraintOps = new SMTOperations(() -> def, smtOptions, new Z3Wrapper(smtOptions, kem, globalOptions, files), kem);
+        this.constraintOps = new SMTOperations(() -> def, smtOptions, new Z3Wrapper(smtOptions, kem, globalOptions, files), kem, globalOptions);
         this.kItemOps = new KItemOperations(stage, deterministicFunctions, kem, this::builtins, globalOptions);
         this.stage = stage;
     }

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
@@ -1,6 +1,7 @@
 // Copyright (c) 2015-2016 K Team. All Rights Reserved.
 package org.kframework.backend.java.symbolic;
 
+import org.kframework.main.GlobalOptions;
 import org.kframework.backend.java.kil.Definition;
 import org.kframework.backend.java.kil.Variable;
 import org.kframework.backend.java.util.Z3Wrapper;
@@ -14,18 +15,21 @@
 
 public class SMTOperations {
 
-    private final SMTOptions smtOptions;
-    private final Z3Wrapper z3;
-
+    private final SMTOptions        smtOptions;
+    private final Z3Wrapper         z3;
+    private final GlobalOptions     global;
     private final KExceptionManager kem;
 
     public SMTOperations(
             Provider<Definition> definitionProvider,
             SMTOptions smtOptions,
-            Z3Wrapper z3, KExceptionManager kem) {
+            Z3Wrapper z3,
+            KExceptionManager kem,
+            GlobalOptions global) {
         this.smtOptions = smtOptions;
-        this.z3 = z3;
-        this.kem = kem;
+        this.z3         = z3;
+        this.kem        = kem;
+        this.global     = global;
     }
 
     public boolean checkUnsat(ConjunctiveFormula constraint) {
@@ -64,8 +68,9 @@ public boolean impliesSMT(
                         smtOptions.z3ImplTimeout);
             } catch (UnsupportedOperationException | SMTTranslationFailure e) {
                 kem.registerCriticalWarning(e.getMessage(), e);
-                System.err.println(e.getMessage() + "\n");
-                // TODO: no longer printing stack trace. Perhaps in the future can extract useful information from stack trace to print
+                if (global.debug) {
+                    System.err.println(e.getMessage() + "\n");
+                }
             }
         }
         return false;