From 9dd9d5e18ab9735001782e386cca0ce59bc8dbee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Oct 2018 05:22:43 -0700 Subject: [PATCH] more integration Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 17 ++++--- src/smt/theory_recfun.cpp | 94 ++++++++++++++++++++++++--------------- src/smt/theory_recfun.h | 4 +- 3 files changed, 67 insertions(+), 48 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 5049eb3fc..a349880e3 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1614,23 +1614,22 @@ namespace smt { void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } }; - struct pp_lit { - smt::context & ctx; - smt::literal lit; - pp_lit(smt::context & ctx, smt::literal lit) : ctx(ctx), lit(lit) {} + context & ctx; + literal lit; + pp_lit(context & ctx, literal lit) : ctx(ctx), lit(lit) {} }; inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) { - pp.ctx.display_detailed_literal(out, pp.lit); - return out; + return pp.ctx.display_detailed_literal(out, pp.lit); } struct pp_lits { - smt::context & ctx; - smt::literal *lits; + context & ctx; + literal const *lits; unsigned len; - pp_lits(smt::context & ctx, unsigned len, smt::literal *lits) : ctx(ctx), lits(lits), len(len) {} + pp_lits(context & ctx, unsigned len, literal const *lits) : ctx(ctx), lits(lits), len(len) {} + pp_lits(context & ctx, literal_vector const& ls) : ctx(ctx), lits(ls.c_ptr()), len(ls.size()) {} }; inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) { diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index dcb8ad097..b108512ba 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -1,11 +1,29 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation, Simon Cuares + +Module Name: + + theory_recfun.cpp + +Abstract: + + Theory responsible for unrolling recursive functions + +Author: + + Simon Cuares December 2017 + +Revision History: + +--*/ #include "util/stats.h" #include "ast/ast_util.h" #include "smt/theory_recfun.h" #include "smt/params/smt_params_helper.hpp" -#define DEBUG(x) TRACE("recfun", tout << x << '\n';) +#define TRACEFN(x) TRACE("recfun", tout << x << '\n';) namespace smt { @@ -14,7 +32,11 @@ namespace smt { m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))), m_util(m_plugin.u()), m_trail(*this), - m_guards(), m_max_depth(0), m_q_case_expand(), m_q_body_expand(), m_q_clauses() + m_guards(), + m_max_depth(0), + m_q_case_expand(), + m_q_body_expand(), + m_q_clauses() { } @@ -40,13 +62,13 @@ namespace smt { bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) { context & ctx = get_context(); - if (! ctx.e_internalized(atom)) { - unsigned num_args = atom->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) - ctx.internalize(atom->get_arg(i), false); + for (expr * arg : *atom) { + ctx.internalize(arg, false); + } + if (!ctx.e_internalized(atom)) { ctx.mk_enode(atom, false, true, false); } - if (! ctx.b_internalized(atom)) { + if (!ctx.b_internalized(atom)) { bool_var v = ctx.mk_bool_var(atom); ctx.set_var_theory(v, get_id()); } @@ -55,12 +77,14 @@ namespace smt { bool theory_recfun::internalize_term(app * term) { context & ctx = get_context(); - for (expr* e : *term) ctx.internalize(e, false); + 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)) - return true; - ctx.mk_enode(term, false, false, true); - return true; // the theory doesn't actually map terms to variables + if (!ctx.e_internalized(term)) { + ctx.mk_enode(term, false, false, true); + } + return true; } void theory_recfun::reset_queues() { @@ -77,35 +101,34 @@ namespace smt { } /* - * when `n` becomes relevant, if it's `f(t1…tn)` with `f` defined, + * when `n` becomes relevant, if it's `f(t1...tn)` with `f` defined, * then case-expand `n`. If it's a macro we can also immediately * body-expand it. */ void theory_recfun::relevant_eh(app * n) { SASSERT(get_context().relevancy()); if (u().is_defined(n)) { - DEBUG("relevant_eh: (defined) " << mk_pp(n, m())); - + TRACEFN("relevant_eh: (defined) " << mk_pp(n, m())); case_expansion e(u(), n); push_case_expand(std::move(e)); } } void theory_recfun::push_scope_eh() { - DEBUG("push_scope"); + TRACEFN("push_scope"); theory::push_scope_eh(); m_trail.push_scope(); } void theory_recfun::pop_scope_eh(unsigned num_scopes) { - DEBUG("pop_scope " << num_scopes); + TRACEFN("pop_scope " << num_scopes); m_trail.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); reset_queues(); } void theory_recfun::restart_eh() { - DEBUG("restart"); + TRACEFN("restart"); reset_queues(); theory::restart_eh(); } @@ -120,7 +143,7 @@ namespace smt { context & ctx = get_context(); for (literal_vector & c : m_q_clauses) { - DEBUG("add axiom " << pp_lits(ctx, c.size(), c.c_ptr())); + TRACEFN("add axiom " << pp_lits(ctx, c)); ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr()); } m_q_clauses.clear(); @@ -145,7 +168,7 @@ namespace smt { } void theory_recfun::max_depth_conflict() { - DEBUG("max-depth conflict"); + TRACEFN("max-depth conflict"); context & ctx = get_context(); literal_vector c; // make clause `depth_limit => V_{g : guards} ~ g` @@ -160,20 +183,20 @@ namespace smt { expr * g = & kv.get_key(); c.push_back(~ ctx.get_literal(g)); } - DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr())); + 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 m_q_clauses.push_back(std::move(c)); } - // if `is_true` and `v = C_f_i(t1…tn)`, then body-expand i-th case of `f(t1…tn)` + // 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); if (!is_true) return; if (!is_app(e)) return; app* a = to_app(e); if (u().is_case_pred(a)) { - DEBUG("assign_case_pred_true "<< mk_pp(e,m())); + TRACEFN("assign_case_pred_true "<< mk_pp(e,m())); // add to set of local assumptions, for depth-limit purpose { m_guards.insert(e, empty()); @@ -207,20 +230,19 @@ namespace smt { } app_ref theory_recfun::apply_pred(recfun::case_pred const & p, - ptr_vector const & args){ - app_ref res(u().mk_case_pred(p, args), m()); - return res; + ptr_vector const & args) { + return app_ref(u().mk_case_pred(p, args), m()); } void theory_recfun::assert_macro_axiom(case_expansion & e) { - DEBUG("assert_macro_axiom " << pp_case_expansion(e,m())); + TRACEFN("assert_macro_axiom " << pp_case_expansion(e,m())); SASSERT(e.m_def->is_fun_macro()); expr_ref lhs(e.m_lhs, m()); context & ctx = get_context(); auto & vars = e.m_def->get_vars(); // substitute `e.args` into the macro RHS expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m()); - DEBUG("macro expansion yields" << mk_pp(rhs,m())); + TRACEFN("macro expansion yields" << mk_pp(rhs,m())); // now build the axiom `lhs = rhs` ctx.internalize(rhs, false); // add unit clause `lhs=rhs` @@ -228,12 +250,12 @@ namespace smt { ctx.mark_as_relevant(l); literal_vector lits; lits.push_back(l); - DEBUG("assert_macro_axiom: " << pp_lits(ctx, lits.size(), lits.c_ptr())); + TRACEFN("assert_macro_axiom: " << pp_lits(ctx, lits)); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } void theory_recfun::assert_case_axioms(case_expansion & e) { - DEBUG("assert_case_axioms "<< pp_case_expansion(e,m()) + TRACEFN("assert_case_axioms "<< pp_case_expansion(e,m()) << " with " << e.m_def->get_cases().size() << " cases"); SASSERT(e.m_def->is_fun_defined()); context & ctx = get_context(); @@ -264,7 +286,7 @@ namespace smt { //TRACE("recfun", tout << "assert_case_axioms " << pp_case_expansion(e) // << " axiom " << mk_pp(*l) <<"\n";); - DEBUG("assert_case_axiom " << pp_lits(get_context(), path.size()+1, c.c_ptr())); + TRACEFN("assert_case_axiom " << pp_lits(get_context(), path.size()+1, c.c_ptr())); get_context().mk_th_axiom(get_id(), path.size()+1, c.c_ptr()); } { @@ -274,7 +296,7 @@ namespace smt { literal g = ctx.get_literal(_g); literal c[2] = {~ concl, g}; - DEBUG("assert_case_axiom " << pp_lits(get_context(), 2, c)); + TRACEFN("assert_case_axiom " << pp_lits(get_context(), 2, c)); get_context().mk_th_axiom(get_id(), 2, c); } } @@ -288,7 +310,7 @@ namespace smt { } void theory_recfun::assert_body_axiom(body_expansion & e) { - DEBUG("assert_body_axioms "<< pp_body_expansion(e,m())); + TRACEFN("assert_body_axioms "<< pp_body_expansion(e,m())); context & ctx = get_context(); recfun::def & d = *e.m_cdef->get_def(); auto & vars = d.get_vars(); @@ -320,7 +342,7 @@ namespace smt { literal l(mk_eq(lhs, rhs, true)); ctx.mark_as_relevant(l); clause.push_back(l); - DEBUG("assert_body_axiom " << pp_lits(ctx, clause.size(), clause.c_ptr())); + TRACEFN("assert_body_axiom " << pp_lits(ctx, clause)); ctx.mk_th_axiom(get_id(), clause.size(), clause.c_ptr()); } @@ -330,7 +352,7 @@ namespace smt { void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); - DEBUG("add_theory_assumption " << mk_pp(dlimit.get(), m())); + TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m())); assumptions.push_back(dlimit); } @@ -354,7 +376,6 @@ namespace smt { st.update("recfun body expansion", m_stats.m_body_expansions); } -#ifdef Z3DEBUG std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) { return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")"; } @@ -366,5 +387,4 @@ namespace smt { } return out << ")"; } -#endif } diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index a1d9048c1..68833be63 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2006 Microsoft Corporation +Copyright (c) 2018 Microsoft Corporation Module Name: @@ -11,7 +11,7 @@ Abstract: Author: - Leonardo de Moura (leonardo) 2008-10-31. + Simon Cuares December 2017 Revision History: