mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

more integration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-17 05:22:43 -07:00
parent c7d0d4e191
commit 9dd9d5e18a
3 changed files with 67 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/smt_context.h
View file

@ -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); } 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 { struct pp_lit {
smt::context & ctx; context & ctx;
smt::literal lit; literal lit;
pp_lit(smt::context & ctx, smt::literal lit) : ctx(ctx), lit(lit) {} pp_lit(context & ctx, literal lit) : ctx(ctx), lit(lit) {}
}; };
inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) { inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) {
pp.ctx.display_detailed_literal(out, pp.lit); return pp.ctx.display_detailed_literal(out, pp.lit);
return out;
} }
struct pp_lits { struct pp_lits {
smt::context & ctx; context & ctx;
smt::literal *lits; literal const *lits;
unsigned len; 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) { inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {

94
src/smt/theory_recfun.cpp
View file

@ -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 "util/stats.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "smt/theory_recfun.h" #include "smt/theory_recfun.h"
#include "smt/params/smt_params_helper.hpp" #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 { namespace smt {
@ -14,7 +32,11 @@ namespace smt {
m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))), m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()), m_util(m_plugin.u()),
m_trail(*this), 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) { bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
context & ctx = get_context(); context & ctx = get_context();
if (! ctx.e_internalized(atom)) { for (expr * arg : *atom) {
unsigned num_args = atom->get_num_args(); ctx.internalize(arg, false);
for (unsigned i = 0; i < num_args; ++i) }
ctx.internalize(atom->get_arg(i), false); if (!ctx.e_internalized(atom)) {
ctx.mk_enode(atom, false, true, false); 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); bool_var v = ctx.mk_bool_var(atom);
ctx.set_var_theory(v, get_id()); ctx.set_var_theory(v, get_id());
} }
@ -55,12 +77,14 @@ namespace smt {
bool theory_recfun::internalize_term(app * term) { bool theory_recfun::internalize_term(app * term) {
context & ctx = get_context(); 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. // the internalization of the arguments may have triggered the internalization of term.
if (ctx.e_internalized(term)) if (!ctx.e_internalized(term)) {
return true; ctx.mk_enode(term, false, false, true);
ctx.mk_enode(term, false, false, true); }
return true; // the theory doesn't actually map terms to variables return true;
} }
void theory_recfun::reset_queues() { 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 * then case-expand `n`. If it's a macro we can also immediately
* body-expand it. * body-expand it.
*/ */
void theory_recfun::relevant_eh(app * n) { void theory_recfun::relevant_eh(app * n) {
SASSERT(get_context().relevancy()); SASSERT(get_context().relevancy());
if (u().is_defined(n)) { 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); case_expansion e(u(), n);
push_case_expand(std::move(e)); push_case_expand(std::move(e));
} }
} }
void theory_recfun::push_scope_eh() { void theory_recfun::push_scope_eh() {
DEBUG("push_scope"); TRACEFN("push_scope");
theory::push_scope_eh(); theory::push_scope_eh();
m_trail.push_scope(); m_trail.push_scope();
} }
void theory_recfun::pop_scope_eh(unsigned num_scopes) { 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); m_trail.pop_scope(num_scopes);
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);
reset_queues(); reset_queues();
} }
void theory_recfun::restart_eh() { void theory_recfun::restart_eh() {
DEBUG("restart"); TRACEFN("restart");
reset_queues(); reset_queues();
theory::restart_eh(); theory::restart_eh();
} }
@ -120,7 +143,7 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
for (literal_vector & c : m_q_clauses) { 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()); ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr());
} }
m_q_clauses.clear(); m_q_clauses.clear();
@ -145,7 +168,7 @@ namespace smt {
} }
void theory_recfun::max_depth_conflict() { void theory_recfun::max_depth_conflict() {
DEBUG("max-depth conflict"); TRACEFN("max-depth conflict");
context & ctx = get_context(); context & ctx = get_context();
literal_vector c; literal_vector c;
// make clause `depth_limit => V_{g : guards} ~ g` // make clause `depth_limit => V_{g : guards} ~ g`
@ -160,20 +183,20 @@ namespace smt {
expr * g = & kv.get_key(); expr * g = & kv.get_key();
c.push_back(~ ctx.get_literal(g)); 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 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)); 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) { void theory_recfun::assign_eh(bool_var v, bool is_true) {
expr* e = get_context().bool_var2expr(v); expr* e = get_context().bool_var2expr(v);
if (!is_true) return; if (!is_true) return;
if (!is_app(e)) return; if (!is_app(e)) return;
app* a = to_app(e); app* a = to_app(e);
if (u().is_case_pred(a)) { 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 // add to set of local assumptions, for depth-limit purpose
{ {
m_guards.insert(e, empty()); m_guards.insert(e, empty());
@ -207,20 +230,19 @@ namespace smt {
} }
app_ref theory_recfun::apply_pred(recfun::case_pred const & p, app_ref theory_recfun::apply_pred(recfun::case_pred const & p,
ptr_vector<expr> const & args){ ptr_vector<expr> const & args) {
app_ref res(u().mk_case_pred(p, args), m()); return app_ref(u().mk_case_pred(p, args), m());
return res;
} }
void theory_recfun::assert_macro_axiom(case_expansion & e) { 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()); SASSERT(e.m_def->is_fun_macro());
expr_ref lhs(e.m_lhs, m()); expr_ref lhs(e.m_lhs, m());
context & ctx = get_context(); context & ctx = get_context();
auto & vars = e.m_def->get_vars(); auto & vars = e.m_def->get_vars();
// substitute `e.args` into the macro RHS // substitute `e.args` into the macro RHS
expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m()); 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` // now build the axiom `lhs = rhs`
ctx.internalize(rhs, false); ctx.internalize(rhs, false);
// add unit clause `lhs=rhs` // add unit clause `lhs=rhs`
@ -228,12 +250,12 @@ namespace smt {
ctx.mark_as_relevant(l); ctx.mark_as_relevant(l);
literal_vector lits; literal_vector lits;
lits.push_back(l); 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()); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
} }
void theory_recfun::assert_case_axioms(case_expansion & e) { 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"); << " with " << e.m_def->get_cases().size() << " cases");
SASSERT(e.m_def->is_fun_defined()); SASSERT(e.m_def->is_fun_defined());
context & ctx = get_context(); context & ctx = get_context();
@ -264,7 +286,7 @@ namespace smt {
//TRACE("recfun", tout << "assert_case_axioms " << pp_case_expansion(e) //TRACE("recfun", tout << "assert_case_axioms " << pp_case_expansion(e)
// << " axiom " << mk_pp(*l) <<"\n";); // << " 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()); 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 g = ctx.get_literal(_g);
literal c[2] = {~ concl, 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); get_context().mk_th_axiom(get_id(), 2, c);
} }
} }
@ -288,7 +310,7 @@ namespace smt {
} }
void theory_recfun::assert_body_axiom(body_expansion & e) { 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(); context & ctx = get_context();
recfun::def & d = *e.m_cdef->get_def(); recfun::def & d = *e.m_cdef->get_def();
auto & vars = d.get_vars(); auto & vars = d.get_vars();
@ -320,7 +342,7 @@ namespace smt {
literal l(mk_eq(lhs, rhs, true)); literal l(mk_eq(lhs, rhs, true));
ctx.mark_as_relevant(l); ctx.mark_as_relevant(l);
clause.push_back(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()); 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) { void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); 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); assumptions.push_back(dlimit);
} }
@ -354,7 +376,6 @@ namespace smt {
st.update("recfun body expansion", m_stats.m_body_expansions); 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) { 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) << ")"; return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")";
} }
@ -366,5 +387,4 @@ namespace smt {
} }
return out << ")"; return out << ")";
} }
#endif
} }

4
src/smt/theory_recfun.h
View file

@ -1,5 +1,5 @@
/*++ /*++
Copyright (c) 2006 Microsoft Corporation Copyright (c) 2018 Microsoft Corporation
Module Name: Module Name:
@ -11,7 +11,7 @@ Abstract:
Author: Author:
Leonardo de Moura (leonardo) 2008-10-31. Simon Cuares December 2017
Revision History: Revision History: