mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

FPA: bugfix for model completion. Thanks to Levent Erkok.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-04-02 13:45:42 +01:00
parent cbb4c12191
commit 4c353ec720
3 changed files with 22 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/float_decl_plugin.cpp
View file

@ -491,6 +491,15 @@ void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbo
sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
} }
expr * float_decl_plugin::get_some_value(sort * s) {
SASSERT(s->is_sort_of(m_family_id, FLOAT_SORT));
mpf tmp;
m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
expr * res = this->mk_value(tmp);
m_fm.del(tmp);
return res;
}
bool float_decl_plugin::is_value(app * e) const { bool float_decl_plugin::is_value(app * e) const {
if (e->get_family_id() != m_family_id) if (e->get_family_id() != m_family_id)
return false; return false;

1
src/ast/float_decl_plugin.h
View file

@ -140,6 +140,7 @@ public:
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic); virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic); virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual expr * get_some_value(sort * s);
virtual bool is_value(app* e) const; virtual bool is_value(app* e) const;
virtual bool is_unique_value(app* e) const { return is_value(e); } virtual bool is_unique_value(app* e) const { return is_value(e); }

19
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -1263,6 +1263,9 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
expr * x = args[0], * y = args[1]; expr * x = args[0], * y = args[1];
TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl;
tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
mk_is_nan(x, x_is_nan); mk_is_nan(x, x_is_nan);
mk_is_nan(y, y_is_nan); mk_is_nan(y, y_is_nan);
@ -1290,6 +1293,8 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
m_simp.mk_ite(c2, m.mk_true(), c3t4, c2else); m_simp.mk_ite(c2, m.mk_true(), c3t4, c2else);
m_simp.mk_ite(c1, m.mk_false(), c2else, result); m_simp.mk_ite(c1, m.mk_false(), c2else, result);
TRACE("fpa2bv_float_eq", tout << "FLOAT_EQ = " << mk_ismt2_pp(result, m) << std::endl; );
} }
void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -2314,9 +2319,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
unsigned ebits = fu.get_ebits(var->get_range()); unsigned ebits = fu.get_ebits(var->get_range());
unsigned sbits = fu.get_sbits(var->get_range()); unsigned sbits = fu.get_sbits(var->get_range());
expr * sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl()); expr_ref sgn(m), sig(m), exp(m);
expr * sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
expr * exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
seen.insert(to_app(a->get_arg(0))->get_decl()); seen.insert(to_app(a->get_arg(0))->get_decl());
seen.insert(to_app(a->get_arg(1))->get_decl()); seen.insert(to_app(a->get_arg(1))->get_decl());
@ -2385,12 +2391,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz; i++)
{ {
func_decl * c = bv_mdl->get_constant(i); func_decl * c = bv_mdl->get_constant(i);
if (seen.contains(c)) if (!seen.contains(c))
continue; float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
} }
// And keep everything else // And keep everything else
sz = bv_mdl->get_num_functions(); sz = bv_mdl->get_num_functions();
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz; i++)
{ {