Add missing checks to make sure SMTLIB code is only generated when th…

…e option was selected

src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java

@@ -126,16 +126,22 @@ public BooleanFormula and(Collection<BooleanFormula> pBits) {
     switch (pBits.size()) {
       case 0:
         BooleanFormula result0 = makeTrue();
-        BooleanGenerator.logMakeTrue(result0, "true");
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logMakeTrue(result0, "true");
+        }
         return result0;
       case 1:
         BooleanFormula result1 = pBits.iterator().next();
-        BooleanGenerator.logAnd(result1, pBits);
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logAnd(result1, pBits);
+        }
         return result1;
       case 2:
         Iterator<BooleanFormula> it = pBits.iterator();
         BooleanFormula result2 = and(it.next(), it.next());
-        BooleanGenerator.logAnd(result2, pBits);
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logAnd(result2, pBits);
+        }
         return result2;
       default:
         BooleanFormula result = wrap(andImpl(Collections2.transform(pBits, this::extractInfo)));
@@ -209,16 +215,22 @@ public BooleanFormula or(Collection<BooleanFormula> pBits) {
     switch (pBits.size()) {
       case 0:
         BooleanFormula result0 = makeFalse();
-        BooleanGenerator.logMakeFalse(result0, "false");
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logMakeFalse(result0, "false");
+        }
         return result0;
       case 1:
         BooleanFormula result1 = pBits.iterator().next();
-        BooleanGenerator.logOr(result1, pBits);
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logOr(result1, pBits);
+        }
         return result1;
       case 2:
         Iterator<BooleanFormula> it = pBits.iterator();
         BooleanFormula result2 = or(it.next(), it.next());
-        BooleanGenerator.logOr(result2, pBits);
+        if (Generator.isLoggingEnabled()) {
+          BooleanGenerator.logOr(result2, pBits);
+        }
         return result2;
       default:
         BooleanFormula result = wrap(orImpl(Collections2.transform(pBits, this::extractInfo)));

src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java

