Merge pull request #396 from sosy-lab/371-better-performance-in-floatingpointmanagertest

Bitwuzla: Fix performance issues in FloatingPointFormulaManagerTest

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -231,6 +231,9 @@ public enum FunctionDeclarationKind {
   /** Division over floating points. */
   FP_DIV,
 
+  /** Remainder of the floating point division. */
+  FP_REM,
+
   /** Multiplication over floating points. */
   FP_MUL,
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java

@@ -28,6 +28,9 @@ public class BitwuzlaFloatingPointManager
   private final TermManager termManager;
   private final Term roundingMode;
 
+  // Keeps track of the temporary variables that are created for fp-to-bv casts
+  private static int counter = 0;
+
   protected BitwuzlaFloatingPointManager(
       BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
     super(pCreator);
@@ -200,20 +203,32 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType
 
   @Override
   protected Term toIeeeBitvectorImpl(Term pNumber) {
-    // FIXME: We should use a reserved symbol for the fresh variables
     int sizeExp = pNumber.sort().fp_exp_size();
     int sizeSig = pNumber.sort().fp_sig_size();
 
     Sort bvSort = termManager.mk_bv_sort(sizeExp + sizeSig);
 
+    // The following code creates a new variable that is returned as result.
+    // Additionally, we track constraints about the equality of the new variable and the FP number,
+    // which is added onto the prover stack whenever the new variable is used as assertion.
+
+    // TODO This internal implementation is a technical dept and should be removed.
+    //   The additional constraints are not transparent in all cases, e.g., when visiting a
+    //   formula, creating a model, or transferring the assertions onto another prover stack.
+    //   A better way would be a direct implementation of this in Bitwuzla, without interfering
+    //   with JavaSMT.
+
     // Note that NaN is handled as a special case in this method. This is not strictly necessary,
     // but if we just use "fpTerm = to_fp(bvVar)" the NaN will be given a random payload (and
     // sign). Since NaN payloads are not preserved here anyway we might as well pick a canonical
-    // representation.
-    Term bvNaN =
-        termManager.mk_bv_value(bvSort, "0" + "1".repeat(sizeExp + 1) + "0".repeat(sizeSig - 2));
-
-    Term bvVar = termManager.mk_const(bvSort, pNumber.symbol() + "_toIeeeBitvector");
+    // representation, e.g., which is "0 11111111 10000000000000000000000" for single precision.
+    String nanRepr = "0" + "1".repeat(sizeExp + 1) + "0".repeat(sizeSig - 2);
+    Term bvNaN = termManager.mk_bv_value(bvSort, nanRepr);
+
+    // TODO creating our own utility variables might eb unexpected from the user.
+    //   We might need to exclude such variables in models and formula traversal.
+    String newVariable = "__JAVASMT__CAST_FROM_BV_" + counter++;
+    Term bvVar = termManager.mk_const(bvSort, newVariable);
     Term equal =
         termManager.mk_term(
             Kind.ITE,
@@ -224,7 +239,7 @@ protected Term toIeeeBitvectorImpl(Term pNumber) {
                 termManager.mk_term(Kind.FP_TO_FP_FROM_BV, bvVar, sizeExp, sizeSig),
                 pNumber));
 
-    bitwuzlaCreator.addVariableCast(equal);
+    bitwuzlaCreator.addConstraintForVariable(newVariable, equal);
     return bvVar;
   }
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -9,16 +9,22 @@
 package org.sosy_lab.java_smt.solvers.bitwuzla;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.HashBasedTable;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Table;
 import java.math.BigInteger;
+import java.util.ArrayDeque;
 import java.util.ArrayList;
-import java.util.HashSet;
+import java.util.Collection;
+import java.util.Deque;
+import java.util.HashMap;
 import java.util.Iterator;
+import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Optional;
 import java.util.Set;
@@ -55,7 +61,21 @@ public class BitwuzlaFormulaCreator extends FormulaCreator<Term, Sort, Void, Bit
 
   private final Table<String, Sort, Term> formulaCache = HashBasedTable.create();
 
-  private final Set<Term> variableCasts = new HashSet<>();
+  /**
+   * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their
+   * defining equation.
+   *
+   * <p>Bitwuzla does not support casts from floating-point to bitvector natively. The reason given
+   * is that the value is undefined for NaN and that the SMT-LIB standard also does not include such
+   * an operation. We try to work around this limitation by introducing a fresh variable <code>
+   * __CAST_FROM_BV_XXX</code>for the result and then adding the constraint <code>
+   * fp.to_fp(__CAST_FROM_BV_XXX) = &lt;float-term&gt;</code> as a side-condition. This is also what
+   * is recommended by the SMT-LIB2 standard. The map <code>variableCasts</code> is used to store
+   * these side-conditions so that they can later be added as assertions. The keys of the map are
+   * the newly introduced variable symbols and the values are the defining equations as mentioned
+   * above.
+   */
+  private final Map<String, Term> constraintsForVariables = new HashMap<>();
 
   protected BitwuzlaFormulaCreator(TermManager pTermManager) {
     super(null, pTermManager.mk_bool_sort(), null, null, null, null);
@@ -221,6 +241,8 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {
       return FunctionDeclarationKind.BV_SGT;
     } else if (kind.equals(Kind.BV_SHL)) {
       return FunctionDeclarationKind.BV_SHL;
+    } else if (kind.equals(Kind.BV_SHR)) {
+      return FunctionDeclarationKind.BV_LSHR;
     } else if (kind.equals(Kind.BV_SLE)) {
       return FunctionDeclarationKind.BV_SLE;
     } else if (kind.equals(Kind.BV_SLT)) {
@@ -283,6 +305,8 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {
       return FunctionDeclarationKind.FP_MIN;
     } else if (kind.equals(Kind.FP_MUL)) {
       return FunctionDeclarationKind.FP_MUL;
+    } else if (kind.equals(Kind.FP_REM)) {
+      return FunctionDeclarationKind.FP_REM;
     } else if (kind.equals(Kind.FP_NEG)) {
       return FunctionDeclarationKind.FP_NEG;
     } else if (kind.equals(Kind.FP_RTI)) {
@@ -572,11 +596,34 @@ public Object convertValue(Term term) {
     throw new AssertionError("Unknown value type.");
   }
 
-  public void addVariableCast(Term equal) {
-    variableCasts.add(equal);
+  /** Add a constraint that is pushed onto the prover stack whenever the variable is used. */
+  public void addConstraintForVariable(String variable, Term constraint) {
+    constraintsForVariables.put(variable, constraint);
   }
 
-  public Iterable<Term> getVariableCasts() {
-    return variableCasts;
+  /**
+   * Returns a set of additional constraints (side-conditions) that are needed to use some variables
+   * from the given term, such as utility variables from casts.
+   *
+   * <p>Bitwuzla does not support fp-to-bv conversion natively. We have to use side-conditions as a
+   * workaround. When a term containing fp-to-bv casts is added to the assertion stack these
+   * side-conditions need to be collected by calling this method and then also adding them to the
+   * assertion stack.
+   */
+  public Collection<Term> getConstraintsForTerm(Term pTerm) {
+    final Set<String> usedConstraintVariables = new LinkedHashSet<>();
+    final Deque<String> waitlist = new ArrayDeque<>(extractVariablesAndUFs(pTerm, false).keySet());
+    while (!waitlist.isEmpty()) {
+      String current = waitlist.pop();
+      if (constraintsForVariables.containsKey(current)) { // ignore variables without constraints
+        if (usedConstraintVariables.add(current)) {
+          // if we found a new variable with constraint, get transitive variables from constraint
+          Term constraint = constraintsForVariables.get(current);
+          waitlist.addAll(extractVariablesAndUFs(constraint, false).keySet());
+        }
+      }
+    }
+
+    return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get);
   }
 }

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java

@@ -186,8 +186,12 @@ public Appender dumpFormula(Term pTerm) {
     return new Appenders.AbstractAppender() {
       @Override
       public void appendTo(Appendable out) throws IOException {
+        if (pTerm.is_value()) {
+          out.append("(assert " + pTerm + ")");
+          return;
+        }
         Bitwuzla bitwuzla = new Bitwuzla(creator.getTermManager());
-        for (Term t : creator.getVariableCasts()) {
+        for (Term t : creator.getConstraintsForTerm(pTerm)) {
           bitwuzla.assert_formula(t);
         }
         bitwuzla.assert_formula(pTerm);

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -12,6 +12,7 @@
 import com.google.common.collect.Collections2;
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
@@ -24,7 +25,6 @@
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
-import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaBooleanFormula;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options;
@@ -93,7 +93,11 @@ public void popImpl() {
   @Override
   public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
     wasLastSatCheckSat = false;
-    env.assert_formula(((BitwuzlaBooleanFormula) constraint).getTerm());
+    Term formula = creator.extractInfo(constraint);
+    env.assert_formula(formula);
+    for (Term t : creator.getConstraintsForTerm(formula)) {
+      env.assert_formula(t);
+    }
     return null;
   }
 
@@ -127,7 +131,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
   public boolean isUnsat() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
-    final Result result = env.check_sat(new Vector_Term(creator.getVariableCasts()));
+    final Result result = env.check_sat();
     return readSATResult(result);
   }
 
@@ -142,12 +146,15 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
       throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
-    Vector_Term ass = new Vector_Term(creator.getVariableCasts());
+
+    Collection<Term> newAssumptions = new LinkedHashSet<>();
     for (BooleanFormula formula : assumptions) {
-      BitwuzlaBooleanFormula bitwuzlaFormula = (BitwuzlaBooleanFormula) formula;
-      ass.add(bitwuzlaFormula.getTerm());
+      Term term = creator.extractInfo(formula);
+      newAssumptions.add(term);
+      newAssumptions.addAll(creator.getConstraintsForTerm(term));
     }
-    final Result result = env.check_sat(ass);
+
+    final Result result = env.check_sat(new Vector_Term(newAssumptions));
     return readSATResult(result);
   }
 

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

@@ -489,6 +489,7 @@ private Expr normalize(Expr operator) {
           .put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
           .put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)
           .put(Kind.FLOATINGPOINT_DIV, FunctionDeclarationKind.FP_DIV)
+          .put(Kind.FLOATINGPOINT_REM, FunctionDeclarationKind.FP_REM)
           .put(Kind.FLOATINGPOINT_LT, FunctionDeclarationKind.FP_LT)
           .put(Kind.FLOATINGPOINT_LEQ, FunctionDeclarationKind.FP_LE)
           .put(Kind.FLOATINGPOINT_GT, FunctionDeclarationKind.FP_GT)

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

@@ -602,6 +602,7 @@ private Term normalize(Term operator) {
           .put(Kind.FLOATINGPOINT_ADD, FunctionDeclarationKind.FP_ADD)
           .put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
           .put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)
+          .put(Kind.FLOATINGPOINT_REM, FunctionDeclarationKind.FP_REM)
           .put(Kind.FLOATINGPOINT_DIV, FunctionDeclarationKind.FP_DIV)
           .put(Kind.FLOATINGPOINT_NEG, FunctionDeclarationKind.FP_NEG)
           .put(Kind.FLOATINGPOINT_LT, FunctionDeclarationKind.FP_LT)

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

@@ -734,6 +734,8 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.FP_DIV;
       case Z3_OP_FPA_MUL:
         return FunctionDeclarationKind.FP_MUL;
+      case Z3_OP_FPA_REM:
+        return FunctionDeclarationKind.FP_REM;
       case Z3_OP_FPA_LT:
         return FunctionDeclarationKind.FP_LT;
       case Z3_OP_FPA_LE: