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

Merged
merged 11 commits into from
Nov 9, 2025
Merged

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

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
11 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
2ec4fce
Merge remote-tracking branch 'origin/master' into use_solver_native_b…
kfriedberger Nov 9, 2025
7b78a86
FP: improve error message and add test for it.
kfriedberger Nov 9, 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
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
31 changes: 10 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,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 cvc5ApiException) {
// This seems to only be thrown for wrong exponent and mantissa sizes
throw new RuntimeException(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