From ed900e44bb2411168b6368f906c7db108b709819 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 02:12:57 +0200 Subject: [PATCH 01/20] Rewrite several tests in FloatingPointFormulaManagerTest to improve performance by reusing the ProverEnvironment for all test values --- .../test/FloatingPointFormulaManagerTest.java | 123 +++++++++++------- 1 file changed, 77 insertions(+), 46 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index bb82895b27..d2b2da9f3c 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -21,6 +21,7 @@ import java.math.BigInteger; import java.util.List; import java.util.Random; +import java.util.function.Function; import org.junit.Before; import org.junit.Test; import org.sosy_lab.common.rationals.Rational; @@ -773,24 +774,46 @@ public void ieeeFpConversion() throws SolverException, InterruptedException { .isTautological(); } + /** + * Map the function over the input list and prove the returned assertions. + * + * @param f A function that takes values from the list and returns assertions + * @param args A list of arguments to the function + */ + private void proveForAll(Function f, List args) + throws InterruptedException, SolverException { + try (ProverEnvironment prover = context.newProverEnvironment()) { + for (T value : args) { + prover.push(); + prover.addConstraint(f.apply(value)); + assertThat(prover).isSatisfiable(); + prover.pop(); + } + } + } + @Test public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException { - for (float f : getListOfFloats()) { - checkBV2FP( - singlePrecType, - bvmgr.makeBitvector(32, Float.floatToRawIntBits(f)), - fpmgr.makeNumber(f, singlePrecType)); - } + proveForAll( + // makeFP(value.float) == fromBV(makeBV(value.bits)) + pFloat -> + fpmgr.equalWithFPSemantics( + fpmgr.makeNumber(pFloat, singlePrecType), + fpmgr.fromIeeeBitvector( + bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), singlePrecType)), + getListOfFloats()); } @Test public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedException { - for (double d : getListOfDoubles()) { - checkBV2FP( - doublePrecType, - bvmgr.makeBitvector(64, Double.doubleToRawLongBits(d)), - fpmgr.makeNumber(d, doublePrecType)); - } + proveForAll( + // makeFP(value.float) == fromBV(makeBV(value.bits)) + pDouble -> + fpmgr.equalWithFPSemantics( + fpmgr.makeNumber(pDouble, doublePrecType), + fpmgr.fromIeeeBitvector( + bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), doublePrecType)), + getListOfDoubles()); } @Test @@ -800,12 +823,13 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - for (float f : getListOfFloats()) { - checkFP2BV( - singlePrecType, - bvmgr.makeBitvector(32, Float.floatToRawIntBits(f)), - fpmgr.makeNumber(f, singlePrecType)); - } + proveForAll( + // makeBV(value.bits) == fromFP(makeFP(value.float)) + pFloat -> + bvmgr.equal( + bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), + fpmgr.toIeeeBitvector(fpmgr.makeNumber(pFloat, singlePrecType))), + getListOfFloats()); } @Test @@ -815,12 +839,13 @@ public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedExce .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - for (double d : getListOfDoubles()) { - checkFP2BV( - doublePrecType, - bvmgr.makeBitvector(64, Double.doubleToRawLongBits(d)), - fpmgr.makeNumber(d, doublePrecType)); - } + proveForAll( + // makeBV(value.bits) == fromFP(makeFP(value.float)) + pDouble -> + bvmgr.equal( + bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), + fpmgr.toIeeeBitvector(fpmgr.makeNumber(pDouble, doublePrecType))), + getListOfFloats()); } private List getListOfFloats() { @@ -1030,32 +1055,38 @@ public void failOnInvalidString() { @Test public void fpFrom32BitPattern() throws SolverException, InterruptedException { - for (float f : getListOfFloats()) { - int bits = Float.floatToRawIntBits(f); - int exponent = (bits >>> 23) & 0xFF; - int mantissa = bits & 0x7FFFFF; - boolean sign = bits < 0; // equal to: (bits >>> 31) & 0x1 - final FloatingPointFormula fpFromBv = - fpmgr.makeNumber( - BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); - final FloatingPointFormula fp = fpmgr.makeNumber(f, singlePrecType); - assertEqualsAsFormula(fpFromBv, fp); - } + proveForAll( + pFloat -> { + // makeFP(value.bits.sign, value.bits.exponent, value.bits.mantissa) = makeFP(value.float) + int bits = Float.floatToRawIntBits(pFloat); + int exponent = (bits >>> 23) & 0xFF; + int mantissa = bits & 0x7FFFFF; + boolean sign = bits < 0; // equal to: (bits >>> 31) & 0x1 + final FloatingPointFormula fpFromBv = + fpmgr.makeNumber( + BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); + final FloatingPointFormula fp = fpmgr.makeNumber(pFloat, singlePrecType); + return fpmgr.assignment(fpFromBv, fp); + }, + getListOfFloats()); } @Test public void fpFrom64BitPattern() throws SolverException, InterruptedException { - for (double d : getListOfDoubles()) { - long bits = Double.doubleToRawLongBits(d); - long exponent = (bits >>> 52) & 0x7FF; - long mantissa = bits & 0xFFFFFFFFFFFFFL; - boolean sign = bits < 0; // equal to: (doubleBits >>> 63) & 1; - final FloatingPointFormula fpFromBv = - fpmgr.makeNumber( - BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); - final FloatingPointFormula fp = fpmgr.makeNumber(d, doublePrecType); - assertEqualsAsFormula(fpFromBv, fp); - } + proveForAll( + // makeFP(value.bits.sign, value.bits.exponent, value.bits.mantissa) = makeFP(value.float) + pDouble -> { + long bits = Double.doubleToRawLongBits(pDouble); + long exponent = (bits >>> 52) & 0x7FF; + long mantissa = bits & 0xFFFFFFFFFFFFFL; + boolean sign = bits < 0; // equal to: (doubleBits >>> 63) & 1; + final FloatingPointFormula fpFromBv = + fpmgr.makeNumber( + BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); + final FloatingPointFormula fp = fpmgr.makeNumber(pDouble, doublePrecType); + return fpmgr.assignment(fpFromBv, fp); + }, + getListOfDoubles()); } @Test From cd607d08e0a26064296e6bd027d70984cf7ad7b9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 02:20:55 +0200 Subject: [PATCH 02/20] Revert "Reduce the number of test runs in FloatingPointFormulaManagerTest.checkIEEEFpConversion for Bitwuzla. The solver seems to have performance issues in this task." This reverts commit 2df60102 --- .../test/FloatingPointFormulaManagerTest.java | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index d2b2da9f3c..77eb87252b 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -869,17 +869,15 @@ private List getListOfFloats() { flts.add(-0.0f); // MathSat5 fails for NEGATIVE_ZERO } - final int stepSize = solverToUse() == Solvers.BITWUZLA ? 10 : 1; - for (int i = 1; i < 20; i += stepSize) { - for (int j = 1; j < 20; j += stepSize) { + for (int i = 1; i < 20; i++) { + for (int j = 1; j < 20; j++) { flts.add((float) (i * Math.pow(10, j))); flts.add((float) (-i * Math.pow(10, j))); } } - final int numRandom = solverToUse() == Solvers.BITWUZLA ? 5 : NUM_RANDOM_TESTS; Random rand = new Random(0); - for (int i = 0; i < numRandom; i++) { + for (int i = 0; i < NUM_RANDOM_TESTS; i++) { float flt = Float.intBitsToFloat(rand.nextInt()); if (!Float.isNaN(flt)) { flts.add(flt); @@ -908,17 +906,15 @@ private List getListOfDoubles() { dbls.add(-0.0); // MathSat5 fails for NEGATIVE_ZERO } - final int stepSize = solverToUse() == Solvers.BITWUZLA ? 10 : 1; - for (int i = 1; i < 20; i += stepSize) { - for (int j = 1; j < 20; j += stepSize) { + for (int i = 1; i < 20; i++) { + for (int j = 1; j < 20; j++) { dbls.add(i * Math.pow(10, j)); dbls.add(-i * Math.pow(10, j)); } } - final int numRandom = solverToUse() == Solvers.BITWUZLA ? 5 : NUM_RANDOM_TESTS; Random rand = new Random(0); - for (int i = 0; i < numRandom; i++) { + for (int i = 0; i < NUM_RANDOM_TESTS; i++) { double d = Double.longBitsToDouble(rand.nextLong()); if (!Double.isNaN(d)) { dbls.add(d); From d3b552990b037b89b171fd988a58daff6eae2afb Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 03:07:40 +0200 Subject: [PATCH 03/20] Bitwuzla: Add a performance hack for checkIeeeBv2FpConversion32 --- .../java_smt/test/FloatingPointFormulaManagerTest.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 77eb87252b..2a30d8cbbc 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -783,6 +783,11 @@ public void ieeeFpConversion() throws SolverException, InterruptedException { private void proveForAll(Function f, List args) throws InterruptedException, SolverException { try (ProverEnvironment prover = context.newProverEnvironment()) { + if (solverToUse().equals(Solvers.BITWUZLA)) { + // Adding this line speeds up performance in checkIeeeBv2FpConversion32 by a factor of 10 + // FIXME: I've no idea why this would work + prover.addConstraint(bmgr.makeTrue()); + } for (T value : args) { prover.push(); prover.addConstraint(f.apply(value)); From 19d1b1b3d1ccd6e108c40515cf9aaa25be925116 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 03:18:53 +0200 Subject: [PATCH 04/20] Bitwuzla: Add a note about the performance issue in checkIeeeFp2BvConversion32 --- .../java_smt/test/FloatingPointFormulaManagerTest.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 2a30d8cbbc..4297af3faa 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -828,6 +828,12 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); + // FIXME: This test is still painfully slow in Bitwuzla. Both fp2bv and bv2fp ultimately map + // to the same operation in Bitwuzla as we define "b = fp2bv(f)" by adding the + // side-condition "f = bv2fp(b)" to the constraints and then simply returning the new bitvector + // variable `b`. The slow down here seems to be related the side-conditions that have to be + // added to the assertions whenever isUnsat() is called. + proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) pFloat -> From 4137075ef701062b9dc53794608df4196d11271d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 03:20:41 +0200 Subject: [PATCH 05/20] Bitwuzla: Removed unused methods --- .../test/FloatingPointFormulaManagerTest.java | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 4297af3faa..affe4cde11 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -935,22 +935,6 @@ private List getListOfDoubles() { return dbls; } - private void checkBV2FP(FloatingPointType type, BitvectorFormula bv, FloatingPointFormula flt) - throws SolverException, InterruptedException { - FloatingPointFormula ieeeFp = fpmgr.fromIeeeBitvector(bv, type); - assertThat(mgr.getFormulaType(ieeeFp)).isEqualTo(mgr.getFormulaType(flt)); - assertEqualsAsFp(flt, ieeeFp); - } - - private void checkFP2BV(FloatingPointType type, BitvectorFormula bv, FloatingPointFormula flt) - throws SolverException, InterruptedException { - BitvectorFormula var = bvmgr.makeVariable(type.getTotalSize(), "x"); - BitvectorFormula ieeeBv = fpmgr.toIeeeBitvector(flt); - assertThat(mgr.getFormulaType(ieeeBv)).isEqualTo(mgr.getFormulaType(var)); - assertThatFormula(bvmgr.equal(bv, ieeeBv)).isTautological(); - assertThatFormula(bmgr.and(bvmgr.equal(bv, var), bvmgr.equal(var, ieeeBv))).isSatisfiable(); - } - @Test public void fpModelContent() throws SolverException, InterruptedException { FloatingPointFormula zeroVar = fpmgr.makeVariable("zero", singlePrecType); From b7aa1bb4a12f6438b8263f12011a30a6b33b826f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 09:22:10 +0200 Subject: [PATCH 06/20] Add the floating point remainder to FunctionDeclarationKind --- src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java | 3 +++ .../java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java | 2 ++ src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java | 1 + src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 1 + src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java | 2 ++ 5 files changed, 9 insertions(+) diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 16075fa10f..5da97bdaf6 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -213,6 +213,9 @@ public enum FunctionDeclarationKind { /** Division over floating points. */ FP_DIV, + /** Remainder of the floating point division */ + FP_REM, + /** Multiplication over floating points. */ FP_MUL, diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 5fa6cc9acf..6f3f239347 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -283,6 +283,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)) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 28a882d106..b272a8b09d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -487,6 +487,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) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 38d6f7fa48..aacf9140f6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -600,6 +600,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) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 8b57b86602..a7ab76d71e 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -726,6 +726,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: From 58f81f5443460da1e46ead24f68ed6addb8a9a95 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 09:45:29 +0200 Subject: [PATCH 07/20] Bitwuzla: Add support for FunctionDeclaration.LSHR --- .../java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 6f3f239347..df12a24ab5 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -221,6 +221,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)) { From fe43eaae96797e7d4bc6a84e701a9d491c2f5474 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 12:11:16 +0200 Subject: [PATCH 08/20] Bitwuzla: Use a global counter to make sure that the variables that are created for fp-to-bv casts are unique --- .../bitwuzla/BitwuzlaFloatingPointManager.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index 7765bfc2a2..aa6a1fcb03 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/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); @@ -198,9 +201,12 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType pTargetType.getMantissaSize() + 1); } + private String newVariable() { + return "__CAST_FROM_BV_" + counter++; + } + @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(); @@ -213,7 +219,8 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { 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"); + String newVariable = newVariable(); + Term bvVar = termManager.mk_const(bvSort, newVariable); Term equal = termManager.mk_term( Kind.ITE, From f704637c1598de5d5295409e5590ac3912709f45 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 12:12:05 +0200 Subject: [PATCH 09/20] Bitwuzla: Print "(assert true)" if the formula is `true` --- .../java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index 9a644f2b60..2404bb74a8 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -186,6 +186,10 @@ 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()) { bitwuzla.assert_formula(t); From 3ced9a9262f1a62e99d3ad6b39b92d9d323e49b8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 12:14:08 +0200 Subject: [PATCH 10/20] Bitwuzla: Improve the variableCasts map and make sure that we only push casts as side-conditions that are actually needed --- .../BitwuzlaFloatingPointManager.java | 2 +- .../bitwuzla/BitwuzlaFormulaCreator.java | 49 ++++++++++++++++--- .../bitwuzla/BitwuzlaFormulaManager.java | 2 +- .../bitwuzla/BitwuzlaTheoremProver.java | 19 +++++-- 4 files changed, 60 insertions(+), 12 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index aa6a1fcb03..3dbdcf42a7 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -231,7 +231,7 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { termManager.mk_term(Kind.FP_TO_FP_FROM_BV, bvVar, sizeExp, sizeSig), pNumber)); - bitwuzlaCreator.addVariableCast(equal); + bitwuzlaCreator.addVariableCast(newVariable, equal); return bvVar; } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index df12a24ab5..c0d5c1516b 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -13,12 +13,16 @@ import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Maps; +import com.google.common.collect.Sets; import com.google.common.collect.Table; import java.math.BigInteger; import java.util.ArrayList; -import java.util.HashSet; +import java.util.HashMap; import java.util.Iterator; import java.util.List; +import java.util.Map; import java.util.Map.Entry; import java.util.Optional; import java.util.Set; @@ -55,7 +59,7 @@ public class BitwuzlaFormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); - private final Set variableCasts = new HashSet<>(); + private final Map variableCasts = new HashMap<>(); protected BitwuzlaFormulaCreator(TermManager pTermManager) { super(null, pTermManager.mk_bool_sort(), null, null, null, null); @@ -568,11 +572,44 @@ public Object convertValue(Term term) { throw new AssertionError("Unknown value type."); } - public void addVariableCast(Term equal) { - variableCasts.add(equal); + public void addVariableCast(String newVariable, Term equal) { + variableCasts.put(newVariable, equal); } - public Iterable getVariableCasts() { - return variableCasts; + private Map> calculateTransitions(Map pVariableCasts) { + return Maps.transformValues( + pVariableCasts, + term -> + Sets.intersection( + pVariableCasts.keySet(), extractVariablesAndUFs(term, false).keySet())); + } + + private Set initialSet(Iterable pTerms) { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (Term term : pTerms) { + builder.addAll(extractVariablesAndUFs(term, false).keySet()); + } + return builder.build(); + } + + private Set takeAStep(Map> pTransitions, Set pVariables) { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (String var : pVariables) { + builder.addAll(pTransitions.get(var)); + } + return builder.build(); + } + + public Iterable getVariableCasts(Iterable pTerms) { + Map> transitions = calculateTransitions(variableCasts); + + Set r0 = ImmutableSet.of(); + Set r1 = Sets.intersection(initialSet(pTerms), transitions.keySet()); + while (!r0.equals(r1)) { + r0 = r1; + r1 = takeAStep(transitions, r0); + } + + return Maps.filterKeys(variableCasts, r0::contains).values(); } } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index 2404bb74a8..29aef66f86 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -191,7 +191,7 @@ public void appendTo(Appendable out) throws IOException { return; } Bitwuzla bitwuzla = new Bitwuzla(creator.getTermManager()); - for (Term t : creator.getVariableCasts()) { + for (Term t : creator.getVariableCasts(ImmutableList.of(pTerm))) { bitwuzla.assert_formula(t); } bitwuzla.assert_formula(pTerm); diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index 56ea0f8d2c..5a775b1aec 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -10,6 +10,7 @@ import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; +import com.google.common.collect.FluentIterable; import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -127,7 +128,8 @@ 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())); + Iterable assertions = env.get_assertions(); + final Result result = env.check_sat(new Vector_Term(creator.getVariableCasts(assertions))); return readSATResult(result); } @@ -142,12 +144,21 @@ public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); wasLastSatCheckSat = false; - Vector_Term ass = new Vector_Term(creator.getVariableCasts()); + + // Extract Terms from the assumptions + Vector_Term newAssumptions = new Vector_Term(); for (BooleanFormula formula : assumptions) { BitwuzlaBooleanFormula bitwuzlaFormula = (BitwuzlaBooleanFormula) formula; - ass.add(bitwuzlaFormula.getTerm()); + newAssumptions.add(bitwuzlaFormula.getTerm()); } - final Result result = env.check_sat(ass); + + // Collect side condition for any casts and add them to the assumptions + Iterable allAsserted = + FluentIterable.concat( + newAssumptions, + creator.getVariableCasts(FluentIterable.concat(env.get_assertions(), newAssumptions))); + + final Result result = env.check_sat(new Vector_Term(allAsserted)); return readSATResult(result); } From 33736b0f40b810173d2b8d73573ee23546f5fc5a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 12:27:06 +0200 Subject: [PATCH 11/20] Bitwuzla: Remove a note as the issue is now fixed --- .../java_smt/test/FloatingPointFormulaManagerTest.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index affe4cde11..1204ff1780 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -828,12 +828,6 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - // FIXME: This test is still painfully slow in Bitwuzla. Both fp2bv and bv2fp ultimately map - // to the same operation in Bitwuzla as we define "b = fp2bv(f)" by adding the - // side-condition "f = bv2fp(b)" to the constraints and then simply returning the new bitvector - // variable `b`. The slow down here seems to be related the side-conditions that have to be - // added to the assertions whenever isUnsat() is called. - proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) pFloat -> From 9b030f7c768ecdf4464e059ddc344bda9d11fbce Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 12:30:04 +0200 Subject: [PATCH 12/20] Bitwuzla: Add a missing dot --- src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 5da97bdaf6..31db681117 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -213,7 +213,7 @@ public enum FunctionDeclarationKind { /** Division over floating points. */ FP_DIV, - /** Remainder of the floating point division */ + /** Remainder of the floating point division. */ FP_REM, /** Multiplication over floating points. */ From 328a5ec0f7a27c860fcc5f57fc7b51c3b14d2f96 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Sep 2024 14:14:44 +0200 Subject: [PATCH 13/20] Bitwuzla: Patch handling of bitvector rotations in the formula visitor --- .../java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index c0d5c1516b..76d551ce66 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -313,6 +313,10 @@ private FunctionDeclarationKind getDeclarationKind(Term term) { return FunctionDeclarationKind.FP_CASTTO_UBV; } else if (kind.equals(Kind.BV_XOR)) { return FunctionDeclarationKind.BV_XOR; + } else if (ImmutableList.of(Kind.BV_ROL, Kind.BV_ROLI, Kind.BV_ROR, Kind.BV_RORI) + .contains(kind)) { + // Rotations are not yet supported by FunctionDeclarationKind + return FunctionDeclarationKind.OTHER; } throw new UnsupportedOperationException("Can not discern formula kind " + kind); } From 7d324801ba942679eaa878e95ca9113f21f492fc Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 19 Sep 2024 04:18:46 +0200 Subject: [PATCH 14/20] Bitwuzla: Push side-conditions for variable casts directly onto the stack to avoid recalculations --- .../bitwuzla/BitwuzlaTheoremProver.java | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index 5a775b1aec..aff3666297 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -11,6 +11,7 @@ import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableList; import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -93,8 +94,19 @@ public void popImpl() { @Override public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { + Term formula = ((BitwuzlaBooleanFormula) constraint).getTerm(); + + // Assert the formula + env.assert_formula(formula); + + // Collect side-conditions for all variable casts and push them onto the stack + for (Term t : creator.getVariableCasts(ImmutableList.of(formula))) { + env.assert_formula(t); + } + + // Set the state to 'changed' wasLastSatCheckSat = false; - env.assert_formula(((BitwuzlaBooleanFormula) constraint).getTerm()); + return null; } @@ -128,8 +140,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); wasLastSatCheckSat = false; - Iterable assertions = env.get_assertions(); - final Result result = env.check_sat(new Vector_Term(creator.getVariableCasts(assertions))); + final Result result = env.check_sat(); return readSATResult(result); } @@ -154,9 +165,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) // Collect side condition for any casts and add them to the assumptions Iterable allAsserted = - FluentIterable.concat( - newAssumptions, - creator.getVariableCasts(FluentIterable.concat(env.get_assertions(), newAssumptions))); + FluentIterable.concat(newAssumptions, creator.getVariableCasts(newAssumptions)); final Result result = env.check_sat(new Vector_Term(allAsserted)); return readSATResult(result); From 43905a85757a66ea194c839c2095acb9d3e043c9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 19 Sep 2024 04:19:00 +0200 Subject: [PATCH 15/20] Bitwuzla: Reuse the same stack frame in proveForAll() for all input formulas --- .../java_smt/test/FloatingPointFormulaManagerTest.java | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 1204ff1780..6be7780a30 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -783,16 +783,9 @@ public void ieeeFpConversion() throws SolverException, InterruptedException { private void proveForAll(Function f, List args) throws InterruptedException, SolverException { try (ProverEnvironment prover = context.newProverEnvironment()) { - if (solverToUse().equals(Solvers.BITWUZLA)) { - // Adding this line speeds up performance in checkIeeeBv2FpConversion32 by a factor of 10 - // FIXME: I've no idea why this would work - prover.addConstraint(bmgr.makeTrue()); - } for (T value : args) { - prover.push(); prover.addConstraint(f.apply(value)); assertThat(prover).isSatisfiable(); - prover.pop(); } } } From e5a22b2d07c1ba6fe5765fc6cf60601f2c0f9df0 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 20 Sep 2024 15:07:29 +0200 Subject: [PATCH 16/20] Bitwuzla: Add documentation for getVariableCasts() and the side-conditions in variableCasts --- .../bitwuzla/BitwuzlaFormulaCreator.java | 73 ++++++++++++------- 1 file changed, 47 insertions(+), 26 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 76d551ce66..4262e6cc47 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -59,6 +59,19 @@ public class BitwuzlaFormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); + /** + * Maps symbols from fp-to-bv casts to their defining equation. + * + *

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 + * __CAST_FROM_BV_XXXfor the result and then adding the constraint + * fp.to_fp(__CAST_FROM_BV_XXX) = <float-term> as a side-condition. This is also what + * is recommended by the SMT-LIB2 standard. The map variableCasts 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 variableCasts = new HashMap<>(); protected BitwuzlaFormulaCreator(TermManager pTermManager) { @@ -576,42 +589,50 @@ public Object convertValue(Term term) { throw new AssertionError("Unknown value type."); } + /** Add a side-condition from a fp-to-bv to the set. */ public void addVariableCast(String newVariable, Term equal) { variableCasts.put(newVariable, equal); } - private Map> calculateTransitions(Map pVariableCasts) { - return Maps.transformValues( - pVariableCasts, - term -> - Sets.intersection( - pVariableCasts.keySet(), extractVariablesAndUFs(term, false).keySet())); - } - - private Set initialSet(Iterable pTerms) { - ImmutableSet.Builder builder = ImmutableSet.builder(); + /** + * Returns a set of side-conditions that are needed to handle the variable casts in the terms. + * + *

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 Iterable getVariableCasts(Iterable pTerms) { + // Build the transition function from the side-conditions. We map the variables on the left + // side of the defining equation to the set of variables on the right side. + // f.ex __CAST_TO_BV_0 -> fp.to_fp(CAST_TO_BV_0) = (+ a b) + // becomes + // Map.of(__CAST_TO_BV, Set.of(__CAST_TO_BV, a b)) + Map> transitions = + Maps.transformValues( + variableCasts, + term -> + Sets.intersection( + variableCasts.keySet(), extractVariablesAndUFs(term, false).keySet())); + + // Calculate the initial set of symbols from the terms in the argument + ImmutableSet.Builder initBuilder = ImmutableSet.builder(); for (Term term : pTerms) { - builder.addAll(extractVariablesAndUFs(term, false).keySet()); - } - return builder.build(); - } - - private Set takeAStep(Map> pTransitions, Set pVariables) { - ImmutableSet.Builder builder = ImmutableSet.builder(); - for (String var : pVariables) { - builder.addAll(pTransitions.get(var)); + initBuilder.addAll(extractVariablesAndUFs(term, false).keySet()); } - return builder.build(); - } - - public Iterable getVariableCasts(Iterable pTerms) { - Map> transitions = calculateTransitions(variableCasts); + ImmutableSet initialSet = initBuilder.build(); Set r0 = ImmutableSet.of(); - Set r1 = Sets.intersection(initialSet(pTerms), transitions.keySet()); + Set r1 = Sets.intersection(initialSet, transitions.keySet()); + // Calculate the fixpoint for the transition function while (!r0.equals(r1)) { r0 = r1; - r1 = takeAStep(transitions, r0); + // Iterate the transition function + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (String var : r0) { + builder.addAll(transitions.get(var)); + } + r1 = builder.build(); } return Maps.filterKeys(variableCasts, r0::contains).values(); From 524cc641a3abfafceeca9f40c19e2dd870c089ee Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 20 Sep 2024 15:10:13 +0200 Subject: [PATCH 17/20] Changed order of arguments for proveForAll in FloatingPointFormulaManagerTest --- .../test/FloatingPointFormulaManagerTest.java | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 6be7780a30..33fc8e2acf 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -777,10 +777,10 @@ public void ieeeFpConversion() throws SolverException, InterruptedException { /** * Map the function over the input list and prove the returned assertions. * - * @param f A function that takes values from the list and returns assertions * @param args A list of arguments to the function + * @param f A function that takes values from the list and returns assertions */ - private void proveForAll(Function f, List args) + private void proveForAll(List args, Function f) throws InterruptedException, SolverException { try (ProverEnvironment prover = context.newProverEnvironment()) { for (T value : args) { @@ -794,24 +794,24 @@ private void proveForAll(Function f, List args) public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException { proveForAll( // makeFP(value.float) == fromBV(makeBV(value.bits)) + getListOfFloats(), pFloat -> fpmgr.equalWithFPSemantics( fpmgr.makeNumber(pFloat, singlePrecType), fpmgr.fromIeeeBitvector( - bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), singlePrecType)), - getListOfFloats()); + bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), singlePrecType))); } @Test public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedException { proveForAll( // makeFP(value.float) == fromBV(makeBV(value.bits)) + getListOfDoubles(), pDouble -> fpmgr.equalWithFPSemantics( fpmgr.makeNumber(pDouble, doublePrecType), fpmgr.fromIeeeBitvector( - bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), doublePrecType)), - getListOfDoubles()); + bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), doublePrecType))); } @Test @@ -823,11 +823,11 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) + getListOfFloats(), pFloat -> bvmgr.equal( bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), - fpmgr.toIeeeBitvector(fpmgr.makeNumber(pFloat, singlePrecType))), - getListOfFloats()); + fpmgr.toIeeeBitvector(fpmgr.makeNumber(pFloat, singlePrecType)))); } @Test @@ -839,11 +839,11 @@ public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedExce proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) + getListOfFloats(), pDouble -> bvmgr.equal( bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), - fpmgr.toIeeeBitvector(fpmgr.makeNumber(pDouble, doublePrecType))), - getListOfFloats()); + fpmgr.toIeeeBitvector(fpmgr.makeNumber(pDouble, doublePrecType)))); } private List getListOfFloats() { @@ -1034,6 +1034,7 @@ public void failOnInvalidString() { @Test public void fpFrom32BitPattern() throws SolverException, InterruptedException { proveForAll( + getListOfFloats(), pFloat -> { // makeFP(value.bits.sign, value.bits.exponent, value.bits.mantissa) = makeFP(value.float) int bits = Float.floatToRawIntBits(pFloat); @@ -1045,14 +1046,14 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); final FloatingPointFormula fp = fpmgr.makeNumber(pFloat, singlePrecType); return fpmgr.assignment(fpFromBv, fp); - }, - getListOfFloats()); + }); } @Test public void fpFrom64BitPattern() throws SolverException, InterruptedException { proveForAll( // makeFP(value.bits.sign, value.bits.exponent, value.bits.mantissa) = makeFP(value.float) + getListOfDoubles(), pDouble -> { long bits = Double.doubleToRawLongBits(pDouble); long exponent = (bits >>> 52) & 0x7FF; @@ -1063,8 +1064,7 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); final FloatingPointFormula fp = fpmgr.makeNumber(pDouble, doublePrecType); return fpmgr.assignment(fpFromBv, fp); - }, - getListOfDoubles()); + }); } @Test From 9718a1890743a4448bd89565d67de3bb84f6ce02 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 21 Sep 2024 15:01:36 +0200 Subject: [PATCH 18/20] Revert "Bitwuzla: Patch handling of bitvector rotations in the formula visitor" This reverts commit 328a5ec0f7a27c860fcc5f57fc7b51c3b14d2f96. --- .../java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 4262e6cc47..8468058b4f 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -326,10 +326,6 @@ private FunctionDeclarationKind getDeclarationKind(Term term) { return FunctionDeclarationKind.FP_CASTTO_UBV; } else if (kind.equals(Kind.BV_XOR)) { return FunctionDeclarationKind.BV_XOR; - } else if (ImmutableList.of(Kind.BV_ROL, Kind.BV_ROLI, Kind.BV_ROR, Kind.BV_RORI) - .contains(kind)) { - // Rotations are not yet supported by FunctionDeclarationKind - return FunctionDeclarationKind.OTHER; } throw new UnsupportedOperationException("Can not discern formula kind " + kind); } From d00c4c2a5801684edb45cfdfb5b675fa81986b45 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 21 Sep 2024 22:43:03 +0200 Subject: [PATCH 19/20] rewrite and simplify a fixed-point algorithm. The new approach has several improvements: - only analyse those constraints that are referenced in terms, - do not compare Sets for the fixed-point, but wait for an empty waitlist. --- .../BitwuzlaFloatingPointManager.java | 12 +++- .../bitwuzla/BitwuzlaFormulaCreator.java | 65 +++++++------------ .../bitwuzla/BitwuzlaFormulaManager.java | 2 +- .../bitwuzla/BitwuzlaTheoremProver.java | 31 +++------ 4 files changed, 46 insertions(+), 64 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index 3dbdcf42a7..5cc42f6ff6 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -212,6 +212,16 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { 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 @@ -231,7 +241,7 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { termManager.mk_term(Kind.FP_TO_FP_FROM_BV, bvVar, sizeExp, sizeSig), pNumber)); - bitwuzlaCreator.addVariableCast(newVariable, equal); + bitwuzlaCreator.addConstraintForVariable(newVariable, equal); return bvVar; } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 15dabe90e6..d231b49305 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -9,18 +9,20 @@ 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.ImmutableSet; -import com.google.common.collect.Maps; -import com.google.common.collect.Sets; import com.google.common.collect.Table; import java.math.BigInteger; +import java.util.ArrayDeque; import java.util.ArrayList; +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; @@ -60,7 +62,8 @@ public class BitwuzlaFormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); /** - * Maps symbols from fp-to-bv casts to their defining equation. + * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their + * defining equation. * *

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 @@ -72,7 +75,7 @@ public class BitwuzlaFormulaCreator extends FormulaCreator variableCasts = new HashMap<>(); + private final Map constraintsForVariables = new HashMap<>(); protected BitwuzlaFormulaCreator(TermManager pTermManager) { super(null, pTermManager.mk_bool_sort(), null, null, null, null); @@ -593,52 +596,34 @@ public Object convertValue(Term term) { throw new AssertionError("Unknown value type."); } - /** Add a side-condition from a fp-to-bv to the set. */ - public void addVariableCast(String newVariable, Term equal) { - variableCasts.put(newVariable, 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); } /** - * Returns a set of side-conditions that are needed to handle the variable casts in the terms. + * 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. * *

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 Iterable getVariableCasts(Iterable pTerms) { - // Build the transition function from the side-conditions. We map the variables on the left - // side of the defining equation to the set of variables on the right side. - // f.ex __CAST_TO_BV_0 -> fp.to_fp(CAST_TO_BV_0) = (+ a b) - // becomes - // Map.of(__CAST_TO_BV, Set.of(__CAST_TO_BV, a b)) - Map> transitions = - Maps.transformValues( - variableCasts, - term -> - Sets.intersection( - variableCasts.keySet(), extractVariablesAndUFs(term, false).keySet())); - - // Calculate the initial set of symbols from the terms in the argument - ImmutableSet.Builder initBuilder = ImmutableSet.builder(); - for (Term term : pTerms) { - initBuilder.addAll(extractVariablesAndUFs(term, false).keySet()); - } - ImmutableSet initialSet = initBuilder.build(); - - Set r0 = ImmutableSet.of(); - Set r1 = Sets.intersection(initialSet, transitions.keySet()); - // Calculate the fixpoint for the transition function - while (!r0.equals(r1)) { - r0 = r1; - // Iterate the transition function - ImmutableSet.Builder builder = ImmutableSet.builder(); - for (String var : r0) { - builder.addAll(transitions.get(var)); + public Collection getConstraintsForTerm(Term pTerm) { + final Set usedConstraintVariables = new LinkedHashSet<>(); + final Deque 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()); + } } - r1 = builder.build(); } - return Maps.filterKeys(variableCasts, r0::contains).values(); + return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get); } } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index 29aef66f86..df2cfaef0d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -191,7 +191,7 @@ public void appendTo(Appendable out) throws IOException { return; } Bitwuzla bitwuzla = new Bitwuzla(creator.getTermManager()); - for (Term t : creator.getVariableCasts(ImmutableList.of(pTerm))) { + for (Term t : creator.getConstraintsForTerm(pTerm)) { bitwuzla.assert_formula(t); } bitwuzla.assert_formula(pTerm); diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index aff3666297..5cd0448c2a 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -10,10 +10,9 @@ import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; -import com.google.common.collect.FluentIterable; -import com.google.common.collect.ImmutableList; import java.util.ArrayList; import java.util.Collection; +import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; @@ -26,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; @@ -94,19 +92,12 @@ public void popImpl() { @Override public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { - Term formula = ((BitwuzlaBooleanFormula) constraint).getTerm(); - - // Assert the formula + wasLastSatCheckSat = false; + Term formula = creator.extractInfo(constraint); env.assert_formula(formula); - - // Collect side-conditions for all variable casts and push them onto the stack - for (Term t : creator.getVariableCasts(ImmutableList.of(formula))) { + for (Term t : creator.getConstraintsForTerm(formula)) { env.assert_formula(t); } - - // Set the state to 'changed' - wasLastSatCheckSat = false; - return null; } @@ -156,18 +147,14 @@ public boolean isUnsatWithAssumptions(Collection assumptions) Preconditions.checkState(!closed); wasLastSatCheckSat = false; - // Extract Terms from the assumptions - Vector_Term newAssumptions = new Vector_Term(); + Collection newAssumptions = new LinkedHashSet<>(); for (BooleanFormula formula : assumptions) { - BitwuzlaBooleanFormula bitwuzlaFormula = (BitwuzlaBooleanFormula) formula; - newAssumptions.add(bitwuzlaFormula.getTerm()); + Term term = creator.extractInfo(formula); + newAssumptions.add(term); + newAssumptions.addAll(creator.getConstraintsForTerm(term)); } - // Collect side condition for any casts and add them to the assumptions - Iterable allAsserted = - FluentIterable.concat(newAssumptions, creator.getVariableCasts(newAssumptions)); - - final Result result = env.check_sat(new Vector_Term(allAsserted)); + final Result result = env.check_sat(new Vector_Term(newAssumptions)); return readSATResult(result); } From 467459e95e094dbf53d023343df765d86f8da318 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 22 Sep 2024 12:54:24 +0200 Subject: [PATCH 20/20] change name of utility variable and document it. --- .../bitwuzla/BitwuzlaFloatingPointManager.java | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index 5cc42f6ff6..b9c708d261 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -201,10 +201,6 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType pTargetType.getMantissaSize() + 1); } - private String newVariable() { - return "__CAST_FROM_BV_" + counter++; - } - @Override protected Term toIeeeBitvectorImpl(Term pNumber) { int sizeExp = pNumber.sort().fp_exp_size(); @@ -225,11 +221,13 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { // 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)); + // 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); - String newVariable = newVariable(); + // 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(