@@ -41,23 +41,29 @@ protected AbstractEvaluator(
   public final <T extends Formula> T eval(T f) {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluation = evalImpl(creator.extractInfo(f));
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     return evaluation == null ? null : (T) creator.encapsulateWithTypeOf(evaluation);
   }
 
   @Nullable
   @Override
   public final BigInteger evaluate(IntegerFormula f) {
     Preconditions.checkState(!isClosed());
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
   public Rational evaluate(RationalFormula f) {
     Object value = evaluateImpl(creator.extractInfo(f));
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     if (value instanceof BigInteger) {
       // We simplified the value internally. Here, we need to convert it back to Rational.
       return Rational.ofBigInteger((BigInteger) value);
@@ -70,7 +76,9 @@ public Rational evaluate(RationalFormula f) {
   @Override
   public final Boolean evaluate(BooleanFormula f) {
     Preconditions.checkState(!isClosed());
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     return (Boolean) evaluateImpl(creator.extractInfo(f));
   }
 
@@ -92,7 +100,9 @@ public final String evaluate(EnumerationFormula f) {
   @Override
   public final BigInteger evaluate(BitvectorFormula f) {
     Preconditions.checkState(!isClosed());
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
@@ -103,7 +113,9 @@ public final Object evaluate(Formula f) {
     Preconditions.checkArgument(
         !(f instanceof ArrayFormula),
         "cannot compute a simple constant evaluation for an array-formula");
-    Generator.getLines().append("(get-value (" + f + "))\n");
+    if (Generator.isLoggingEnabled()) {
+      Generator.getLines().append("(get-value (" + f + "))\n");
+    }
     return evaluateImpl(creator.extractInfo(f));
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -202,7 +202,11 @@ public BooleanFormula universalParseFromString(String pString) {
 
   @Override
   public void dumpSMTLIB2() throws IOException {
-    Generator.dumpSMTLIB2();
+    if (Generator.isLoggingEnabled()) {
+      Generator.dumpSMTLIB2();
+    } else {
+      throw new UnsupportedOperationException("Generator needs to be enabled");
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -87,7 +87,9 @@ public int size() {
   @Override
   public final void push() throws InterruptedException {
     checkState(!closed);
-    Generator.logPush();
+    if (Generator.isLoggingEnabled()) {
+      Generator.logPush();
+    }
     pushImpl();
     assertedFormulas.add(new LinkedHashMap<>());
   }
@@ -98,7 +100,9 @@ public final void push() throws InterruptedException {
   public final void pop() {
     checkState(!closed);
     checkState(assertedFormulas.size() > 1, "initial level must remain until close");
-    Generator.logPop();
+    if (Generator.isLoggingEnabled()) {
+      Generator.logPop();
+    }
     assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
     popImpl();
   }

src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java

@@ -40,8 +40,11 @@ protected AbstractUFManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFunctionD
   public final <T extends Formula> FunctionDeclaration<T> declareUF(
       String pName, FormulaType<T> pReturnType, List<FormulaType<?>> pArgTypes) {
     checkVariableName(pName);
-    if (pName.contains("PIPE")) {
-      pName = pName.replaceAll("PIPE", "|");
+    if (Generator.isLoggingEnabled()) {
+      // FIXME Find a better way to handle quoted symbols
+      if (pName.contains("PIPE")) {
+        pName = pName.replaceAll("PIPE", "|");
+      }
     }
     List<TType> argTypes = Lists.transform(pArgTypes, this::toSolverType);
     FunctionDeclaration<T> result =
@@ -87,8 +90,11 @@ public final <T extends Formula> T callUF(
   public <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, List<Formula> pArgs) {
     checkVariableName(name);
-    if (name.contains("PIPE")) {
-      name = name.replaceAll("PIPE", "|");
+    if (Generator.isLoggingEnabled()) {
+      // FIXME Find a better way to handle quoted symbols
+      if (name.contains("PIPE")) {
+        name = name.replaceAll("PIPE", "|");
+      }
     }
     List<FormulaType<?>> argTypes = Lists.transform(pArgs, getFormulaCreator()::getFormulaType);
     FunctionDeclaration<T> func = declareUF(name, pReturnType, argTypes);

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -84,11 +84,13 @@ public void close() {
    */
   @Override
   public boolean isUnsat() throws SolverException, InterruptedException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      // FIXME: Find a better way to handle the IOException
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        // FIXME Find a better way to handle the IOException
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -185,10 +185,12 @@ public ImmutableList<ValueAssignment> getModelAssignments() throws SolverExcepti
   @Override
   @SuppressWarnings("try")
   public boolean isUnsat() throws InterruptedException, SolverException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     closeAllEvaluators();

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -164,10 +164,12 @@ public ImmutableList<ValueAssignment> getModelAssignments() throws SolverExcepti
   @Override
   @SuppressWarnings("try")
   public boolean isUnsat() throws InterruptedException, SolverException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     closeAllEvaluators();

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -101,10 +101,12 @@ private long buildConfig(Set<ProverOptions> opts) {
 
   @Override
   public boolean isUnsat() throws InterruptedException, SolverException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     return !msat_check_sat(curEnv);

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -219,10 +219,12 @@ protected String getReasonFromSolverFeatures(
   @SuppressWarnings("try") // ShutdownHook is never referenced, and this is correct.
   public boolean isUnsat() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     closeAllEvaluators();
     changedSinceLastSatQuery = false;

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -105,10 +105,12 @@ protected String addConstraint0(BooleanFormula constraint) {
 
   @Override
   public boolean isUnsat() throws InterruptedException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     checkState(!closed);
 

src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java

@@ -120,10 +120,12 @@ protected void pushImpl() throws InterruptedException {
 
   @Override
   public boolean isUnsat() throws SolverException, InterruptedException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     boolean unsat;

src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java

@@ -135,10 +135,12 @@ protected long getUnsatCore0() {
 
   @Override
   public boolean isUnsat() throws Z3SolverException, InterruptedException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     logSolverStack();

src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java

@@ -82,10 +82,12 @@ protected void assertContraintAndTrack(long constraint, long symbol) {
 
   @Override
   public boolean isUnsat() throws Z3SolverException, InterruptedException {
-    try {
-      Generator.dumpSMTLIB2();
-    } catch (IOException pE) {
-      throw new RuntimeException(pE);
+    if (Generator.isLoggingEnabled()) {
+      try {
+        Generator.dumpSMTLIB2();
+      } catch (IOException pE) {
+        throw new RuntimeException(pE);
+      }
     }
     Preconditions.checkState(!closed);
     logSolverStack();

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -196,7 +196,9 @@ public final void initSolver() throws InvalidConfigurationException {
     } catch (UnsupportedOperationException e) {
       emgr = null;
     }
-    Generator.resetGenerator();
+    if (Generator.isLoggingEnabled()) {
+      Generator.resetGenerator();
+    }
   }
 
   @After