From 083d09aa810cbddd5e7140928bf7f9f678e105d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Feb 2021 13:52:10 -0800 Subject: [PATCH] fix #5016 --- src/ast/ast_ll_pp.cpp | 9 +- src/ast/recfun_decl_plugin.cpp | 22 ++-- src/ast/recfun_decl_plugin.h | 34 ++++++ src/sat/sat_extension.h | 3 + src/sat/sat_solver.cpp | 68 +++++++---- src/sat/sat_solver.h | 7 +- src/sat/smt/dt_solver.cpp | 20 +++- src/sat/smt/euf_solver.cpp | 31 +++++ src/sat/smt/euf_solver.h | 18 +++ src/sat/smt/recfun_solver.cpp | 161 ++++++++++++++------------ src/sat/smt/recfun_solver.h | 60 +++------- src/smt/theory_recfun.cpp | 203 +++++++++++++-------------------- src/smt/theory_recfun.h | 22 ++-- src/smt/theory_str.cpp | 2 - 14 files changed, 366 insertions(+), 294 deletions(-) diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index 83d1fbf85..62dbd74b5 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -20,6 +20,7 @@ Revision History: #include #include "ast/for_each_ast.h" #include "ast/arith_decl_plugin.h" +#include "ast/datatype_decl_plugin.h" // #define AST_LL_PP_SHOW_FAMILY_NAME @@ -30,6 +31,7 @@ class ll_printer { bool m_only_exprs; bool m_compact; arith_util m_autil; + datatype_util m_dt; void display_def_header(ast * n) { if (n != m_root) { @@ -114,6 +116,10 @@ class ll_printer { } m_out << "]"; } + else if (is_func_decl(d) && m_dt.is_is(to_func_decl(d))) { + func_decl* fd = m_dt.get_recognizer_constructor(to_func_decl(d)); + m_out << " " << fd->get_name(); + } } public: @@ -124,7 +130,8 @@ public: m_root(n), m_only_exprs(only_exprs), m_compact(compact), - m_autil(m) { + m_autil(m), + m_dt(m) { } void pp(ast* n) { diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index e26a59b6d..5c670c126 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -185,7 +185,9 @@ namespace recfun { conditions.push_back(choices->sign ? c : m.mk_not(c)); // binding to add to the substitution - subst.insert(ite, choices->sign ? th : el); + expr_ref tgt(choices->sign ? th : el, m); + tgt = subst(tgt); + subst.insert(ite, tgt); } } @@ -193,9 +195,10 @@ namespace recfun { void def::add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr * rhs, bool is_imm) { case_def c(m, m_fid, this, name, case_index, get_domain(), conditions, rhs); c.set_is_immediate(is_imm); - TRACEFN("add_case " << name << " " << mk_pp(rhs, m) - << " :is_imm " << is_imm - << " :guards " << conditions); + TRACEFN("add_case " << name + << "\n" << mk_pp(rhs, m) + << "\n:is_imm " << is_imm + << "\n:guards " << conditions); m_cases.push_back(c); } @@ -250,7 +253,7 @@ namespace recfun { while (! stack.empty()) { expr * e = stack.back(); - stack.pop_back(); + stack.pop_back(); if (m.is_ite(e)) { // need to do a case split on `e`, forking the search space @@ -490,9 +493,9 @@ namespace recfun { max_score = kv.m_value; } } - if (max_score <= 4) { + if (max_score <= 4) break; - } + ptr_vector domain; ptr_vector args; for (unsigned i = 0; i < n; ++i) { @@ -500,21 +503,20 @@ namespace recfun { args.push_back(vars[i]); } - symbol fresh_name(m().mk_fresh_id()); + symbol fresh_name("fold-rec-" + std::to_string(m().mk_fresh_id())); auto pd = mk_def(fresh_name, n, domain.c_ptr(), max_expr->get_sort()); func_decl* f = pd.get_def()->get_decl(); expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m()); set_definition(subst, pd, n, vars, max_expr); subst.insert(max_expr, new_body); result = subst(result); - TRACEFN("substituted " << mk_pp(max_expr, m()) << " -> " << new_body << "\n" << result); + TRACEFN("substituted\n" << mk_pp(max_expr, m()) << "\n->\n" << new_body << "\n" << result); } return result; } } - case_expansion::case_expansion(recfun::util& u, app * n) : m_lhs(n, u.m()), m_def(nullptr), m_args(u.m()) { SASSERT(u.is_defined(n)); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index fad0fe23e..83abc7620 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -312,7 +312,41 @@ namespace recfun { return e.display(out); } + struct propagation_item { + case_expansion* m_case { nullptr }; + body_expansion* m_body { nullptr }; + expr_ref_vector* m_core { nullptr }; + expr* m_guard { nullptr }; + + ~propagation_item() { + dealloc(m_case); + dealloc(m_body); + dealloc(m_core); + } + + propagation_item(expr* guard): + m_guard(guard) {} + + propagation_item(expr_ref_vector const& core): + m_core(alloc(expr_ref_vector, core)) { + } + propagation_item(body_expansion* b): + m_body(b) {} + + propagation_item(case_expansion* c): + m_case(c) {} + + bool is_guard() const { return m_guard != nullptr; } + bool is_core() const { return m_core != nullptr; } + bool is_case() const { return m_case != nullptr; } + bool is_body() const { return m_body != nullptr; } + + expr_ref_vector const& core() const { SASSERT(is_core()); return *m_core; } + body_expansion & body() const { SASSERT(is_body()); return *m_body; } + case_expansion & case_ex() const { SASSERT(is_case()); return *m_case; } + expr* guard() const { SASSERT(is_guard()); return m_guard; } + }; } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index ce504bea6..d60ca4d02 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -118,6 +118,9 @@ namespace sat { virtual bool is_blocked(literal l, ext_constraint_idx) { return false; } virtual bool check_model(model const& m) const { return true; } virtual void gc_vars(unsigned num_vars) {} + virtual bool should_research(sat::literal_vector const& core) { return false;} + virtual void add_assumptions() {} + virtual bool tracking_assumptions() { return false; } virtual bool extract_pb(std::function& card, std::function& pb) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 69db141b8..b156e6694 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1342,17 +1342,8 @@ namespace sat { m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } - lbool is_sat = l_undef; - while (is_sat == l_undef && !should_cancel()) { - if (inconsistent()) is_sat = resolve_conflict_core(); - else if (should_propagate()) propagate(true); - else if (do_cleanup(false)) continue; - else if (should_gc()) do_gc(); - else if (should_rephase()) do_rephase(); - else if (should_restart()) do_restart(!m_config.m_restart_fast); - else if (should_simplify()) do_simplify(); - else if (!decide()) is_sat = final_check(); - } + + lbool is_sat = search(); log_stats(); return is_sat; } @@ -1710,6 +1701,12 @@ namespace sat { } lbool solver::bounded_search() { + flet _disable_simplify(m_simplify_enabled, false); + flet _restart_enabled(m_restart_enabled, false); + return search(); + } + + lbool solver::basic_search() { lbool is_sat = l_undef; while (is_sat == l_undef && !should_cancel()) { if (inconsistent()) is_sat = resolve_conflict_core(); @@ -1717,17 +1714,31 @@ namespace sat { else if (do_cleanup(false)) continue; else if (should_gc()) do_gc(); else if (should_rephase()) do_rephase(); - else if (should_restart()) return l_undef; + else if (should_restart()) { if (!m_restart_enabled) return l_undef; do_restart(!m_config.m_restart_fast); } + else if (should_simplify()) do_simplify(); else if (!decide()) is_sat = final_check(); } return is_sat; } + lbool solver::search() { + if (!m_ext || !m_ext->tracking_assumptions()) + return basic_search(); + while (true) { + pop_to_base_level(); + reinit_assumptions(); + lbool r = basic_search(); + if (r != l_false) + return r; + if (!m_ext->should_research(m_core)) + return r; + } + } + bool solver::should_propagate() const { return !inconsistent() && m_qhead < m_trail.size(); } - lbool solver::final_check() { if (m_ext) { switch (m_ext->check()) { @@ -1796,6 +1807,7 @@ namespace sat { add_assumption(lit); assign_scoped(lit); } + m_search_lvl = scope_lvl(); SASSERT(m_search_lvl == 1); } @@ -1811,6 +1823,7 @@ namespace sat { void solver::reset_assumptions() { m_assumptions.reset(); m_assumption_set.reset(); + m_ext_assumption_set.reset(); } void solver::add_assumption(literal lit) { @@ -1819,11 +1832,6 @@ namespace sat { set_external(lit.var()); } - void solver::pop_assumption() { - VERIFY(m_assumptions.back() == m_assumption_set.pop()); - m_assumptions.pop_back(); - } - void solver::reassert_min_core() { SASSERT(m_min_core_valid); pop_to_base_level(); @@ -1852,7 +1860,10 @@ namespace sat { if (inconsistent()) break; assign_scoped(lit); } - if (!inconsistent()) propagate(false); + init_ext_assumptions(); + + if (!inconsistent()) + propagate(false); TRACE("sat", tout << "consistent: " << !inconsistent() << "\n"; for (literal a : m_assumptions) { @@ -1868,12 +1879,23 @@ namespace sat { } } + void solver::init_ext_assumptions() { + if (m_ext && m_ext->tracking_assumptions()) { + m_ext_assumption_set.reset(); + unsigned trail_size = m_trail.size(); + if (!inconsistent()) + m_ext->add_assumptions(); + for (unsigned i = trail_size; i < m_trail.size(); ++i) + m_ext_assumption_set.insert(m_trail[i]); + } + } + bool solver::tracking_assumptions() const { - return !m_assumptions.empty() || !m_user_scope_literals.empty(); + return !m_assumptions.empty() || !m_user_scope_literals.empty() || (m_ext && m_ext->tracking_assumptions()); } bool solver::is_assumption(literal l) const { - return tracking_assumptions() && m_assumption_set.contains(l); + return tracking_assumptions() && (m_assumption_set.contains(l) || m_ext_assumption_set.contains(l)); } void solver::set_activity(bool_var v, unsigned new_act) { @@ -1931,7 +1953,7 @@ namespace sat { } bool solver::should_simplify() const { - return m_conflicts_since_init >= m_next_simplify; + return m_conflicts_since_init >= m_next_simplify && m_simplify_enabled; } /** \brief Apply all simplifications. @@ -2278,7 +2300,7 @@ namespace sat { IF_VERBOSE(30, display_status(verbose_stream());); TRACE("sat", tout << "restart " << restart_level(to_base) << "\n";); pop_reinit(restart_level(to_base)); - set_next_restart(); + set_next_restart(); } unsigned solver::restart_level(bool to_base) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 3ed0f51d6..bae4f0bfa 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -182,6 +182,7 @@ namespace sat { scoped_ptr m_clone; // for debugging purposes literal_vector m_assumptions; // additional assumptions during check literal_set m_assumption_set; // set of enabled assumptions + literal_set m_ext_assumption_set; // set of enabled assumptions literal_vector m_core; // unsat core unsigned m_par_id; @@ -497,9 +498,13 @@ namespace sat { unsigned m_num_checkpoints { 0 }; double m_min_d_tk { 0 } ; unsigned m_next_simplify { 0 }; + bool m_simplify_enabled { true }; + bool m_restart_enabled { true }; bool decide(); bool_var next_var(); lbool bounded_search(); + lbool basic_search(); + lbool search(); lbool final_check(); void init_search(); @@ -512,8 +517,8 @@ namespace sat { void resolve_weighted(); void reset_assumptions(); void add_assumption(literal lit); - void pop_assumption(); void reinit_assumptions(); + void init_ext_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; bool should_simplify() const; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index e7f88bf2e..c7f062819 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -222,6 +222,8 @@ namespace dt { else if (is_update_field(n)) { assert_update_field_axioms(n); } + else if (is_recognizer(n)) + ; else { sort* s = n->get_expr()->get_sort(); if (dt.get_datatype_num_constructors(s) == 1) @@ -251,7 +253,9 @@ namespace dt { TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";); + enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr); + if (recognizer == nullptr) r = dt.get_constructor_is(non_rec_c); else if (ctx.value(recognizer) != l_false) @@ -263,13 +267,15 @@ namespace dt { unsigned idx = 0; ptr_vector const& constructors = *dt.get_datatype_constructors(srt); for (enode* curr : d->m_recognizers) { + if (curr == nullptr) { // found empty slot... r = dt.get_constructor_is(constructors[idx]); break; } - else if (ctx.value(curr) != l_false) + else if (ctx.value(curr) != l_false) { return; + } ++idx; } if (r == nullptr) @@ -342,6 +348,7 @@ namespace dt { } void solver::add_recognizer(theory_var v, enode* recognizer) { + TRACE("dt", tout << "add recognizer " << v << " " << mk_pp(recognizer->get_expr(), m) << "\n";); SASSERT(is_recognizer(recognizer)); v = m_find.find(v); var_data* d = m_var_data[v]; @@ -596,7 +603,7 @@ namespace dt { a3 = cons(v3, a1) */ bool solver::occurs_check(enode* n) { - TRACE("dt", tout << "occurs check: " << ctx.bpp(n) << "\n";); + TRACE("dt_verbose", tout << "occurs check: " << ctx.bpp(n) << "\n";); m_stats.m_occurs_check++; bool res = false; @@ -611,7 +618,7 @@ namespace dt { if (oc_cycle_free(app)) continue; - TRACE("dt", tout << "occurs check loop: " << ctx.bpp(app) << (op == ENTER ? " enter" : " exit") << "\n";); + TRACE("dt_verbose", tout << "occurs check loop: " << ctx.bpp(app) << (op == ENTER ? " enter" : " exit") << "\n";); switch (op) { case ENTER: @@ -627,6 +634,7 @@ namespace dt { if (res) { clear_mark(); ctx.set_conflict(euf::th_propagation::mk(*this, m_used_eqs)); + TRACE("dt", tout << "occurs check conflict: " << ctx.bpp(n) << "\n";); } return res; } @@ -741,17 +749,21 @@ namespace dt { } } mk_var(n); + } else if (is_recognizer(term)) { + mk_var(n); enode* arg = n->get_arg(0); theory_var v = mk_var(arg); - add_recognizer(v, n); + add_recognizer(v, n); + } else { SASSERT(is_accessor(term)); SASSERT(n->num_args() == 1); mk_var(n->get_arg(0)); } + return true; } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index f86102fe8..5118b8fca 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -27,9 +27,16 @@ Author: #include "sat/smt/q_solver.h" #include "sat/smt/fpa_solver.h" #include "sat/smt/dt_solver.h" +#include "sat/smt/recfun_solver.h" namespace euf { + std::ostream& clause_pp::display(std::ostream& out) const { + for (auto lit : lits) + out << s.literal2expr(lit) << " "; + return out; + } + solver::solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p) : extension(symbol("euf"), m.mk_family_id("euf")), m(m), @@ -103,6 +110,7 @@ namespace euf { fpa_util fpa(m); arith_util arith(m); datatype_util dt(m); + recfun::util rf(m); if (pb.get_family_id() == fid) ext = alloc(sat::ba_solver, *this, fid); else if (bvu.get_family_id() == fid) @@ -115,6 +123,8 @@ namespace euf { ext = alloc(arith::solver, *this, fid); else if (dt.get_family_id() == fid) ext = alloc(dt::solver, *this, fid); + else if (rf.get_family_id() == fid) + ext = alloc(recfun::solver, *this); if (ext) add_solver(ext); @@ -430,6 +440,7 @@ namespace euf { if (!init_relevancy()) give_up = true; + for (auto* e : m_solvers) { if (!m.inc()) return sat::check_result::CR_GIVEUP; @@ -558,6 +569,26 @@ namespace euf { if (m_ackerman) m_ackerman->propagate(); } + + bool solver::should_research(sat::literal_vector const& core) { + bool result = false; + for (auto* e : m_solvers) + if (e->should_research(core)) + result = true; + return result; + } + + void solver::add_assumptions() { + for (auto* e : m_solvers) + e->add_assumptions(); + } + + bool solver::tracking_assumptions() { + for (auto* e : m_solvers) + if (e->tracking_assumptions()) + return true; + return false; + } void solver::clauses_modifed() { for (auto* e : m_solvers) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index aff9d6b55..84a926650 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -51,6 +51,14 @@ namespace euf { size_t to_index() const { return sat::constraint_base::mem2base(this); } }; + class clause_pp { + solver& s; + sat::literal_vector const& lits; + public: + clause_pp(solver& s, sat::literal_vector const& lits):s(s), lits(lits) {} + std::ostream& display(std::ostream& out) const; + }; + class solver : public sat::extension, public th_internalizer, public th_decompile { typedef top_sort deps_t; friend class ackerman; @@ -266,6 +274,9 @@ namespace euf { bool is_external(bool_var v) override; bool propagated(literal l, ext_constraint_idx idx) override; bool unit_propagate() override; + bool should_research(sat::literal_vector const& core) override; + void add_assumptions() override; + bool tracking_assumptions() override; void propagate(literal lit, ext_justification_idx idx); bool propagate(enode* a, enode* b, ext_justification_idx idx); @@ -297,6 +308,7 @@ namespace euf { std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override; euf::egraph::b_pp bpp(enode* n) { return m_egraph.bpp(n); } + clause_pp pp(literal_vector const& lits) { return clause_pp(*this, lits); } void collect_statistics(statistics& st) const override; extension* copy(sat::solver* s) override; enode* copy(solver& dst_ctx, enode* src_n); @@ -396,8 +408,14 @@ namespace euf { }; + + inline std::ostream& operator<<(std::ostream& out, clause_pp const& p) { + return p.display(out); + } + }; inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) { return s.display(out); } + diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index eec8ea3c8..0da80ebdd 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -66,6 +66,7 @@ namespace recfun { */ void solver::assert_macro_axiom(case_expansion & e) { m_stats.m_macro_expansions++; + TRACEFN("case expansion " << e); SASSERT(e.m_def->is_fun_macro()); auto & vars = e.m_def->get_vars(); auto lhs = e.m_lhs; @@ -84,6 +85,14 @@ namespace recfun { * also body-expand paths that do not depend on any defined fun */ void solver::assert_case_axioms(case_expansion & e) { + if (e.m_def->is_fun_macro()) { + assert_macro_axiom(e); + return; + } + + ++m_stats.m_case_expansions; + TRACEFN("assert_case_axioms " << e + << " with " << e.m_def->get_cases().size() << " cases"); SASSERT(e.m_def->is_fun_defined()); // add case-axioms for all case-paths // assert this was not defined before. @@ -106,36 +115,41 @@ namespace recfun { disable_guard(pred_applied, guards); continue; } - activate_guard(pred_applied, guards); + assert_guard(pred_applied, guards); } add_clause(preds); } - void solver::activate_guard(expr* pred_applied, expr_ref_vector const& guards) { + void solver::assert_guard(expr* pred_applied, expr_ref_vector const& guards) { sat::literal_vector lguards; for (expr* ga : guards) lguards.push_back(mk_literal(ga)); add_equiv_and(mk_literal(pred_applied), lguards); } + void solver::block_core(expr_ref_vector const& core) { + sat::literal_vector clause; + for (expr* e : core) + clause.push_back(~mk_literal(e)); + add_clause(clause); + } + /** * make clause `depth_limit => ~guard` * the guard appears at a depth below the current cutoff. */ void solver::disable_guard(expr* guard, expr_ref_vector const& guards) { - expr_ref nguard(m.mk_not(guard), m); - if (is_disabled_guard(nguard)) - return; - SASSERT(!is_enabled_guard(nguard)); - sat::literal_vector c; + SASSERT(!is_enabled_guard(guard)); app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); - c.push_back(~mk_literal(dlimit)); - c.push_back(~mk_literal(guard)); - m_disabled_guards.push_back(nguard); - SASSERT(!m_guard2pending.contains(nguard)); - m_guard2pending.insert(nguard, alloc(expr_ref_vector, guards)); - TRACEFN("add clause\n" << c); - m_propagation_queue.push_back(alloc(propagation_item, c)); + expr_ref_vector core(m); + core.push_back(dlimit); + core.push_back(guard); + if (!m_guard2pending.contains(guard)) { + m_disabled_guards.push_back(guard); + m_guard2pending.insert(guard, alloc(expr_ref_vector, guards)); + } + TRACEFN("add clause\n" << core); + push_core(core); } /** @@ -147,6 +161,7 @@ namespace recfun { * */ void solver::assert_body_axiom(body_expansion & e) { + ++m_stats.m_body_expansions; recfun::def & d = *e.m_cdef->get_def(); auto & vars = d.get_vars(); auto & args = e.m_args; @@ -184,11 +199,6 @@ namespace recfun { return out << "disabled guards:\n" << m_disabled_guards << "\n"; } - std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { - UNREACHABLE(); - return out; - } - void solver::collect_statistics(statistics& st) const { st.update("recfun macro expansion", m_stats.m_macro_expansions); st.update("recfun case expansion", m_stats.m_case_expansions); @@ -196,53 +206,35 @@ namespace recfun { } euf::th_solver* solver::clone(euf::solver& ctx) { - return nullptr; + return alloc(solver, ctx); } bool solver::unit_propagate() { + force_push(); if (m_qhead == m_propagation_queue.size()) return false; ctx.push(value_trail(m_qhead)); for (; m_qhead < m_propagation_queue.size() && !s().inconsistent(); ++m_qhead) { auto& p = *m_propagation_queue[m_qhead]; - if (p.is_guard()) { - expr* ng = nullptr; - VERIFY(m.is_not(p.m_guard, ng)); - activate_guard(ng, *m_guard2pending[p.m_guard]); - } - else if (p.is_clause()) { - add_clause(p.m_clause); - } - else if (p.is_case()) { - recfun::case_expansion& e = *p.m_case; - if (e.m_def->is_fun_macro()) - assert_macro_axiom(e); - else - assert_case_axioms(e); - ++m_stats.m_case_expansions; - } - else { - SASSERT(p.is_body()); - assert_body_axiom(*p.m_body); - ++m_stats.m_body_expansions; - } + if (p.is_guard()) + assert_guard(p.guard(), *m_guard2pending[p.guard()]); + else if (p.is_core()) + block_core(p.core()); + else if (p.is_case()) + assert_case_axioms(p.case_ex()); + else + assert_body_axiom(p.body()); } return true; } - void solver::push_body_expand(expr* e) { - auto* b = alloc(body_expansion, u(), to_app(e)); - m_propagation_queue.push_back(alloc(propagation_item, b)); - ctx.push(push_back_vector>(m_propagation_queue)); - } - - void solver::push_case_expand(expr* e) { - auto* c = alloc(case_expansion, u(), to_app(e)); - m_propagation_queue.push_back(alloc(propagation_item, c)); + void solver::push(propagation_item* p) { + m_propagation_queue.push_back(p); ctx.push(push_back_vector>(m_propagation_queue)); } sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + force_push(); SASSERT(m.is_bool(e)); if (!visit_rec(m, e, sign, root, redundant)) { TRACE("array", tout << mk_pp(e, m) << "\n";); @@ -255,6 +247,7 @@ namespace recfun { } void solver::internalize(expr* e, bool redundant) { + force_push(); visit_rec(m, e, false, false, redundant); } @@ -268,8 +261,6 @@ namespace recfun { return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { ctx.internalize(e, m_is_redundant); - euf::enode* n = expr2enode(e); - // TODO ensure_var(n); return true; } m_stack.push_back(sat::eframe(e)); @@ -284,35 +275,57 @@ namespace recfun { n = mk_enode(e, false); SASSERT(!n->is_attached_to(get_id())); mk_var(n); -#if 0 - for (auto* arg : euf::enode_args(n)) - ensure_var(arg); - switch (a->get_decl_kind()) { - default: - UNREACHABLE(); - break; - } -#endif if (u().is_defined(e) && u().has_defs()) push_case_expand(e); - return true; } - - - euf::theory_var solver::mk_var(euf::enode* n) { - return euf::null_theory_var; - } - - void solver::init_search() { - + void solver::add_assumptions() { + if (u().has_defs() || m_disabled_guards.empty()) { + app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); + TRACEFN("add_theory_assumption " << dlimit); + s().assign_scoped(mk_literal(dlimit)); + for (auto g : m_disabled_guards) + s().assign_scoped(~mk_literal(g)); + } } - void solver::finalize_model(model& mdl) { - + bool solver::should_research(sat::literal_vector const& core) { + bool found = false; + unsigned min_gen = UINT_MAX; + expr* to_delete = nullptr; + unsigned n = 0; + for (sat::literal lit : core) { + expr* e = ctx.bool_var2expr(lit.var()); + if (lit.sign() && is_disabled_guard(e)) { + found = true; + unsigned gen = ctx.get_max_generation(e); + if (gen < min_gen) + n = 0; + + if (gen <= min_gen && s().rand()() % (++n) == 0) { + to_delete = e; + min_gen = gen; + } + } + else if (u().is_num_rounds(e)) + found = true; + } + if (found) { + ++m_num_rounds; + if (to_delete) { + m_disabled_guards.erase(to_delete); + m_enabled_guards.push_back(to_delete); + push_guard(to_delete); + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); + } + else { + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n"); + } + for (expr* g : m_enabled_guards) + push_guard(g); + } + return found; } - - } diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h index 4cc0ef46f..f8ce8f2e6 100644 --- a/src/sat/smt/recfun_solver.h +++ b/src/sat/smt/recfun_solver.h @@ -49,44 +49,16 @@ namespace recfun { unsigned_vector m_preds_lim; unsigned m_num_rounds { 0 }; - struct propagation_item { - case_expansion* m_case { nullptr }; - body_expansion* m_body { nullptr }; - sat::literal_vector m_clause; - expr* m_guard { nullptr }; - - ~propagation_item() { - dealloc(m_case); - dealloc(m_body); - } - - propagation_item(expr* guard): - m_guard(guard) - {} - - propagation_item(sat::literal_vector const& clause): - m_clause(clause) - {} - - propagation_item(body_expansion* b): - m_body(b) - {} - propagation_item(case_expansion* c): - m_case(c) - {} - - bool is_guard() const { return m_guard != nullptr; } - bool is_clause() const { return !m_clause.empty(); } - bool is_case() const { return m_case != nullptr; } - bool is_body() const { return m_body != nullptr; } - }; scoped_ptr_vector m_propagation_queue; unsigned m_qhead { 0 }; - void push_body_expand(expr* e); - void push_case_expand(expr* e); + void push_body_expand(expr* e) { push(alloc(propagation_item, alloc(body_expansion, u(), to_app(e)))); } + void push_case_expand(expr* e) { push(alloc(propagation_item, alloc(case_expansion, u(), to_app(e)))); } + void push_guard(expr* e) { push(alloc(propagation_item, e)); } + void push_core(expr_ref_vector const& core) { push(alloc(propagation_item, core)); } + void push(propagation_item* p); - bool is_enabled_guard(expr* guard) { expr_ref ng(m.mk_not(guard), m); return m_enabled_guards.contains(ng); } + bool is_enabled_guard(expr* guard) { return m_enabled_guards.contains(guard); } bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); } recfun::util & u() const { return m_util; } @@ -96,20 +68,15 @@ namespace recfun { bool is_defined(euf::enode * e) const { return is_defined(e->get_expr()); } bool is_case_pred(euf::enode * e) const { return is_case_pred(e->get_expr()); } - void activate_guard(expr* guard, expr_ref_vector const& guards); - expr_ref apply_args(vars const & vars, expr_ref_vector const & args, expr * e); //!< substitute variables by args + expr_ref apply_args(vars const & vars, expr_ref_vector const & args, expr * e); void assert_macro_axiom(case_expansion & e); void assert_case_axioms(case_expansion & e); void assert_body_axiom(body_expansion & e); - - void add_induction_lemmas(unsigned depth); + void assert_guard(expr* guard, expr_ref_vector const& guards); + void block_core(expr_ref_vector const& core); void disable_guard(expr* guard, expr_ref_vector const& guards); - unsigned get_depth(expr* e); - void set_depth(unsigned d, expr* e); - void set_depth_rec(unsigned d, expr* e); - sat::literal mk_eq_lit(expr* l, expr* r); bool is_standard_order(recfun::vars const& vars) const { return vars.empty() || vars[vars.size()-1]->get_idx() == 0; } @@ -130,15 +97,16 @@ namespace recfun { sat::check_result check() override; std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return display_constraint(out, idx); } - std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out; } void collect_statistics(statistics& st) const override; euf::th_solver* clone(euf::solver& ctx) override; bool unit_propagate() override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void internalize(expr* e, bool redundant) override; - euf::theory_var mk_var(euf::enode* n) override; - void init_search() override; - void finalize_model(model& mdl) override; bool is_shared(euf::theory_var v) const override { return true; } + void init_search() override {} + bool should_research(sat::literal_vector const& core) override; + void add_assumptions() override; + bool tracking_assumptions() override { return true; } }; } diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index a935b5454..7f8a6dd0c 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -19,6 +19,7 @@ Revision History: #include "util/stats.h" #include "ast/ast_util.h" +#include "ast/ast_ll_pp.h" #include "ast/for_each_expr.h" #include "smt/theory_recfun.h" @@ -33,9 +34,7 @@ namespace smt { m_util(m_plugin.u()), m_disabled_guards(m), m_enabled_guards(m), - m_preds(m), - m_q_case_expand(), - m_q_body_expand() { + m_preds(m) { } theory_recfun::~theory_recfun() { @@ -48,11 +47,7 @@ namespace smt { return alloc(theory_recfun, *new_ctx); } - void theory_recfun::init_search_eh() { - } - bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) { - TRACEFN(mk_pp(atom, m)); if (!u().has_defs()) { return false; } @@ -67,7 +62,7 @@ namespace smt { ctx.set_var_theory(v, get_id()); } if (!ctx.relevancy() && u().is_defined(atom)) { - push_case_expand(alloc(recfun::case_expansion, u(), atom)); + push_case_expand(atom); } return true; } @@ -79,39 +74,23 @@ namespace smt { for (expr* e : *term) { ctx.internalize(e, false); } - // the internalization of the arguments may have triggered the internalization of term. if (!ctx.e_internalized(term)) { ctx.mk_enode(term, false, false, true); - if (!ctx.relevancy() && u().is_defined(term)) { - push_case_expand(alloc(recfun::case_expansion, u(), term)); - } } - + if (!ctx.relevancy() && u().is_defined(term)) { + push_case_expand(term); + } return true; } - void theory_recfun::reset_queues() { - for (auto* e : m_q_case_expand) { - dealloc(e); - } - m_q_case_expand.reset(); - for (auto* e : m_q_body_expand) { - dealloc(e); - } - m_q_body_expand.reset(); - m_q_clauses.clear(); - } void theory_recfun::reset_eh() { - reset_queues(); m_stats.reset(); theory::reset_eh(); m_disabled_guards.reset(); m_enabled_guards.reset(); - m_q_guards.reset(); - for (auto & kv : m_guard2pending) { + for (auto & kv : m_guard2pending) dealloc(kv.m_value); - } m_guard2pending.reset(); } @@ -122,9 +101,9 @@ namespace smt { */ void theory_recfun::relevant_eh(app * n) { SASSERT(ctx.relevancy()); - TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); + // TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); if (u().is_defined(n) && u().has_defs()) { - push_case_expand(alloc(recfun::case_expansion, u(), n)); + push_case_expand(n); } } @@ -135,7 +114,6 @@ namespace smt { void theory_recfun::pop_scope_eh(unsigned num_scopes) { theory::pop_scope_eh(num_scopes); - reset_queues(); // restore depth book-keeping unsigned new_lim = m_preds_lim.size()-num_scopes; @@ -150,80 +128,50 @@ namespace smt { #endif m_preds_lim.shrink(new_lim); } - - void theory_recfun::restart_eh() { - TRACEFN("restart"); - reset_queues(); - theory::restart_eh(); - } - + bool theory_recfun::can_propagate() { - return - !m_q_case_expand.empty() || - !m_q_body_expand.empty() || - !m_q_clauses.empty() || - !m_q_guards.empty(); + return m_qhead < m_propagation_queue.size(); } void theory_recfun::propagate() { - - for (expr* g : m_q_guards) { - expr* ng = nullptr; - VERIFY(m.is_not(g, ng)); - activate_guard(ng, *m_guard2pending[g]); + if (m_qhead == m_propagation_queue.size()) + return; + ctx.push_trail(value_trail(m_qhead)); + for (; m_qhead < m_propagation_queue.size() && !ctx.inconsistent(); ++m_qhead) { + auto& p = *m_propagation_queue[m_qhead]; + if (p.is_guard()) + activate_guard(p.guard(), *m_guard2pending[p.guard()]); + else if (p.is_core()) + block_core(p.core()); + else if (p.is_case()) + assert_case_axioms(p.case_ex()); + else + assert_body_axiom(p.body()); } - m_q_guards.reset(); - - for (literal_vector & c : m_q_clauses) { - TRACEFN("add axiom " << pp_lits(ctx, c)); - ctx.mk_th_axiom(get_id(), c); - } - m_q_clauses.clear(); - - for (unsigned i = 0; i < m_q_case_expand.size(); ++i) { - recfun::case_expansion* e = m_q_case_expand[i]; - if (e->m_def->is_fun_macro()) { - // body expand immediately - assert_macro_axiom(*e); - } - else { - // case expand - SASSERT(e->m_def->is_fun_defined()); - assert_case_axioms(*e); - } - dealloc(e); - m_q_case_expand[i] = nullptr; - } - m_stats.m_case_expansions += m_q_case_expand.size(); - m_q_case_expand.reset(); - - for (unsigned i = 0; i < m_q_body_expand.size(); ++i) { - assert_body_axiom(*m_q_body_expand[i]); - dealloc(m_q_body_expand[i]); - m_q_body_expand[i] = nullptr; - } - m_stats.m_body_expansions += m_q_body_expand.size(); - m_q_body_expand.reset(); } + void theory_recfun::push(propagation_item* p) { + m_propagation_queue.push_back(p); + ctx.push_trail(push_back_vector>(m_propagation_queue)); + } + + /** * make clause `depth_limit => ~guard` * the guard appears at a depth below the current cutoff. */ void theory_recfun::disable_guard(expr* guard, expr_ref_vector const& guards) { - expr_ref nguard(m.mk_not(guard), m); - if (is_disabled_guard(nguard)) - return; - SASSERT(!is_enabled_guard(nguard)); - literal_vector c; + SASSERT(!is_enabled_guard(guard)); app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); - c.push_back(~mk_literal(dlimit)); - c.push_back(~mk_literal(guard)); - m_disabled_guards.push_back(nguard); - SASSERT(!m_guard2pending.contains(nguard)); - m_guard2pending.insert(nguard, alloc(expr_ref_vector, guards)); - TRACEFN("add clause\n" << pp_lits(ctx, c)); - m_q_clauses.push_back(std::move(c)); + expr_ref_vector core(m); + core.push_back(dlimit); + core.push_back(guard); + if (!m_guard2pending.contains(guard)) { + m_disabled_guards.push_back(guard); + m_guard2pending.insert(guard, alloc(expr_ref_vector, guards)); + } + TRACEFN("add core: " << core); + push_core(core); } /** @@ -268,7 +216,7 @@ namespace smt { if (is_true && u().is_case_pred(e)) { TRACEFN("assign_case_pred_true " << mk_pp(e, m)); // body-expand - push_body_expand(alloc(recfun::body_expansion, u(), to_app(e))); + push_body_expand(e); } } @@ -280,8 +228,7 @@ namespace smt { expr * e) { SASSERT(is_standard_order(vars)); var_subst subst(m, true); - expr_ref new_body(m); - new_body = subst(e, args); + expr_ref new_body = subst(e, args); ctx.get_rewriter()(new_body); // simplify set_depth_rec(depth + 1, new_body); return new_body; @@ -315,6 +262,13 @@ namespace smt { return lit; } + void theory_recfun::block_core(expr_ref_vector const& core) { + literal_vector clause; + for (expr* e : core) + clause.push_back(~mk_literal(e)); + ctx.mk_th_axiom(get_id(), clause); + } + /** * For functions f(args) that are given as macros f(vs) = rhs * @@ -344,6 +298,13 @@ namespace smt { * also body-expand paths that do not depend on any defined fun */ void theory_recfun::assert_case_axioms(recfun::case_expansion & e) { + + if (e.m_def->is_fun_macro()) { + assert_macro_axiom(e); + return; + } + + ++m_stats.m_case_expansions; TRACEFN("assert_case_axioms " << e << " with " << e.m_def->get_cases().size() << " cases"); SASSERT(e.m_def->is_fun_defined()); @@ -352,7 +313,6 @@ namespace smt { literal_vector preds; auto & vars = e.m_def->get_vars(); - unsigned max_depth = 0; for (recfun::case_def const & c : e.m_def->get_cases()) { // applied predicate to `args` app_ref pred_applied = c.apply_case_predicate(e.m_args); @@ -372,18 +332,16 @@ namespace smt { } else if (!is_enabled_guard(pred_applied)) { disable_guard(pred_applied, guards); - max_depth = std::max(depth, max_depth); continue; } activate_guard(pred_applied, guards); } + // the disjunction of branches is asserted // to close the available cases. - { - scoped_trace_stream _tr2(*this, preds); - ctx.mk_th_axiom(get_id(), preds); - } - (void)max_depth; + + scoped_trace_stream _tr(*this, preds); + ctx.mk_th_axiom(get_id(), preds); } void theory_recfun::activate_guard(expr* pred_applied, expr_ref_vector const& guards) { @@ -393,13 +351,10 @@ namespace smt { for (expr* ga : guards) { literal guard = mk_literal(ga); lguards.push_back(~guard); - literal c[2] = {~concl, guard}; - std::function fn = [&]() { return literal_vector(2, c); }; - scoped_trace_stream _tr(*this, fn); - ctx.mk_th_axiom(get_id(), 2, c); + scoped_trace_stream _tr1(*this, ~concl, guard); + ctx.mk_th_axiom(get_id(), ~concl, guard); } - std::function fn1 = [&]() { return lguards; }; - scoped_trace_stream _tr1(*this, fn1); + scoped_trace_stream _tr2(*this, lguards); ctx.mk_th_axiom(get_id(), lguards); } @@ -412,6 +367,7 @@ namespace smt { * */ void theory_recfun::assert_body_axiom(recfun::body_expansion & e) { + ++m_stats.m_body_expansions; recfun::def & d = *e.m_cdef->get_def(); auto & vars = d.get_vars(); auto & args = e.m_args; @@ -432,16 +388,15 @@ namespace smt { } } clause.push_back(mk_eq_lit(lhs, rhs)); + TRACEFN(e << "\n" << pp_lits(ctx, clause)); std::function fn = [&]() { return clause; }; scoped_trace_stream _tr(*this, fn); ctx.mk_th_axiom(get_id(), clause); - TRACEFN("body " << e); - TRACEFN(pp_lits(ctx, clause)); } final_check_status theory_recfun::final_check_eh() { - TRACEFN("final\n"); if (can_propagate()) { + TRACEFN("final\n"); propagate(); return FC_CONTINUE; } @@ -453,7 +408,8 @@ namespace smt { app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); TRACEFN("add_theory_assumption " << dlimit); assumptions.push_back(dlimit); - assumptions.append(m_disabled_guards); + for (expr* e : m_disabled_guards) + assumptions.push_back(m.mk_not(e)); } } @@ -463,41 +419,42 @@ namespace smt { expr* to_delete = nullptr; unsigned n = 0; unsigned current_depth = UINT_MAX; - for (auto & e : unsat_core) { - if (is_disabled_guard(e)) { + for (auto * ne : unsat_core) { + expr* e = nullptr; + if (m.is_not(ne, e) && is_disabled_guard(e)) { found = true; - expr* ne = nullptr; - VERIFY(m.is_not(e, ne)); - unsigned depth = get_depth(ne); - if (depth < current_depth) + unsigned depth = get_depth(e); + if (depth < current_depth) n = 0; if (depth <= current_depth && (ctx.get_random_value() % (++n)) == 0) { to_delete = e; current_depth = depth; } } - else if (u().is_num_rounds(e)) { + else if (u().is_num_rounds(ne)) found = true; - } } if (found) { m_num_rounds++; if (to_delete) { m_disabled_guards.erase(to_delete); m_enabled_guards.push_back(to_delete); - m_q_guards.push_back(to_delete); - IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); } else { - IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increment-round)\n"); + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n"); } + for (expr* g : m_enabled_guards) + push_guard(g); } + TRACEFN("should research " << found); return found; } void theory_recfun::display(std::ostream & out) const { out << "recfun\n"; out << "disabled guards:\n" << m_disabled_guards << "\n"; + out << "enabled guards:\n" << m_enabled_guards << "\n"; } void theory_recfun::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 57e163fc1..a60b4c9ea 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -45,12 +45,18 @@ namespace smt { unsigned_vector m_preds_lim; unsigned m_num_rounds { 0 }; - ptr_vector m_q_case_expand; - ptr_vector m_q_body_expand; - vector m_q_clauses; - ptr_vector m_q_guards; + typedef recfun::propagation_item propagation_item; - bool is_enabled_guard(expr* guard) { expr_ref ng(m.mk_not(guard), m); return m_enabled_guards.contains(ng); } + scoped_ptr_vector m_propagation_queue; + unsigned m_qhead { 0 }; + + void push_body_expand(expr* e) { push(alloc(propagation_item, alloc(recfun::body_expansion, u(), to_app(e)))); } + void push_case_expand(expr* e) { push(alloc(propagation_item, alloc(recfun::case_expansion, u(), to_app(e)))); } + void push_guard(expr* e) { push(alloc(propagation_item, e)); } + void push_core(expr_ref_vector const& core) { push(alloc(propagation_item, core)); } + void push(propagation_item* p); + + bool is_enabled_guard(expr* guard) { return m_enabled_guards.contains(guard); } bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); } recfun::util & u() const { return m_util; } @@ -62,11 +68,11 @@ namespace smt { void activate_guard(expr* guard, expr_ref_vector const& guards); - void reset_queues(); expr_ref apply_args(unsigned depth, recfun::vars const & vars, expr_ref_vector const & args, expr * e); //!< substitute variables by args void assert_macro_axiom(recfun::case_expansion & e); void assert_case_axioms(recfun::case_expansion & e); void assert_body_axiom(recfun::body_expansion & e); + void block_core(expr_ref_vector const& core); literal mk_literal(expr* e); void disable_guard(expr* guard, expr_ref_vector const& guards); @@ -79,8 +85,6 @@ namespace smt { return vars.empty() || vars[vars.size()-1]->get_idx() == 0; } protected: - void push_case_expand(recfun::case_expansion* e) { m_q_case_expand.push_back(e); } - void push_body_expand(recfun::body_expansion* e) { m_q_body_expand.push_back(e); } bool internalize_atom(app * atom, bool gate_ctx) override; bool internalize_term(app * term) override; @@ -91,7 +95,6 @@ namespace smt { void assign_eh(bool_var v, bool is_true) override; void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; - void restart_eh() override; bool can_propagate() override; void propagate() override; bool should_research(expr_ref_vector &) override; @@ -104,7 +107,6 @@ namespace smt { theory_recfun(context& ctx); ~theory_recfun() override; theory * mk_fresh(context * new_ctx) override; - void init_search_eh() override; void display(std::ostream & out) const override; void collect_statistics(::statistics & st) const override; }; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 427aa48ac..f80c09f4b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7553,8 +7553,6 @@ namespace smt { // the thing we iterate over should just be variable_set - internal_variable_set // so we avoid computing the set difference (but this might be slower) for (expr* var : variable_set) { - //for(obj_hashtable::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { - //expr* var = *it; if (internal_variable_set.find(var) == internal_variable_set.end()) { TRACE("str", tout << "new variable: " << mk_pp(var, m) << std::endl;); strVarMap[var] = 1;