From 34fc0cdd5c85e9b851ff535ff485c7e70a7c586c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jun 2021 16:23:27 -0700 Subject: [PATCH] #5324 --- src/sat/smt/euf_solver.cpp | 6 ++-- src/sat/smt/fpa_solver.cpp | 68 ++++++++++++++++++++++++------------- src/sat/smt/fpa_solver.h | 5 ++- src/sat/tactic/goal2sat.cpp | 4 +-- 4 files changed, 53 insertions(+), 30 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 89779f144bc..9d3cc971635 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -332,10 +332,10 @@ namespace euf { propagated1 = true; } - for (auto* s : m_solvers) { - if (s->unit_propagate()) + for (unsigned i = 0; i < m_solvers.size(); ++i) + if (m_solvers[i]->unit_propagate()) propagated1 = true; - } + if (!propagated1) break; propagated = true; diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 5904376f02b..ef2fd731cdf 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -122,6 +122,50 @@ namespace fpa { n = mk_enode(e, false); SASSERT(!n->is_attached_to(get_id())); mk_var(n); + TRACE("fp", tout << "post: " << mk_bounded_pp(e, m) << "\n";); + m_nodes.push_back(std::tuple(n, sign, root)); + ctx.push(push_back_trail(m_nodes)); + 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_decl()->get_range() == s); + + if (is_attached_to_var(n)) + return; + attach_new_th_var(n); + + expr* owner = n->get_expr(); + + if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) { + // For every RM term, we need to make sure that it's + // associated bit-vector is within the valid range. + 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(mk_literal(valid)); + } + activate(owner); + } + + bool solver::unit_propagate() { + + if (m_nodes.size() <= m_nodes_qhead) + return false; + ctx.push(value_trail(m_nodes_qhead)); + for (; m_nodes_qhead < m_nodes.size(); ++m_nodes_qhead) + unit_propagate(m_nodes[m_nodes_qhead]); + return true; + } + + void solver::unit_propagate(std::tuple const& t) { + auto [n, sign, root] = t; + expr* e = n->get_expr(); + app* a = to_app(e); if (m.is_bool(e)) { sat::literal atom(ctx.get_si().add_bool_var(e), false); atom = ctx.attach_lit(atom, e); @@ -151,31 +195,7 @@ namespace fpa { break; } } - 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_decl()->get_range() == s); - - if (is_attached_to_var(n)) - return; - attach_new_th_var(n); - - expr* owner = n->get_expr(); - - if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) { - // For every RM term, we need to make sure that it's - // associated bit-vector is within the valid range. - 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(mk_literal(valid)); - } - activate(owner); } void solver::activate(expr* n) { diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h index 9f0d8ae3619..795abdfdd3d 100644 --- a/src/sat/smt/fpa_solver.h +++ b/src/sat/smt/fpa_solver.h @@ -36,6 +36,8 @@ namespace fpa { bv_util & m_bv_util; arith_util & m_arith_util; obj_map m_conversions; + svector> m_nodes; + unsigned m_nodes_qhead = 0; bool visit(expr* e) override; bool visited(expr* e) override; @@ -45,6 +47,7 @@ namespace fpa { sat::literal_vector mk_side_conditions(); void attach_new_th_var(enode* n); void activate(expr* e); + void unit_propagate(std::tuple const& t); void ensure_equality_relation(theory_var x, theory_var y); public: @@ -67,7 +70,7 @@ namespace fpa { bool add_dep(euf::enode* n, top_sort& dep) override; void finalize_model(model& mdl) override; - bool unit_propagate() override { return false; } + bool unit_propagate() override; void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); } sat::check_result check() override { return sat::check_result::CR_DONE; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d7b97b5213d..925dac7f89a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -744,7 +744,7 @@ struct goal2sat::imp : public sat::sat_internalizer { }; void process(expr* n, bool is_root, bool redundant) { - TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 3) + TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 2) << " root: " << is_root << " result-stack: " << m_result_stack.size() << " frame-stack: " << m_frame_stack.size() << "\n";); @@ -784,7 +784,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_frame_stack[fsz - 1].m_idx++; if (!visit(arg, false, false)) goto loop; - TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(t, m, 2) << " result stack: " << m_result_stack.size() << "\n";); + TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(arg, m, 2) << " result stack: " << m_result_stack.size() << "\n";); } TRACE("goal2sat_bug", tout << "converting\n"; tout << mk_bounded_pp(t, m, 2) << " root: " << root << " sign: " << sign << "\n";