From 35eb6eccd1daaacbcda760a43f25f37e0a3eda56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Oct 2018 17:14:10 -0700 Subject: [PATCH] iterative deepening Signed-off-by: Nikolaj Bjorner --- src/ast/recfun_decl_plugin.cpp | 7 +-- src/smt/smt_context.cpp | 34 +++++++++++--- src/smt/smt_context.h | 4 +- src/smt/smt_theory.h | 9 ++++ src/smt/theory_recfun.cpp | 85 +++++++++++++++++++++------------- src/smt/theory_recfun.h | 15 ++---- 6 files changed, 101 insertions(+), 53 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index de8bf94b1..1cd9a4fb8 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -184,7 +184,8 @@ namespace recfun { return res; } - void def::add_case(std::string & name, unsigned n_conditions, expr ** conditions, expr * rhs, bool is_imm) { + void def::add_case(std::string & name, unsigned n_conditions, + expr ** conditions, expr * rhs, bool is_imm) { case_def c(m, m_fid, this, name, get_domain(), n_conditions, conditions, rhs); c.set_is_immediate(is_imm); TRACEFN("add_case " << name << " " << mk_pp(rhs, m) @@ -202,7 +203,7 @@ namespace recfun { TRACEFN("bug: " << m_name << " has cases already"); UNREACHABLE(); } - SASSERT(n_vars = m_domain.size()); + SASSERT(n_vars == m_domain.size()); TRACEFN("compute cases " << mk_pp(rhs0, m)); @@ -235,7 +236,7 @@ namespace recfun { if (m_macro) { // constant function or trivial control flow, only one (dummy) case name.append("dummy"); - add_case(name, 0, 0, rhs); + add_case(name, 0, nullptr, rhs); return; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f7b7bdbea..4b8b1b9d9 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3266,6 +3266,18 @@ namespace smt { m_assumptions.reset(); } + bool context::should_research(lbool r) { + if (r != l_false || m_unsat_core.empty()) { + return false; + } + for (theory* th : m_theory_set) { + if (th->should_research(m_unsat_core)) { + return true; + } + } + return false; + } + lbool context::mk_unsat_core(lbool r) { if (r != l_false) return r; SASSERT(inconsistent()); @@ -3353,7 +3365,7 @@ namespace smt { add_theory_assumptions(theory_assumptions); if (!theory_assumptions.empty()) { TRACE("search", tout << "Adding theory assumptions to context" << std::endl;); - return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true); + return check(0, nullptr, reset_cancel); } internalize_assertions(); @@ -3407,19 +3419,23 @@ namespace smt { } } - lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) { + lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) { if (!check_preamble(reset_cancel)) return l_undef; SASSERT(at_base_level()); setup_context(false); expr_ref_vector asms(m_manager, num_assumptions, assumptions); - if (!already_did_theory_assumptions) add_theory_assumptions(asms); + add_theory_assumptions(asms); // introducing proxies: if (!validate_assumptions(asms)) return l_undef; TRACE("unsat_core_bug", tout << asms << "\n";); internalize_assertions(); init_assumptions(asms); TRACE("before_search", display(tout);); - lbool r = search(); - r = mk_unsat_core(r); + lbool r; + do { + r = search(); + r = mk_unsat_core(r); + } + while (should_research(r)); r = check_finalize(r); return r; } @@ -3435,8 +3451,12 @@ namespace smt { internalize_assertions(); init_assumptions(asms); for (auto const& clause : clauses) init_clause(clause); - lbool r = search(); - r = mk_unsat_core(r); + lbool r; + do { + r = search(); + r = mk_unsat_core(r); + } + while (should_research(r)); r = check_finalize(r); return r; } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 5902f9b2c..45341d368 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1137,6 +1137,8 @@ namespace smt { void add_theory_assumptions(expr_ref_vector & theory_assumptions); lbool mk_unsat_core(lbool result); + + bool should_research(lbool result); void validate_unsat_core(); @@ -1524,7 +1526,7 @@ namespace smt { void pop(unsigned num_scopes); - lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false); + lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true); lbool check(expr_ref_vector const& cube, vector const& clauses); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index fa0ec0c82..15b0aeed6 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -194,6 +194,15 @@ namespace smt { return l_false; } + /** + \brief This method is called from the smt_context when an unsat core is generated. + The theory may tell the solver to perform iterative deepening by invalidating + this unsat core and increasing some resource constraints. + */ + virtual bool should_research(expr_ref_vector & unsat_core) { + return false; + } + /** \brief This method is invoked before the search starts. */ diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 220cfcbbf..6f62cccc0 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -32,12 +32,10 @@ namespace smt { m(m), m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))), m_util(m_plugin.u()), - m_trail(*this), - m_guards(), + m_guards(m), m_max_depth(0), m_q_case_expand(), - m_q_body_expand(), - m_q_clauses() + m_q_body_expand() { } @@ -89,11 +87,9 @@ namespace smt { void theory_recfun::reset_queues() { m_q_case_expand.reset(); m_q_body_expand.reset(); - m_q_clauses.reset(); } void theory_recfun::reset_eh() { - m_trail.reset(); reset_queues(); m_stats.reset(); theory::reset_eh(); @@ -116,12 +112,10 @@ namespace smt { void theory_recfun::push_scope_eh() { TRACEFN("push_scope"); theory::push_scope_eh(); - m_trail.push_scope(); } void theory_recfun::pop_scope_eh(unsigned num_scopes) { TRACEFN("pop_scope " << num_scopes); - m_trail.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); reset_queues(); } @@ -131,15 +125,15 @@ namespace smt { 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()); } - + void theory_recfun::propagate() { - + for (literal_vector & c : m_q_clauses) { TRACEFN("add axiom " << pp_lits(ctx(), c)); ctx().mk_th_axiom(get_id(), c); @@ -179,7 +173,7 @@ namespace smt { c.push_back(~ mk_literal(g)); } TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c)); - SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict + SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict m_q_clauses.push_back(std::move(c)); } @@ -190,26 +184,23 @@ namespace smt { */ void theory_recfun::assign_eh(bool_var v, bool is_true) { expr* e = ctx().bool_var2expr(v); - if (!is_true || !is_app(e)) return; - app* a = to_app(e); - if (u().is_case_pred(a)) { - TRACEFN("assign_case_pred_true "<< mk_pp(e,m)); + if (is_true && u().is_case_pred(e)) { + app* a = to_app(e); + TRACEFN("assign_case_pred_true " << mk_pp(e, m)); // add to set of local assumptions, for depth-limit purpose - SASSERT(!m_guards.contains(e)); - m_guards.insert(e); - m.inc_ref(e); - insert_ref_map trail_elt(m, m_guards, e); - m_trail.push(trail_elt); + SASSERT(!m_guards.contains(a)); + m_guards.push_back(a); + ctx().push_trail(push_back_vector(m_guards)); - if (m_guards.size() > get_max_depth()) { - // too many body-expansions: depth-limit conflict - max_depth_conflict(); - } - else { + if (m_guards.size() <= get_max_depth()) { // body-expand body_expansion b_e(u(), a); push_body_expand(std::move(b_e)); } + else { + // too many body-expansions: depth-limit conflict + max_depth_conflict(); + } } } @@ -238,7 +229,19 @@ namespace smt { } literal theory_recfun::mk_eq_lit(expr* l, expr* r) { - literal lit = mk_eq(l, r, false); + literal lit; + if (m.is_true(r) || m.is_false(r)) { + std::swap(l, r); + } + if (m.is_true(l)) { + lit = mk_literal(r); + } + else if (m.is_false(l)) { + lit = ~mk_literal(r); + } + else { + lit = mk_eq(l, r, false); + } ctx().mark_as_relevant(lit); return lit; } @@ -326,6 +329,21 @@ namespace smt { } final_check_status theory_recfun::final_check_eh() { + if (m_guards.size() > get_max_depth()) { +#if 1 + return FC_GIVEUP; +#else + for (unsigned i = get_max_depth(); i < m_guards.size(); ++i) { + app* a = m_guards.get(i); + body_expansion b_e(u(), a); + push_body_expand(std::move(b_e)); + } + unsigned new_depth = m_guards.size() + 1; + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :new-depth " << new_depth << ")\n"); + set_max_depth(new_depth); + return FC_CONTINUE; +#endif + } return FC_DONE; } @@ -335,13 +353,16 @@ namespace smt { assumptions.push_back(dlimit); } - // if `dlimit` occurs in unsat core, return "unknown" - lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) { + // if `dlimit` occurs in unsat core, return 'true' + bool theory_recfun::should_research(expr_ref_vector & unsat_core) { for (auto & e : unsat_core) { - if (u().is_depth_limit(e)) - return l_undef; + if (u().is_depth_limit(e)) { + unsigned new_depth = (3 * (1 + get_max_depth())) / 2; + set_max_depth(new_depth); + return true; + } } - return l_false; + return false; } void theory_recfun::display(std::ostream & out) const { diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 019ef7918..a2ec27314 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -72,8 +72,7 @@ namespace smt { body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() { SASSERT(u.is_case_pred(n)); m_cdef = &u.get_case_def(n->get_name()); - for (expr * arg : *n) - m_args.push_back(arg); + m_args.append(n->get_num_args(), n->get_args()); } body_expansion(recfun_case_def const & d, ptr_vector & args) : m_cdef(&d), m_args(args) {} body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {} @@ -88,16 +87,11 @@ namespace smt { friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &); - - typedef trail_stack th_trail_stack; - typedef obj_hashtable guard_set; - ast_manager& m; recfun_decl_plugin& m_plugin; recfun_util& m_util; stats m_stats; - th_trail_stack m_trail; - guard_set m_guards; // true case-preds + app_ref_vector m_guards; // true case-preds unsigned m_max_depth; // for fairness and termination vector m_q_case_expand; @@ -117,8 +111,8 @@ namespace smt { void assert_macro_axiom(case_expansion & e); void assert_case_axioms(case_expansion & e); void assert_body_axiom(body_expansion & e); - void max_depth_conflict(void); literal mk_literal(expr* e); + void max_depth_conflict(); literal mk_eq_lit(expr* l, expr* r); bool is_standard_order(recfun::vars const& vars) const { return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; } protected: @@ -137,7 +131,7 @@ namespace smt { void restart_eh() override; bool can_propagate() override; void propagate() override; - lbool validate_unsat_core(expr_ref_vector &) override; + bool should_research(expr_ref_vector &) override; void new_eq_eh(theory_var v1, theory_var v2) override {} void new_diseq_eh(theory_var v1, theory_var v2) override {} @@ -152,6 +146,7 @@ namespace smt { virtual void collect_statistics(::statistics & st) const override; unsigned get_max_depth() const { return m_max_depth; } void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; } + void inc_max_depth() { ++m_max_depth; } }; }