Princess: redirect 'System.err' to avoid cluttering the output.

This is a first step for #392 .
The situation is also reported to Ostrich in uuverifiers/ostrich#95 .

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java

@@ -20,6 +20,9 @@
 import ap.parser.ITerm;
 import com.google.common.base.Preconditions;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import java.io.IOException;
+import java.io.OutputStream;
+import java.io.PrintStream;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Collection;
@@ -29,6 +32,7 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
+import java.util.function.Supplier;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -89,7 +93,8 @@ public boolean isUnsat() throws SolverException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
     evaluatedTerms.clear();
-    final Value result = api.checkSat(true);
+
+    final Value result = callWithoutSystemErrStream(() -> api.checkSat(true));
     if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) {
       wasLastSatCheckSat = true;
       evaluatedTerms.add(api.partialModelAsFormula());
@@ -183,7 +188,7 @@ protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
    * @throws SimpleAPIException if model can not be constructed.
    */
   private PartialModel partialModel() throws SimpleAPIException {
-    return api.partialModel();
+    return callWithoutSystemErrStream(api::partialModel);
   }
 
   @Override
@@ -197,7 +202,7 @@ public List<BooleanFormula> getUnsatCore() {
     Preconditions.checkState(!closed);
     checkGenerateUnsatCores();
     final List<BooleanFormula> result = new ArrayList<>();
-    final Set<Object> core = asJava(api.getUnsatCore());
+    final Set<Object> core = asJava(callWithoutSystemErrStream(api::getUnsatCore));
     for (Object partitionId : core) {
       result.add(partitions.peek().get(partitionId));
     }
@@ -278,4 +283,34 @@ public String toString() {
       return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols);
     }
   }
+
+  /**
+   * Princess uses Ostrich as internal library. Ostrich logs to `System.err`. We redirect this
+   * stream to the void to avoid cluttering the output.
+   *
+   * <p>Technical dept: `System.err` is a global static field, we redirect all logging. :-(
+   *
+   * @param fn the function to call
+   */
+  @SuppressWarnings(value = "IllegalInstantiation")
+  @CanIgnoreReturnValue
+  static <R> R callWithoutSystemErrStream(Supplier<R> fn) {
+    final PrintStream originalErrStream = System.err;
+    try (OutputStream nullOutput = new NullOutputStream();
+        PrintStream nullStream = new PrintStream(nullOutput)) {
+      System.setErr(nullStream);
+      return fn.get();
+    } catch (IOException ioException) {
+      throw new AssertionError(ioException);
+    } finally {
+      System.setErr(originalErrStream);
+    }
+  }
+
+  private static final class NullOutputStream extends OutputStream {
+    @Override
+    public void write(int b) {
+      // do nothing
+    }
+  }
 }

src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
+import static org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.callWithoutSystemErrStream;
 import static scala.collection.JavaConverters.asJava;
 
 import ap.api.PartialModel;
@@ -69,7 +70,8 @@ class PrincessModel extends AbstractModel<IExpression, Sort, PrincessEnvironment
 
   @Override
   public ImmutableList<ValueAssignment> asList() {
-    scala.collection.Map<IExpression, IExpression> interpretation = model.interpretation();
+    scala.collection.Map<IExpression, IExpression> interpretation =
+        callWithoutSystemErrStream(model::interpretation);
 
     // get abbreviations, we do not want to export them.
     Set<Predicate> abbrevs = new LinkedHashSet<>();
@@ -303,16 +305,16 @@ private ITerm simplifyRational(ITerm pTerm) {
       ITerm term = (ITerm) expr;
       ITerm var = api.createConstant(newVariable, getSort(term));
       api.addAssertion(var.$eq$eq$eq(term));
-      api.checkSat(true);
-      ITerm value = simplifyRational(api.evalToTerm(var));
+      callWithoutSystemErrStream(() -> api.checkSat(true));
+      ITerm value = simplifyRational(callWithoutSystemErrStream(() -> api.evalToTerm(var)));
       api.pop();
       prover.addEvaluatedTerm(value.$eq$eq$eq(term));
       return value;
     } else {
       IFormula formula = (IFormula) expr;
       IFormula var = api.createBooleanVariable(newVariable);
       api.addAssertion(var.$less$eq$greater(formula));
-      api.checkSat(true);
+      callWithoutSystemErrStream(() -> api.checkSat(true));
       IFormula value = IBoolLit$.MODULE$.apply(api.eval(var));
       api.pop();
       prover.addEvaluatedTerm(value.$less$eq$greater(formula));