Skip to content

Commit 9efd7a4

Browse files
committed
SMT back-end: implement float to bitvector conversion
Implement what the comment said by creating an appropriate symbol via `find_symbols`.
1 parent bb5433f commit 9efd7a4

File tree

1 file changed

+33
-4
lines changed

1 file changed

+33
-4
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 33 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2687,10 +2687,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
26872687

26882688
if(use_FPA_theory)
26892689
{
2690-
// This conversion is non-trivial as it requires creating a
2691-
// new bit-vector variable and then asserting that it converts
2692-
// to the required floating-point number.
2693-
SMT2_TODO("bit-wise floatbv to bv");
2690+
defined_expressionst::const_iterator it =
2691+
defined_expressions.find(expr);
2692+
CHECK_RETURN(it != defined_expressions.end());
2693+
out << it->second;
26942694
}
26952695
else
26962696
{
@@ -5440,6 +5440,35 @@ void smt2_convt::find_symbols(const exprt &expr)
54405440
out << ")\n"; // define-fun
54415441
}
54425442
}
5443+
else if(
5444+
use_FPA_theory && expr.id() == ID_typecast &&
5445+
to_typecast_expr(expr).op().type().id() == ID_floatbv &&
5446+
expr.type().id() == ID_bv)
5447+
{
5448+
// This is _NOT_ a semantic conversion, but bit-wise.
5449+
if(defined_expressions.find(expr) == defined_expressions.end())
5450+
{
5451+
// This conversion is non-trivial as it requires creating a
5452+
// new bit-vector variable and then asserting that it converts
5453+
// to the required floating-point number.
5454+
const irep_idt id =
5455+
"bvfromfloat." + std::to_string(defined_expressions.size());
5456+
out << "(declare-fun " << id << " () ";
5457+
convert_type(expr.type());
5458+
out << ')' << '\n';
5459+
5460+
const typecast_exprt &tc = to_typecast_expr(expr);
5461+
const auto &floatbv_type = to_floatbv_type(tc.op().type());
5462+
out << "(assert (= ";
5463+
out << "((_ to_fp " << floatbv_type.get_e() << " "
5464+
<< floatbv_type.get_f() + 1 << ") " << id << ')';
5465+
convert_expr(tc.op());
5466+
out << ')'; // =
5467+
out << ')' << '\n';
5468+
5469+
defined_expressions[expr] = id;
5470+
}
5471+
}
54435472
else if(expr.id() == ID_initial_state)
54445473
{
54455474
irep_idt function = "initial-state";

0 commit comments

Comments
 (0)