From 4c353ec7204a6a16f9b87eb1bbae694db40076cb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Apr 2013 13:45:42 +0100 Subject: [PATCH 1/3] 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++) { From 67e9d746533b1fe81a8de567b1d9644c7c5be688 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Apr 2013 09:44:31 -0700 Subject: [PATCH 2/3] constify a few functions Signed-off-by: Nuno Lopes --- src/ast/bv_decl_plugin.cpp | 4 ++-- src/ast/bv_decl_plugin.h | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 0ef3b60d6..8b77244f9 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -766,7 +766,7 @@ bool bv_recognizers::is_zero(expr const * n) const { return decl->get_parameter(0).get_rational().is_zero(); } -bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) { +bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) const { if (!is_extract(e)) return false; low = get_extract_low(e); high = get_extract_high(e); @@ -774,7 +774,7 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex return true; } -bool bv_recognizers::is_bv2int(expr const* e, expr*& r) { +bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const { if (!is_bv2int(e)) return false; r = to_app(e)->get_arg(0); return true; diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 8ea90f844..c5ebfb2d9 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -288,10 +288,10 @@ public: bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); } unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); } unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); } - unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); } - unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); } - bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b); - bool is_bv2int(expr const * e, expr * & r); + unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); } + unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); } + bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const; + bool is_bv2int(expr const * e, expr * & r) const; bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); } bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); } bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); } From 1c96a7d52f48b42891e5f40fa47e0b38c77a0b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2013 15:51:09 -0700 Subject: [PATCH 3/3] Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option. Signed-off-by: Leonardo de Moura --- src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_bv_params.cpp | 1 + src/util/gparams.cpp | 1 + 3 files changed, 3 insertions(+) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 43dd1b586..21b5c6281 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -29,6 +29,7 @@ def_module_params(module_name='smt', ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'), ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'), ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), + ('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index c2a31c59d..d3f386ab4 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -22,4 +22,5 @@ Revision History: void theory_bv_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); m_bv_reflect = p.bv_reflect(); + m_bv_enable_int2bv2int = p.bv_enable_int2bv(); } diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 8b1fbe40e..3b2e8edc1 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -49,6 +49,7 @@ char const * g_params_renames[] = { "restart_factor", "smt.restart_factor", "arith_random_initial_value", "smt.arith.random_initial_value", "bv_reflect", "smt.bv.reflect", + "bv_enable_int2bv_propagation", "smt.bv.enable_int2bv", "qi_cost", "smt.qi.cost", "qi_eager_threshold", "smt.qi.eager_threshold", "nl_arith", "smt.arith.nl",