From 2087c01cacce68e171d8a153bc0af78e719b3259 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Oct 2020 07:18:36 -0700 Subject: [PATCH] first cut of fpa solver Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/bv2fpa_converter.h | 19 ++ src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/fpa_solver.cpp | 477 +++++++++++++++++++++++++++++++++ src/sat/smt/fpa_solver.h | 74 +++++ src/sat/smt/sat_th.cpp | 23 ++ src/sat/smt/sat_th.h | 4 + src/smt/theory_fpa.cpp | 34 +-- 7 files changed, 601 insertions(+), 31 deletions(-) create mode 100644 src/sat/smt/fpa_solver.cpp create mode 100644 src/sat/smt/fpa_solver.h diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h index 6a9499fc6..f533bcffc 100644 --- a/src/ast/fpa/bv2fpa_converter.h +++ b/src/ast/fpa/bv2fpa_converter.h @@ -18,6 +18,7 @@ Notes: --*/ #pragma once +#include "util/trail.h" #include "ast/fpa_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" @@ -69,3 +70,21 @@ public: array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f); }; +template +class fpa2bv_conversion_trail_elem : public trail { + ast_manager& m; + obj_map& m_map; + expr_ref key; +public: + fpa2bv_conversion_trail_elem(ast_manager& m, obj_map& map, expr* e) : + m(m), m_map(map), key(e, m) { } + ~fpa2bv_conversion_trail_elem() override { } + void undo(T& s) override { + expr* val = m_map.find(key); + m_map.remove(key); + m.dec_ref(key); + m.dec_ref(val); + key = nullptr; + } +}; + diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index bc8a9bc96..12c522a70 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -23,6 +23,7 @@ z3_add_component(sat_smt euf_proof.cpp euf_relevancy.cpp euf_solver.cpp + fpa_solver.cpp q_mbi.cpp q_model_finder.cpp q_solver.cpp diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp new file mode 100644 index 000000000..dcee1e63c --- /dev/null +++ b/src/sat/smt/fpa_solver.cpp @@ -0,0 +1,477 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + fpa_solver.cpp + +Abstract: + + Floating-Point Theory Plugin + +Author: + + Christoph (cwinter) 2014-04-23 + +Revision History: + +--*/ + +#include "sat/smt/fpa_solver.h" + +namespace fpa { + + solver::solver(euf::solver& ctx) : + euf::th_euf_solver(ctx, ctx.get_manager().mk_family_id("fpa")), + m_th_rw(ctx.get_manager()), + m_converter(ctx.get_manager(), m_th_rw), + m_rw(ctx.get_manager(), m_converter, params_ref()), + m_fpa_util(m_converter.fu()), + m_bv_util(m_converter.bu()), + m_arith_util(m_converter.au()) + { + params_ref p; + p.set_bool("arith_lhs", true); + m_th_rw.updt_params(p); + } + + solver::~solver() { + dec_ref_map_key_values(m, m_conversions); + dec_ref_collection_values(m, m_is_added_to_model); + SASSERT(m_conversions.empty()); + SASSERT(m_is_added_to_model.empty()); + } + + + expr_ref solver::convert(expr* e) + { + expr_ref res(m); + expr* ccnv; + TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;); + + if (m_conversions.find(e, ccnv)) { + res = ccnv; + TRACE("t_fpa_detail", tout << "cached:" << std::endl; + tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << + mk_ismt2_pp(res, m) << std::endl;); + } + else { + res = m_rw.convert(m_th_rw, e); + + TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl; + tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << + mk_ismt2_pp(res, m) << std::endl;); + + m_conversions.insert(e, res); + m.inc_ref(e); + m.inc_ref(res); + + // ctx.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); + } + return res; + } + + sat::literal_vector solver::mk_side_conditions() { + sat::literal_vector conds; + expr_ref t(m); + for (expr* arg : m_converter.m_extra_assertions) { + ctx.get_rewriter()(arg, t); + m_th_rw(t); + conds.push_back(b_internalize(t)); + } + m_converter.m_extra_assertions.reset(); + return conds; + } + + void solver::attach_new_th_var(enode * n) { + theory_var v = mk_var(n); + ctx.attach_th_var(n, this, v); + TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_expr(), m) << " := " << v << "\n";); + } + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + SASSERT(m.is_bool(e)); + if (!visit_rec(m, e, sign, root, redundant)) + return sat::null_literal; + return expr2literal(e); + } + + void solver::internalize(expr* e, bool redundant) { + visit_rec(m, e, false, false, redundant); + } + + bool solver::visited(expr* e) { + euf::enode* n = expr2enode(e); + return n && n->is_attached_to(get_id()); + } + + bool solver::visit(expr* e) { + if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { + ctx.internalize(e, m_is_redundant); + return true; + } + m_stack.push_back(sat::eframe(e)); + return false; + } + + bool solver::post_visit(expr* e, bool sign, bool root) { + euf::enode* n = expr2enode(e); + app* a = to_app(e); + SASSERT(!n || !n->is_attached_to(get_id())); + if (!n) + n = mk_enode(e, false); + SASSERT(!n->is_attached_to(get_id())); + mk_var(n); + if (m.is_bool(e)) { + sat::literal atom(ctx.get_si().add_bool_var(e), false); + atom = ctx.attach_lit(atom, e); + sat::literal bv_atom = b_internalize(m_rw.convert_atom(m_th_rw, e)); + sat::literal_vector conds = mk_side_conditions(); + conds.push_back(bv_atom); + add_equiv_and(atom, conds); + if (root) { + if (sign) + atom.neg(); + add_unit(atom); + } + return true; + } + + switch (a->get_decl_kind()) { + case OP_FPA_TO_FP: + case OP_FPA_TO_UBV: + case OP_FPA_TO_SBV: + case OP_FPA_TO_REAL: + case OP_FPA_TO_IEEE_BV: { + expr_ref conv = convert(e); + expr_ref eq = ctx.mk_eq(e, conv); + add_unit(b_internalize(eq)); + add_units(mk_side_conditions()); + break; + } + default: /* ignore */; + } + return true; + } + + void solver::apply_sort_cnstr(enode * n, sort * s) { + TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_expr(), m) << "\n";); + SASSERT(s->get_family_id() == get_id()); + SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)); + SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr())); + SASSERT(n->get_expr()->get_decl()->get_range() == s); + + expr * owner = n->get_expr(); + + if (is_attached_to_var(n)) + return; + attach_new_th_var(n); + + if (m_fpa_util.is_rm(s)) { + // For every RM term, we need to make sure that it's + // associated bit-vector is within the valid range. + if (!m_fpa_util.is_bv2rm(owner)) { + expr_ref valid(m), limit(m); + limit = m_bv_util.mk_numeral(4, 3); + valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit); + add_unit(b_internalize(valid)); + } + } + activate(owner); + } + + void solver::activate(expr* n) { + TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";); + + mpf_manager& mpfm = m_fpa_util.fm(); + + if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { + if (!m_fpa_util.is_fp(n)) { + app_ref wrapped = m_converter.wrap(n); + mpf_rounding_mode rm; + scoped_mpf val(mpfm); + if (m_fpa_util.is_rm_numeral(n, rm)) { + expr_ref rm_num(m); + rm_num = m_bv_util.mk_numeral(rm, 3); + add_unit(b_internalize(ctx.mk_eq(wrapped, rm_num))); + } + else if (m_fpa_util.is_numeral(n, val)) { + expr_ref bv_val_e(m), cc_args(m); + bv_val_e = convert(n); + SASSERT(is_app(bv_val_e)); + SASSERT(to_app(bv_val_e)->get_num_args() == 3); + app_ref bv_val_a(m); + bv_val_a = to_app(bv_val_e.get()); + expr* args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) }; + cc_args = m_bv_util.mk_concat(3, args); + add_unit(b_internalize(ctx.mk_eq(wrapped, cc_args))); + add_units(mk_side_conditions()); + } + else { + expr_ref wu = ctx.mk_eq(m_converter.unwrap(wrapped, m.get_sort(n)), n); + TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;); + add_unit(b_internalize(wu)); + } + } + } + else if (is_app(n) && to_app(n)->get_family_id() == get_id()) { + // These are the conversion functions fp.to_* */ + SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); + } + else { + /* Theory variables can be merged when (= bv-term (bvwrap fp-term)), + in which case context::relevant_eh may call solver::relevant_eh + after theory_bv::relevant_eh, regardless of whether solver is + interested in this term. But, this can only happen because of + (bvwrap ...) terms, i.e., `n' must be a bit-vector expression, + which we can safely ignore. */ + SASSERT(m_bv_util.is_bv(n)); + } + } + + void solver::ensure_equality_relation(theory_var x, theory_var y) { + enode* e_x = var2enode(x); + enode* e_y = var2enode(y); + + TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl; + tout << mk_ismt2_pp(e_x->get_expr(), m) << std::endl << " = " << std::endl << + mk_ismt2_pp(e_y->get_expr(), m) << std::endl;); + + fpa_util& fu = m_fpa_util; + + expr* xe = e_x->get_expr(); + expr* ye = e_y->get_expr(); + + if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye)) + return; + + expr_ref xc = convert(xe); + expr_ref yc = convert(ye); + + TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl << + "yc = " << mk_ismt2_pp(yc, m) << std::endl;); + + expr_ref c(m); + + if ((fu.is_float(xe) && fu.is_float(ye)) || + (fu.is_rm(xe) && fu.is_rm(ye))) + m_converter.mk_eq(xc, yc, c); + else + c = m.mk_eq(xc, yc); + + m_th_rw(c); + + sat::literal eq1 = b_internalize(ctx.mk_eq(e_x, e_y)); + sat::literal eq2 = b_internalize(c); + add_equiv(eq1, eq2); + add_units(mk_side_conditions()); + } + + void solver::new_eq_eh(euf::th_eq const& eq) { + ensure_equality_relation(eq.v1(), eq.v2()); + } + + void solver::new_diseq_eh(euf::th_eq const& eq) { + ensure_equality_relation(eq.v1(), eq.v2()); + } + + void solver::asserted(sat::literal l) { + expr* e = ctx.bool_var2expr(l.var()); + + TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";); + + sat::literal c = b_internalize(convert(e)); + sat::literal_vector conds = mk_side_conditions(); + conds.push_back(c); + if (l.sign()) { + for (sat::literal sc : conds) + add_clause(l, sc); + } + else { + for (auto& sc : conds) + sc.neg(); + conds.push_back(l); + add_clause(conds); + } + } + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr* e = n->get_expr(); + app_ref wrapped(m); + expr_ref value(m); + auto is_wrapped = [&]() { + if (!wrapped) wrapped = m_converter.wrap(e); + return expr2enode(wrapped) != nullptr; + }; + if (m_fpa_util.is_fp(e)) { + SASSERT(n->num_args() == 3); + expr* a = values.get(n->get_arg(0)->get_root_id()); + expr* b = values.get(n->get_arg(1)->get_root_id()); + expr* c = values.get(n->get_arg(2)->get_root_id()); + value = bvs2fpa_value(m.get_sort(e), a, b, c); + } + else if (m_fpa_util.is_bv2rm(e)) { + SASSERT(n->num_args() == 1); + value = bv2rm_value(values.get(n->get_arg(0)->get_root_id())); + } + else if (m_fpa_util.is_rm(e) && is_wrapped()) + value = bv2rm_value(values.get(expr2enode(wrapped)->get_root_id())); + else if (m_fpa_util.is_float(e) && is_wrapped()) + value = bvs2fpa_value(m.get_sort(e), expr2enode(wrapped), nullptr, nullptr); + else { + unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e)); + unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e)); + value = m_fpa_util.mk_pzero(ebits, sbits); + } + values.set(n->get_root_id(), value); + } + + expr* solver::bv2rm_value(expr* b) { + app* result = nullptr; + unsigned bv_sz; + rational val(0); + VERIFY(m_bv_util.is_numeral(b, val, bv_sz)); + SASSERT(bv_sz == 3); + + switch (val.get_uint64()) { + case BV_RM_TIES_TO_AWAY: result = m_fpa_util.mk_round_nearest_ties_to_away(); break; + case BV_RM_TIES_TO_EVEN: result = m_fpa_util.mk_round_nearest_ties_to_even(); break; + case BV_RM_TO_NEGATIVE: result = m_fpa_util.mk_round_toward_negative(); break; + case BV_RM_TO_POSITIVE: result = m_fpa_util.mk_round_toward_positive(); break; + case BV_RM_TO_ZERO: + default: result = m_fpa_util.mk_round_toward_zero(); + } + + TRACE("t_fpa", tout << "result: " << mk_ismt2_pp(result, m) << std::endl;); + return result; + } + + + expr* solver::bvs2fpa_value(sort* s, expr* a, expr* b, expr* c) { + mpf_manager& mpfm = m_fpa_util.fm(); + unsynch_mpz_manager& mpzm = mpfm.mpz_manager(); + app* result; + unsigned ebits = m_fpa_util.get_ebits(s); + unsigned sbits = m_fpa_util.get_sbits(s); + + scoped_mpz bias(mpzm); + mpzm.power(mpz(2), ebits - 1, bias); + mpzm.dec(bias); + + scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm); + unsigned bv_sz; + + if (b == nullptr) { + SASSERT(m_bv_util.is_bv(a)); + SASSERT(m_bv_util.get_bv_size(a) == (ebits + sbits)); + + rational all_r(0); + scoped_mpz all_z(mpzm); + + VERIFY(m_bv_util.is_numeral(a, all_r, bv_sz)); + SASSERT(bv_sz == (ebits + sbits)); + SASSERT(all_r.is_int()); + mpzm.set(all_z, all_r.to_mpq().numerator()); + + mpzm.machine_div2k(all_z, ebits + sbits - 1, sgn_z); + mpzm.mod(all_z, mpfm.m_powers2(ebits + sbits - 1), all_z); + + mpzm.machine_div2k(all_z, sbits - 1, exp_z); + mpzm.mod(all_z, mpfm.m_powers2(sbits - 1), all_z); + + mpzm.set(sig_z, all_z); + } + else { + SASSERT(b); + SASSERT(c); + rational sgn_r(0), exp_r(0), sig_r(0); + + bool r = m_bv_util.is_numeral(a, sgn_r, bv_sz); + SASSERT(r && bv_sz == 1); + r = m_bv_util.is_numeral(b, exp_r, bv_sz); + SASSERT(r && bv_sz == ebits); + r = m_bv_util.is_numeral(c, sig_r, bv_sz); + SASSERT(r && bv_sz == sbits - 1); + (void)r; + + SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator())); + SASSERT(mpzm.is_one(exp_r.to_mpq().denominator())); + SASSERT(mpzm.is_one(sig_r.to_mpq().denominator())); + + mpzm.set(sgn_z, sgn_r.to_mpq().numerator()); + mpzm.set(exp_z, exp_r.to_mpq().numerator()); + mpzm.set(sig_z, sig_r.to_mpq().numerator()); + } + + scoped_mpz exp_u = exp_z - bias; + SASSERT(mpzm.is_int64(exp_u)); + + scoped_mpf f(mpfm); + mpfm.set(f, ebits, sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z); + result = m_fpa_util.mk_value(f); + + TRACE("t_fpa", tout << "result: [" << + mpzm.to_string(sgn_z) << "," << + mpzm.to_string(exp_z) << "," << + mpzm.to_string(sig_z) << "] --> " << + mk_ismt2_pp(result, m) << std::endl;); + + return result; + } + + void solver::add_dep(euf::enode* n, top_sort& dep) { + expr* e = n->get_expr(); + if (m_fpa_util.is_fp(e)) { + SASSERT(n->num_args() == 3); + for (enode* arg : euf::enode_args(n)) + dep.add(n, arg); + } + else if (m_fpa_util.is_bv2rm(e)) { + SASSERT(n->num_args() == 1); + dep.add(n, n->get_arg(0)); + } + else if (m_fpa_util.is_rm(e) || m_fpa_util.is_float(e)) { + app_ref wrapped = m_converter.wrap(e); + if (expr2enode(wrapped)) + dep.add(n, expr2enode(wrapped)); + } + } + + std::ostream& solver::display(std::ostream & out) const { + bool first = true; + for (enode* n : ctx.get_egraph().nodes()) { + theory_var v = n->get_th_var(m_fpa_util.get_family_id()); + if (v != -1) { + if (first) out << "fpa theory variables:" << std::endl; + out << v << " -> " << + mk_ismt2_pp(n->get_expr(), m) << std::endl; + first = false; + } + } + // if there are no fpa theory variables, was fp ever used? + if (first) + return out; + + out << "bv theory variables:" << std::endl; + for (enode * n : ctx.get_egraph().nodes()) { + theory_var v = n->get_th_var(m_bv_util.get_family_id()); + if (v != -1) out << v << " -> " << + mk_ismt2_pp(n->get_expr(), m) << std::endl; + } + + out << "arith theory variables:" << std::endl; + for (enode* n : ctx.get_egraph().nodes()) { + theory_var v = n->get_th_var(m_arith_util.get_family_id()); + if (v != -1) out << v << " -> " << + mk_ismt2_pp(n->get_expr(), m) << std::endl; + } + + out << "equivalence classes:\n"; + for (enode * n : ctx.get_egraph().nodes()) { + expr * e = n->get_expr(); + out << n->get_root_id() << " --> " << mk_ismt2_pp(e, m) << std::endl; + } + return out; + } + +}; diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h new file mode 100644 index 000000000..be60ee456 --- /dev/null +++ b/src/sat/smt/fpa_solver.h @@ -0,0 +1,74 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + fpa_solver.h + +Abstract: + + Floating-Point Theory Plugin + +Author: + + Christoph (cwinter) 2014-04-23 + +Revision History: + +--*/ +#pragma once + +#include "sat/smt/euf_solver.h" +#include "ast/fpa/fpa2bv_converter.h" +#include "ast/fpa/fpa2bv_rewriter.h" + +namespace fpa { + + typedef euf::enode enode; + typedef euf::theory_var theory_var; + + class solver : public euf::th_euf_solver { + protected: + th_rewriter m_th_rw; + fpa2bv_converter_wrapped m_converter; + fpa2bv_rewriter m_rw; + fpa_util & m_fpa_util; + bv_util & m_bv_util; + arith_util & m_arith_util; + obj_map m_conversions; + obj_hashtable m_is_added_to_model; + + bool visit(expr* e) override; + bool visited(expr* e) override; + bool post_visit(expr* e, bool sign, bool root) override; + + expr_ref convert(expr* e); + sat::literal_vector mk_side_conditions(); + void attach_new_th_var(enode* n); + void activate(expr* e); + void ensure_equality_relation(theory_var x, theory_var y); + expr* bv2rm_value(expr* b); + expr* bvs2fpa_value(sort* s, expr* a, expr* b, expr* c); + + + public: + solver(euf::solver& ctx); + ~solver() override; + + void asserted(sat::literal l) override; + void new_eq_eh(euf::th_eq const& eq) override; + bool use_diseqs() const override { return true; } + void new_diseq_eh(euf::th_eq const& eq) override; + + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; + void internalize(expr* e, bool redundant) override; + void apply_sort_cnstr(euf::enode* n, sort* s) override; + + std::ostream& display(std::ostream& out) const override; + + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + void add_dep(euf::enode* n, top_sort& dep) override; + }; + +} + diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 61fa091ff..3406dc284 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -126,6 +126,14 @@ namespace euf { return !was_true; } + bool th_euf_solver::add_units(sat::literal_vector const& lits) { + bool is_new = false; + for (auto lit : lits) + if (add_unit(lit)) + is_new = true; + return is_new; + } + bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { bool was_true = is_true(a, b); sat::literal lits[2] = { a, b }; @@ -155,6 +163,21 @@ namespace euf { return !was_true; } + void th_euf_solver::add_equiv(sat::literal a, sat::literal b) { + add_clause(~a, b); + add_clause(a, ~b); + } + + void th_euf_solver::add_equiv_and(sat::literal a, sat::literal_vector const& bs) { + for (auto b : bs) + add_clause(~a, b); + sat::literal_vector _bs; + for (auto b : bs) + _bs.push_back(~b); + _bs.push_back(a); + add_clause(_bs); + } + bool th_euf_solver::is_true(sat::literal lit) { return ctx.s().value(lit) == l_true; } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index b384700d2..f18d99dd4 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -123,11 +123,15 @@ namespace euf { sat::status mk_status(); bool add_unit(sat::literal lit); + bool add_units(sat::literal_vector const& lits); bool add_clause(sat::literal lit) { return add_unit(lit); } bool add_clause(sat::literal a, sat::literal b); bool add_clause(sat::literal a, sat::literal b, sat::literal c); bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d); bool add_clause(sat::literal_vector const& lits); + void add_equiv(sat::literal a, sat::literal b); + void add_equiv_and(sat::literal a, sat::literal_vector const& bs); + bool is_true(sat::literal lit); bool is_true(sat::literal a, sat::literal b) { return is_true(a) || is_true(b); } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index eeee6297f..61ba1bff5 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -25,24 +25,6 @@ Revision History: namespace smt { - class fpa2bv_conversion_trail_elem : public trail { - ast_manager & m; - obj_map & m_map; - expr_ref key; - public: - fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & map, expr * e) : - m(m), m_map(map), key(e, m) { } - ~fpa2bv_conversion_trail_elem() override { } - void undo(theory_fpa & th) override { - expr * val = m_map.find(key); - m_map.remove(key); - m.dec_ref(key); - m.dec_ref(val); - key = nullptr; - } - }; - - theory_fpa::theory_fpa(context& ctx) : theory(ctx, ctx.get_manager().mk_family_id("fpa")), m_th_rw(ctx.get_manager()), @@ -206,7 +188,7 @@ namespace smt { m_conversions.insert(e, res); m.inc_ref(e); m.inc_ref(res); - m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); + m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); } return res; @@ -250,7 +232,6 @@ namespace smt { } bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) { - force_push(); TRACE("t_fpa_internalize", tout << "internalizing atom: " << mk_ismt2_pp(atom, m) << std::endl;); SASSERT(atom->get_family_id() == get_family_id()); @@ -272,7 +253,6 @@ namespace smt { } bool theory_fpa::internalize_term(app * term) { - force_push(); TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, m) << "\n";); SASSERT(term->get_family_id() == get_family_id()); SASSERT(!ctx.e_internalized(term)); @@ -374,8 +354,6 @@ namespace smt { c_eq_iff = m.mk_iff(xe_eq_ye, c); assert_cnstr(c_eq_iff); assert_cnstr(mk_side_conditions()); - - return; } void theory_fpa::new_diseq_eh(theory_var x, theory_var y) { @@ -418,8 +396,6 @@ namespace smt { c_eq_iff = m.mk_iff(not_xe_eq_ye, c); assert_cnstr(c_eq_iff); assert_cnstr(mk_side_conditions()); - - return; } theory* theory_fpa::mk_fresh(context* new_ctx) { @@ -427,15 +403,11 @@ namespace smt { } void theory_fpa::push_scope_eh() { - if (lazy_push()) - return; theory::push_scope_eh(); m_trail_stack.push_scope(); } void theory_fpa::pop_scope_eh(unsigned num_scopes) { - if (lazy_pop(num_scopes)) - return; m_trail_stack.pop_scope(num_scopes); TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";); theory::pop_scope_eh(num_scopes); @@ -446,8 +418,8 @@ namespace smt { TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";); - expr_ref converted(m); - converted = m.mk_and(convert(e), mk_side_conditions()); + expr_ref converted = convert(e); + converted = m.mk_and(converted, mk_side_conditions()); expr_ref cnstr(m); cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);