From 4c353ec7204a6a16f9b87eb1bbae694db40076cb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Apr 2013 13:45:42 +0100 Subject: [PATCH] FPA: bugfix for model completion. Thanks to Levent Erkok. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 9 +++++++++ src/ast/float_decl_plugin.h | 1 + src/tactic/fpa/fpa2bv_converter.cpp | 19 ++++++++++++------- 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 62ec3a4cf..26131bc28 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -491,6 +491,15 @@ void float_decl_plugin::get_sort_names(svector & sort_names, symbo 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 { if (e->get_family_id() != m_family_id) return false; diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 6f1ef5ec2..4ec17addf 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -140,6 +140,7 @@ public: unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); virtual void get_sort_names(svector & sort_names, symbol const & logic); + virtual expr * get_some_value(sort * s); virtual bool is_value(app* e) const; virtual bool is_unique_value(app* e) const { return is_value(e); } diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 79f86ac46..838090045 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -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]; + 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); mk_is_nan(x, x_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(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) { @@ -2314,9 +2319,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { unsigned ebits = fu.get_ebits(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 * sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); - expr * exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); + expr_ref sgn(m), sig(m), exp(m); + sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->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(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++) { func_decl * c = bv_mdl->get_constant(i); - if (seen.contains(c)) - continue; - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + if (!seen.contains(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(); for (unsigned i = 0; i < sz; i++) {