Skip to content

Commit 5cc1648

Browse files
committed
SMT2 parser: implement fp.to_sbv and fp.to_ubv
This adds fp.to_sbv and fp.to_ubv to the SMT-LIB2 parser.
1 parent bc8e2c6 commit 5cc1648

File tree

5 files changed

+31
-4
lines changed

5 files changed

+31
-4
lines changed

regression/cbmc/Float-no-simp2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-cprover-smt-backend
1+
CORE
22
main.c
33
--floatbv --no-simplify
44
^EXIT=0$

regression/cbmc/Float-to-int1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE broken-z3-smt-backend
22
main.c
33
--floatbv
44
^EXIT=0$

regression/cbmc/Float-to-int2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv
44
^EXIT=0$

regression/cbmc/Float-to-int3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE broken-z3-smt-backend
22
main.c
33
--floatbv
44
^EXIT=0$

src/solvers/smt2/smt2_parser.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -836,6 +836,33 @@ exprt smt2_parsert::function_application()
836836
throw error()
837837
<< "unexpected sort given as operand to to_fp_unsigned";
838838
}
839+
else if(id == "fp.to_sbv" || id == "fp.to_ubv")
840+
{
841+
// These are indexed by the number of bits of the result.
842+
if(next_token() != smt2_tokenizert::NUMERAL)
843+
throw error() << "expected number after " << id;
844+
845+
auto width = std::stoll(smt2_tokenizer.get_buffer());
846+
847+
if(next_token() != smt2_tokenizert::CLOSE)
848+
throw error() << "expected ')' after " << id;
849+
850+
auto op = operands();
851+
852+
if(op.size() != 2)
853+
throw error() << id << " takes two operands";
854+
855+
if(op[1].type().id() != ID_floatbv)
856+
throw error() << id << " takes a FloatingPoint operand";
857+
858+
if(id == "fp.to_sbv")
859+
return typecast_exprt(
860+
floatbv_typecast_exprt(op[1], op[0], signedbv_typet(width)),
861+
unsignedbv_typet(width));
862+
else
863+
return floatbv_typecast_exprt(
864+
op[1], op[0], unsignedbv_typet(width));
865+
}
839866
else
840867
{
841868
throw error() << "unknown indexed identifier '"

0 commit comments

Comments
 (0)