From 8e79a6195b3c43fdd1bbc62360229a4a68bcb793 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 18:40:06 +0200 Subject: [PATCH 1/8] Replace generic implementation of fromIeeeBitvectorImpl() with CVC4 native implementation --- .../cvc4/CVC4FloatingPointFormulaManager.java | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index 248f6a55a8..d43a93b950 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -17,6 +17,7 @@ import edu.stanford.CVC4.FloatingPointConvertSort; import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FloatingPointToFPFloatingPoint; +import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector; import edu.stanford.CVC4.FloatingPointToFPSignedBitVector; import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector; import edu.stanford.CVC4.FloatingPointToSBV; @@ -358,20 +359,10 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); - Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); - Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); - - Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); - Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); - Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); - - return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); + // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP + FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType)); + Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort)); + return exprManager.mkExpr(op, bitvector); } @Override From 52f7a933ea27011af6106406c083d6db2fbd184b Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 18:43:13 +0200 Subject: [PATCH 2/8] Replace generic implementation of fromIeeeBitvectorImpl() with CVC5 native implementation --- .../cvc5/CVC5FloatingPointFormulaManager.java | 31 ++++++------------- 1 file changed, 10 insertions(+), 21 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 883a8a1f8a..59624962ff 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -408,29 +408,18 @@ protected Term isNegative(Term pParam) { } @Override - protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Op signExtract; - Op exponentExtract; - Op mantissaExtract; + protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { try { - signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); - } catch (CVC5ApiException e) { - throw new IllegalArgumentException( - "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); + return termManager.mkTerm( + termManager.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + pTargetType.getExponentSize(), + pTargetType.getMantissaSize() + 1), // add sign bit + pBitvector); + } catch (CVC5ApiException pE) { + // This seems to only be thrown for wrong exponent and mantissa sizes + throw new RuntimeException(pE); } - - Term sign = termManager.mkTerm(signExtract, bitvector); - Term exponent = termManager.mkTerm(exponentExtract, bitvector); - Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); - - return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); } @Override From 4ad6477e351fbcfba4c4e5cc305390817defbd09 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 18:43:21 +0200 Subject: [PATCH 3/8] Format --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index d43a93b950..1dbf7f7821 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -10,7 +10,6 @@ import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.BitVector; -import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.FloatingPoint; From 38ba5d2fb1b90adc0b11bcf1e6506b6704dcfaeb Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 14:17:33 +0200 Subject: [PATCH 4/8] Rename exception because of checkstyle --- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 59624962ff..6869a3d079 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -416,9 +416,9 @@ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetT pTargetType.getExponentSize(), pTargetType.getMantissaSize() + 1), // add sign bit pBitvector); - } catch (CVC5ApiException pE) { + } catch (CVC5ApiException pCVC5ApiException) { // This seems to only be thrown for wrong exponent and mantissa sizes - throw new RuntimeException(pE); + throw new RuntimeException(pCVC5ApiException); } } From 06fb659eca7c8618902f73e013514f78c72205b6 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:55:14 +0200 Subject: [PATCH 5/8] Change exception name in fromIeeeBitvectorImpl() again because of checkstyle :D --- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 6869a3d079..85f1afbe2d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -416,9 +416,9 @@ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetT pTargetType.getExponentSize(), pTargetType.getMantissaSize() + 1), // add sign bit pBitvector); - } catch (CVC5ApiException pCVC5ApiException) { + } catch (CVC5ApiException cvc5ApiException) { // This seems to only be thrown for wrong exponent and mantissa sizes - throw new RuntimeException(pCVC5ApiException); + throw new RuntimeException(cvc5ApiException); } } From 54ebac4dc20888840f2d492e1843829dcb930aea Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 14:34:03 +0200 Subject: [PATCH 6/8] Add default type sizes check for fromIeeeBitvector() --- .../basicimpl/AbstractFloatingPointFormulaManager.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 47c847afe2..f97215c3d9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -24,6 +24,7 @@ import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; /** @@ -245,6 +246,11 @@ protected abstract TFormulaInfo castFromImpl( @Override public FloatingPointFormula fromIeeeBitvector( BitvectorFormula pNumber, FloatingPointType pTargetType) { + BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber); + Preconditions.checkArgument( + bvType.getSize() == pTargetType.getTotalSize(), + "The total size of the used FloatingPointType has to match the size of the bitvector" + + " given"); return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType)); } From 126e8189c32f2bf9dc6f6aa0ce0543954b04f5a4 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 15:01:51 +0200 Subject: [PATCH 7/8] Improve default type sizes check error msg for fromIeeeBitvector() and add more info about CVC5 exception for the same method --- .../basicimpl/AbstractFloatingPointFormulaManager.java | 9 +++++++-- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 4 +++- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index f97215c3d9..e52dd2e697 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -15,6 +15,7 @@ import java.math.BigInteger; import java.util.HashMap; import java.util.Map; +import org.sosy_lab.common.MoreStrings; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -249,8 +250,12 @@ public FloatingPointFormula fromIeeeBitvector( BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber); Preconditions.checkArgument( bvType.getSize() == pTargetType.getTotalSize(), - "The total size of the used FloatingPointType has to match the size of the bitvector" - + " given"); + MoreStrings.lazyString( + () -> + String.format( + "The total size of the used FloatingPointType %s has to match the size of " + + "the bitvector argument %s", + pTargetType.getTotalSize(), bvType.getSize()))); return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType)); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 85f1afbe2d..83e0a2a6ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -417,7 +417,9 @@ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetT pTargetType.getMantissaSize() + 1), // add sign bit pBitvector); } catch (CVC5ApiException cvc5ApiException) { - // This seems to only be thrown for wrong exponent and mantissa sizes + // This seems to only be thrown for wrong exponent and mantissa sizes (e.g. negative + // numbers, size not equal to BV size etc.). We check for this beforehand, so this should + // not be thrown. throw new RuntimeException(cvc5ApiException); } } From 1c091804ae3bac5c288b0b10b2dfccdce1563de8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 15:06:23 +0200 Subject: [PATCH 8/8] Make exception thrown by CVC5 in fromIeeeBitvectorImpl() a IllegalArgumentException, as it fits better --- .../java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 83e0a2a6ec..34b895cec6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -420,7 +420,7 @@ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetT // This seems to only be thrown for wrong exponent and mantissa sizes (e.g. negative // numbers, size not equal to BV size etc.). We check for this beforehand, so this should // not be thrown. - throw new RuntimeException(cvc5ApiException); + throw new IllegalArgumentException(cvc5ApiException); } }