From f78e595b566cbb9d6f5d55311a046268dd97c98c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 1 Dec 2012 15:51:33 +0000 Subject: [PATCH] Added QF_FPABV logic, default tactic, and the asIEEEBV conversion function. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 30 +++++++++++-- src/ast/float_decl_plugin.h | 9 +++- src/ast/rewriter/float_rewriter.cpp | 5 +++ src/ast/rewriter/float_rewriter.h | 2 + src/cmd_context/cmd_context.cpp | 6 ++- src/tactic/fpa/fpa2bv_converter.cpp | 45 +++++++++++++++++-- src/tactic/fpa/fpa2bv_converter.h | 1 + src/tactic/fpa/fpa2bv_rewriter.h | 1 + src/tactic/fpa/qffpa_tactic.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 1 + 10 files changed, 90 insertions(+), 11 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 7cf8f32bd..dbe7d5232 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -348,13 +348,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float! sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to asFloat"); - if (arity != 2 && arity != 3) + if (arity != 2 && arity != 3) m_manager->raise_exception("invalid number of arguments to asFloat operator"); if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) m_manager->raise_exception("sort mismatch"); @@ -373,6 +373,23 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, } } +func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support"); + if (arity != 1) + m_manager->raise_exception("invalid number of arguments to asIEEEBV"); + if (!is_float_sort(domain[0])) + m_manager->raise_exception("sort mismatch"); + + // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector. + unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); + parameter ps[] = { parameter(float_sz) }; + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); + symbol name("asIEEEBV"); + return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -420,6 +437,8 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_FUSED_MA: return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); + case OP_TO_IEEE_BV: + return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -462,7 +481,10 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); + op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); + + if (m_bv_plugin) + op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 416275306..c4503349b 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -67,6 +67,7 @@ enum float_op_kind { OP_FLOAT_IS_SIGN_MINUS, OP_TO_FLOAT, + OP_TO_IEEE_BV, LAST_FLOAT_OP }; @@ -118,6 +119,8 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); @@ -159,7 +162,7 @@ class float_util { ast_manager & m_manager; float_decl_plugin * m_plugin; family_id m_fid; - arith_util m_a_util; + arith_util m_a_util; public: float_util(ast_manager & m); ~float_util(); @@ -209,7 +212,7 @@ public: bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); } - app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); } + app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); } app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); } app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); } app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); } @@ -238,6 +241,8 @@ public: app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); } + + app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); } }; #endif diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index ad0709423..9678af216 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -59,6 +59,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; + case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } return st; } @@ -439,3 +440,7 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result return BR_FAILED; } + +br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index e4258895d..7c86a5bc3 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -67,6 +67,8 @@ public: br_status mk_is_nzero(expr * arg1, expr_ref & result); br_status mk_is_pzero(expr * arg1, expr_ref & result); br_status mk_is_sign_minus(expr * arg1, expr_ref & result); + + br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); }; #endif diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index afcac48ac..9ec11d085 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -460,6 +460,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "LIA" || s == "LRA" || s == "QF_FPA" || + s == "QF_FPABV" || s == "HORN"; } @@ -478,6 +479,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_ABV" || s == "QF_AUFBV" || s == "QF_BVRE" || + s == "QF_FPABV" || s == "HORN"; } @@ -502,7 +504,7 @@ bool cmd_context::logic_has_seq() const { } bool cmd_context::logic_has_floats() const { - return !has_logic() || m_logic == "QF_FPA"; + return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV"; } bool cmd_context::logic_has_array_core(symbol const & s) const { @@ -599,7 +601,7 @@ bool cmd_context::supported_logic(symbol const & s) const { logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || logic_has_horn(s) || - s == "QF_FPA"; + s == "QF_FPA" || s == "QF_FPABV"; } void cmd_context::set_logic(symbol const & s) { diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 77ff50e9b..21d5a2d23 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1399,6 +1399,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a } } +void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + expr * sgn, * s, * e; + split(args[0], sgn, s, e); + result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, s), e); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); @@ -2035,7 +2042,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { tout << bv_mdl->get_constant(i)->get_name() << " --> " << mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; ); - + + obj_hashtable seen; for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); @@ -2053,6 +2061,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { 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()); + 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(2))->get_decl()); + if (!sgn && !sig && !exp) continue; @@ -2080,7 +2092,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); float_mdl->register_decl(var, fu.mk_value(fp_val)); - + mpzm.del(sig_z); } @@ -2104,9 +2116,36 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; case BV_RM_TO_ZERO: default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); - } + } + seen.insert(var); } } fu.fm().del(fp_val); + + // Keep all the non-float constants. + unsigned sz = bv_mdl->get_num_constants(); + 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)); + } + + // And keep everything else + sz = bv_mdl->get_num_functions(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * c = bv_mdl->get_function(i); + float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + } + + sz = bv_mdl->get_num_uninterpreted_sorts(); + for (unsigned i = 0; i < sz; i++) + { + sort * s = bv_mdl->get_uninterpreted_sort(i); + ptr_vector u = bv_mdl->get_universe(s); + float_mdl->register_usort(s, u.size(), u.c_ptr()); + } } diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 291120e92..1ee374941 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -100,6 +100,7 @@ public: void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); fpa2bv_model_converter * mk_model_converter(); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 62c6f1a2d..91682c6e1 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -129,6 +129,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; + case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 660565463..8ca2183c1 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -27,6 +27,7 @@ class tactic; tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("qffpa", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffpa_tactic(m, p)") + ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ #endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 4cf530b1e..7a274a830 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -79,6 +79,7 @@ static void init(strategic_solver * s) { s->set_tactic_for(symbol("UFBV"), alloc(ufbv_fct)); s->set_tactic_for(symbol("BV"), alloc(ufbv_fct)); s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct)); + s->set_tactic_for(symbol("QF_FPABV"), alloc(qffpa_fct)); s->set_tactic_for(symbol("HORN"), alloc(horn_fct)); }