From 7b1e1d52e72dd06c2cf06a8604bb189c602eec14 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 6 Dec 2017 14:05:14 +0100 Subject: [PATCH] wip: conflicts for pruning branches with too many unrollings use the local assumption on depth to ensure the conflict clause is valid --- src/ast/recfun_decl_plugin.cpp | 38 +++++++--------- src/ast/recfun_decl_plugin.h | 2 +- src/smt/theory_recfun.cpp | 81 ++++++++++++++++++++++++++++------ 3 files changed, 85 insertions(+), 36 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index b8bf1637a..3ebd888c7 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -23,10 +23,9 @@ Revision History: #include "ast/ast_pp.h" #include "util/scoped_ptr_vector.h" -#define DEBUG(x) do { auto& out = std::cout; out << "recfun: "; x; out << '\n' << std::flush; } while(0) +#define DEBUG(x) TRACE("recfun", tout << x << '\n';) #define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun " #_pred_); - namespace recfun { case_pred::case_pred(ast_manager & m, family_id fid, std::string const & s, sort_ref_vector const & domain) : m_name(), m_name_buf(s), m_domain(domain), m_decl(m) @@ -186,10 +185,7 @@ namespace recfun { 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); - TRACE("recfun", tout << "add_case " << name << " " << mk_pp(rhs, m()) - << " :is_imm " << is_imm - << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m());); - DEBUG(out << "add_case " << name << " " << mk_pp(rhs, m()) + DEBUG("add_case " << name << " " << mk_pp(rhs, m()) << " :is_imm " << is_imm << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m())); m_cases.push_back(c); @@ -201,12 +197,12 @@ namespace recfun { unsigned n_vars, var *const * vars, expr* rhs0) { if (m_cases.size() != 0) { - TRACE("recfun", tout << "bug: cases for " << m_name << " has cases already";); + DEBUG("bug: cases for " << m_name << " has cases already"); UNREACHABLE(); } SASSERT(n_vars = m_domain.size()); - DEBUG(out << "compute cases " << mk_pp(rhs0, m())); + DEBUG("compute cases " << mk_pp(rhs0, m())); unsigned case_idx = 0; std::string name; @@ -226,7 +222,7 @@ namespace recfun { th_rw(rhs0, simplified_rhs); rhs = simplified_rhs.get(); - DEBUG(out << "simplified into " << mk_pp(rhs, m())); + DEBUG("simplified into " << mk_pp(rhs, m())); #else expr* rhs = rhs0; #endif @@ -252,7 +248,7 @@ namespace recfun { } while (! st.empty()) { - DEBUG(out << "main loop iter"); + DEBUG("main loop iter"); branch b = st.pop_branch(); @@ -334,7 +330,7 @@ namespace recfun { } } - TRACE("recfun", tout << "done analysing " << get_name();); + DEBUG("done analysing " << get_name()); } /* @@ -364,6 +360,12 @@ namespace recfun { return depth_limit_pred_ref(pred, *this); } + app_ref util::mk_depth_limit_pred(unsigned d) { + depth_limit_pred_ref p = get_depth_limit_pred(d); + app_ref res(m().mk_const(p->get_decl()), m()); + return res; + } + // used to know which `app` are from this theory struct is_imm_pred : is_immediate_pred { util & u; @@ -399,12 +401,13 @@ namespace recfun { depth_limit_pred::depth_limit_pred(ast_manager & m, family_id fid, unsigned d) : m_name_buf(), m_name(""), m_depth(d), m_decl(m) { // build name, then build decl - std::ostringstream tmpname(m_name_buf); - tmpname << "depth_limit_" << d; + std::ostringstream tmpname; + tmpname << "depth_limit_" << d << std::flush; + m_name_buf.append(tmpname.str()); m_name = symbol(m_name_buf.c_str()); parameter params[1] = { parameter(d) }; func_decl_info info(fid, OP_DEPTH_LIMIT, 1, params); - m_decl = m.mk_func_decl(m_name, 0, ((sort*const *)nullptr), m.mk_bool_sort(), info); + m_decl = m.mk_const_decl(m_name, m.mk_bool_sort(), info); } namespace decl { @@ -444,13 +447,6 @@ namespace recfun { } } - app_ref plugin::mk_depth_limit_pred(unsigned d) { - depth_limit_pred_ref p = u().get_depth_limit_pred(d); - app_ref res(m()); - m().mk_app(p->get_decl(), 0, nullptr, res); - return res; - } - def* plugin::mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs) { SASSERT(! m_defs.contains(name)); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 677a44302..272ab43c4 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -208,7 +208,6 @@ namespace recfun { bool has_case_def(const symbol& s) const { return m_case_defs.contains(s); } case_def& get_case_def(symbol const& s) { SASSERT(has_case_def(s)); return *(m_case_defs[s]); } bool is_declared(symbol const& s) const { return m_defs.contains(s); } - app_ref mk_depth_limit_pred(unsigned d); private: func_decl * mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); @@ -274,6 +273,7 @@ namespace recfun { } depth_limit_pred_ref get_depth_limit_pred(unsigned d); + app_ref mk_depth_limit_pred(unsigned d); }; } diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index db9f7d938..b572f0bf7 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -4,10 +4,18 @@ #include "smt/theory_recfun.h" #include "smt/params/smt_params_helper.hpp" -#define DEBUG(x) \ - do { \ - TRACE("recfun", tout << x << '\n';); \ - auto& out = std::cout; out << "recfun: "; out << x; out << '\n' << std::flush; } while(0) +#define DEBUG(x) TRACE("recfun", tout << x << '\n';) + +struct pp_lit { + smt::context & ctx; + smt::literal lit; + pp_lit(smt::context & ctx, smt::literal lit) : ctx(ctx), lit(lit) {} +}; + +std::ostream & operator<<(std::ostream & out, pp_lit const & pp) { + pp.ctx.display_detailed_literal(out, pp.lit); + return out; +} // NOTE: debug struct pp_lits { @@ -76,7 +84,6 @@ namespace smt { } bool theory_recfun::internalize_term(app * term) { - DEBUG("internalizing term: " << mk_pp(term, m())); context & ctx = get_context(); for (expr* e : *term) ctx.internalize(e, false); // the internalization of the arguments may have triggered the internalization of term. @@ -112,11 +119,13 @@ namespace smt { } void theory_recfun::push_scope_eh() { + DEBUG("push_scope"); theory::push_scope_eh(); m_trail.push_scope(); } void theory_recfun::pop_scope_eh(unsigned num_scopes) { + DEBUG("pop_scope"); m_trail.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); reset_queues(); @@ -151,20 +160,64 @@ namespace smt { m_q_body_expand.clear(); } + class depth_conflict_justification : public justification { + literal_vector lits; + theory_recfun * th; + ast_manager & m() const { return th->get_manager(); } + public: + depth_conflict_justification(theory_recfun * th, region & r, literal_vector const & lits) + : lits(lits), th(th) {} + depth_conflict_justification(depth_conflict_justification const & from) + : lits(from.lits), th(from.th) {} + depth_conflict_justification(depth_conflict_justification && from) + : lits(std::move(from.lits)), th(from.th) {} + char const * get_name() const override { return "depth-conflict"; } + theory_id get_from_theory() const override { return th->get_id(); } + + void get_antecedents(conflict_resolution & cr) override { + auto & ctx = cr.get_context(); + for (unsigned i=0; i < lits.size(); ++i) { + DEBUG("mark literal " << pp_lit(ctx, lits[i])); + cr.mark_literal(lits[i]); + } + } + proof * mk_proof(conflict_resolution & cr) override { + UNREACHABLE(); + /* FIXME: actual proof + app * lemma = m().mk_or(c.size(), c.c_ptr()); + return m().mk_lemma(m().mk_false(), lemma); + */ + } + }; + + void theory_recfun::max_depth_conflict() { DEBUG("max-depth conflict"); - // TODO: build clause from `m_guards` - /* context & ctx = get_context(); - region & r = ctx.get_region(); - ctx.set_conflict( - */ + literal_vector c; + // make clause `depth_limit => V_{g : guards} ~ g` + { + // first literal must be the depth limit one + app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth()); + ctx.internalize(dlimit, false); + c.push_back(~ ctx.get_literal(dlimit)); + SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true); + } + for (auto& kv : m_guards) { + expr * g = & kv.get_key(); + c.push_back(~ ctx.get_literal(g)); + } + DEBUG("max-depth conflict: add clause " << pp_lits(ctx, c.size(), c.c_ptr())); + SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict + region r; + + depth_conflict_justification js(this, r, c); + ctx.set_conflict(ctx.mk_justification(js)); } // if `is_true` and `v = C_f_i(t1…tn)`, then body-expand i-th case of `f(t1…tn)` void theory_recfun::assign_eh(bool_var v, bool is_true) { expr* e = get_context().bool_var2expr(v); - DEBUG("assign_eh "<< mk_pp(e,m())); if (!is_true) return; if (!is_app(e)) return; app* a = to_app(e); @@ -256,7 +309,6 @@ namespace smt { } // assert `p(args) <=> And(guards)` (with CNF on the fly) ctx.internalize(pred_applied, false); - // FIXME: we need to be informed wen `pred_applied` is true!! ctx.mark_as_relevant(ctx.get_bool_var(pred_applied)); literal concl = ctx.get_literal(pred_applied); { @@ -335,8 +387,9 @@ namespace smt { } void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { - DEBUG("add_theory_assumptions"); - // TODO: add depth-limit assumptions? + app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth()); + DEBUG("add_theory_assumption " << mk_pp(dlimit.get(), m())); + assumptions.push_back(dlimit); } void theory_recfun::display(std::ostream & out) const {