Skip to content

Use Solver Native Implementation of Bitvector to IEEE FP for CVC4 and CVC5 #514

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Use Solver Native Implementation of Bitvector to IEEE FP for CVC4 and CVC5 #514

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
8e79a61
Replace generic implementation of fromIeeeBitvectorImpl() with CVC4 n…
Sep 2, 2025
52f7a93
Replace generic implementation of fromIeeeBitvectorImpl() with CVC5 n…
Sep 2, 2025
4ad6477
Format
Sep 2, 2025
38ba5d2
Rename exception because of checkstyle
Sep 3, 2025
06fb659
Change exception name in fromIeeeBitvectorImpl() again because of che…
Sep 3, 2025
54ebac4
Add default type sizes check for fromIeeeBitvector()
Sep 5, 2025
126e818
Improve default type sizes check error msg for fromIeeeBitvector() an…
Sep 5, 2025
1c09180
Make exception thrown by CVC5 in fromIeeeBitvectorImpl() a IllegalArg…
Sep 5, 2025
f6e8248
Merge branch 'master' into use_solver_native_bv_to_ieee-fp_CVC4_CVC5
Sep 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -24,6 +25,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;

/**
Expand Down Expand Up @@ -245,6 +247,15 @@ protected abstract TFormulaInfo castFromImpl(
@Override
public FloatingPointFormula fromIeeeBitvector(
BitvectorFormula pNumber, FloatingPointType pTargetType) {
BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber);
Preconditions.checkArgument(
bvType.getSize() == pTargetType.getTotalSize(),
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));
}

Expand Down
20 changes: 5 additions & 15 deletions src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,13 @@

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;
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;
Expand Down Expand Up @@ -358,20 +358,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
Expand Down
33 changes: 12 additions & 21 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -408,29 +408,20 @@ 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 cvc5ApiException) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We catch other CVC5ApiExceptions as IllegalStateException, because it shows a bug in JavaSMT or a missed illegal usage of the API. Can we replace this plain RuntimeException?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good question!

The documentation of CVC5 is a little sparse when it comes to the reason why exceptions are thrown:

/**
   * Create operator of Kind:
   * <ul>
   *   <li>BITVECTOR_EXTRACT</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_IEEE_BV</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_FP</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_REAL</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_SBV</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_UBV</li>
   * </ul>
   * See enum {@link Kind} for a description of the parameters.
   * @param kind The kind of the operator.
   * @param arg1 The first unsigned int argument to this operator.
   * @param arg2 The second unsigned int argument to this operator.
   * @return The operator.
   * @throws CVC5ApiException on error
   */

However, from the code it is clear that the reasons can be negative integer input, and whatever exception is thrown by native code is also thrown in the JNI wrapper. The native code checks that the given FP size arguments fit the bitvector size as far as i can see. We could/should just check the given FP precision against the BV size ourselves, and this exception is never thrown.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added a default check for the used sizes and extended the documentation in CVC5 and switched to an IllegalArgumentException.

// 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 IllegalArgumentException(cvc5ApiException);
}

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
Expand Down