walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: use 'real' instead of 'fpa' values in latest Z3 for floats

This commit is contained in:
Daniel Marjamäki 2020-12-22 18:05:21 +01:00
parent 315892d991
commit a9e7974963
2 changed files with 4 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
lib/exprengine.cpp
View File

@ -1279,40 +1279,26 @@ public:
// these will be cleaner and hopefully more robust.
z3::expr z3_fp_const(const std::string &name) {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return context.fpa_const(name.c_str(), 11, 53);
#else
return context.real_const(name.c_str());
#endif
}
z3::expr z3_fp_val(long double value, std::string name) {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
(void)name;
return context.fpa_val(static_cast<double>(value));
#else
(void)value;
while (name.size() > 1 && (name.back() == 'f' || name.back() == 'F' || name.back() == 'l' || name.back() == 'L'))
name.erase(name.size() - 1);
return context.real_val(name.c_str());
#endif
}
bool z3_is_fp(z3::expr e) const {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return e.is_fpa();
#else
return e.is_real();
#endif
}
int floatSymbol = 0;
void z3_to_fp(z3::expr &e) {
if (e.is_int())
// TODO: Is there a better way to promote e?
e = z3_fp_const("f" + std::to_string(++floatSymbol));
e = z3::to_real(e);
}
z3::expr z3_int_val(int128_t value) {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
return context.int_val(int64_t(value));

2
test/testexprengine.cpp
View File

@ -838,7 +838,7 @@ private:
void floatValue5() { // float < int
const char code[] = "void foo(float f) { if (f < 1){} }";
const char expected[] = "(< $1 f1)\n" // TODO: The "f1" should be something like (float)1
const char expected[] = "(< $1 (to_real 1))\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "<"));
}