mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-18 10:01:32 -07:00
parent 2f5f546990
commit d22a0d04ed
6 changed files with 144 additions and 126 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.h
View file

@ -707,6 +707,10 @@ public:
func_decl * get_decl() const { return m_decl; } func_decl * get_decl() const { return m_decl; }
family_id get_family_id() const { return get_decl()->get_family_id(); } family_id get_family_id() const { return get_decl()->get_family_id(); }
decl_kind get_decl_kind() const { return get_decl()->get_decl_kind(); } decl_kind get_decl_kind() const { return get_decl()->get_decl_kind(); }
symbol const& get_name() const { return get_decl()->get_name(); }
unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
parameter const* get_parameters() const { return get_decl()->get_parameters(); }
bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; } bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
unsigned get_num_args() const { return m_num_args; } unsigned get_num_args() const { return m_num_args; }
expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; } expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }

86
src/ast/recfun_decl_plugin.cpp
View file

@ -23,7 +23,7 @@ Revision History:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#define DEBUG(x) TRACE("recfun", tout << x << '\n';) #define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
#define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun " #_pred_); #define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun " #_pred_);
namespace recfun { namespace recfun {
@ -42,18 +42,18 @@ namespace recfun {
sort_ref_vector const & arg_sorts, sort_ref_vector const & arg_sorts,
unsigned num_guards, expr ** guards, expr* rhs) unsigned num_guards, expr ** guards, expr* rhs)
: m_pred(m, fid, name, arg_sorts), m_guards(m), m_rhs(expr_ref(rhs,m)), m_def(d) { : m_pred(m, fid, name, arg_sorts), m_guards(m), m_rhs(expr_ref(rhs,m)), m_def(d) {
for (unsigned i=0; i<num_guards; ++i) { for (unsigned i = 0; i < num_guards; ++i) {
m_guards.push_back(expr_ref(guards[i], m)); m_guards.push_back(guards[i]);
} }
} }
def::def(ast_manager &m, family_id fid, symbol const & s, def::def(ast_manager &m, family_id fid, symbol const & s,
unsigned arity, sort *const * domain, sort* range) unsigned arity, sort* const * domain, sort* range)
: m_manager(m), m_name(s), : m(m), m_name(s),
m_domain(m), m_range(range, m), m_vars(m), m_cases(), m_domain(m), m_range(range, m), m_vars(m), m_cases(),
m_decl(m), m_fid(fid), m_macro(false) m_decl(m), m_fid(fid), m_macro(false)
{ {
for (unsigned i=0; i < arity; ++i) for (unsigned i = 0; i < arity; ++i)
m_domain.push_back(domain[i]); m_domain.push_back(domain[i]);
SASSERT(arity == get_arity()); SASSERT(arity == get_arity());
@ -69,8 +69,8 @@ namespace recfun {
ite_find_p(ast_manager & m) : m(m) {} ite_find_p(ast_manager & m) : m(m) {}
virtual bool operator()(expr * e) { return m.is_ite(e); } virtual bool operator()(expr * e) { return m.is_ite(e); }
}; };
ite_find_p p(m()); ite_find_p p(m);
check_pred cp(p, m()); check_pred cp(p, m);
return cp(e); return cp(e);
} }
@ -108,8 +108,10 @@ namespace recfun {
ite_lst const * to_split; // `ite` terms to make a choice on ite_lst const * to_split; // `ite` terms to make a choice on
unfold_lst const * to_unfold; // terms yet to unfold unfold_lst const * to_unfold; // terms yet to unfold
branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : path(path), to_split(to_split), to_unfold(to_unfold) {} branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) :
branch(branch const & from) : path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {} path(path), to_split(to_split), to_unfold(to_unfold) {}
branch(branch const & from) :
path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {}
}; };
// state for computing cases from the RHS of a functions' definition // state for computing cases from the RHS of a functions' definition
@ -161,14 +163,14 @@ namespace recfun {
{ {
for (; choices != nullptr; choices = choices->next) { for (; choices != nullptr; choices = choices->next) {
app * ite = choices->ite; app * ite = choices->ite;
SASSERT(m.is_ite(ite)); expr* c = nullptr, *th = nullptr, *el = nullptr;
VERIFY(m.is_ite(ite, c, th, el));
// condition to add to the guard // condition to add to the guard
expr * cond0 = ite->get_arg(0); conditions.push_back(choices->sign ? c : m.mk_not(c));
conditions.push_back(choices->sign ? cond0 : m.mk_not(cond0));
// binding to add to the substitution // binding to add to the substitution
subst.insert(ite, choices->sign ? ite->get_arg(1) : ite->get_arg(2)); subst.insert(ite, choices->sign ? th : el);
} }
} }
@ -183,11 +185,11 @@ namespace recfun {
} }
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); case_def c(m, m_fid, this, name, get_domain(), n_conditions, conditions, rhs);
c.set_is_immediate(is_imm); c.set_is_immediate(is_imm);
DEBUG("add_case " << name << " " << mk_pp(rhs, m()) TRACEFN("add_case " << name << " " << mk_pp(rhs, m)
<< " :is_imm " << is_imm << " :is_imm " << is_imm
<< " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m())); << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m));
m_cases.push_back(c); m_cases.push_back(c);
} }
@ -197,12 +199,12 @@ namespace recfun {
unsigned n_vars, var *const * vars, expr* rhs0) unsigned n_vars, var *const * vars, expr* rhs0)
{ {
if (m_cases.size() != 0) { if (m_cases.size() != 0) {
DEBUG("bug: cases for " << m_name << " has cases already"); TRACEFN("bug: " << m_name << " has cases already");
UNREACHABLE(); UNREACHABLE();
} }
SASSERT(n_vars = m_domain.size()); SASSERT(n_vars = m_domain.size());
DEBUG("compute cases " << mk_pp(rhs0, m())); TRACEFN("compute cases " << mk_pp(rhs0, m));
unsigned case_idx = 0; unsigned case_idx = 0;
std::string name; std::string name;
@ -211,18 +213,18 @@ namespace recfun {
name.append(m_name.bare_str()); name.append(m_name.bare_str());
name.append("_"); name.append("_");
for (unsigned i=0; i<n_vars; ++i) for (unsigned i = 0; i < n_vars; ++i)
m_vars.push_back(vars[i]); m_vars.push_back(vars[i]);
#if 0 #if 0
// simplify `rhs` // simplify `rhs`
expr_ref simplified_rhs(m()); expr_ref simplified_rhs(m);
expr* rhs; expr* rhs;
th_rw.reset(); th_rw.reset();
th_rw(rhs0, simplified_rhs); th_rw(rhs0, simplified_rhs);
rhs = simplified_rhs.get(); rhs = simplified_rhs.get();
DEBUG("simplified into " << mk_pp(rhs, m())); TRACEFN("simplified into " << mk_pp(rhs, m()));
#else #else
expr* rhs = rhs0; expr* rhs = rhs0;
#endif #endif
@ -241,14 +243,14 @@ namespace recfun {
// rebuilding a `ite`-free RHS on the fly for each path in `rhs`. // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.
// Each such `ite`-free term is converted into a case_def and added to definition. // Each such `ite`-free term is converted into a case_def and added to definition.
case_state st(m()); case_state st(m);
{ {
branch b(nullptr, nullptr, st.mk_unfold_lst(rhs)); branch b(nullptr, nullptr, st.mk_unfold_lst(rhs));
st.push_branch(b); st.push_branch(b);
} }
while (! st.empty()) { while (! st.empty()) {
DEBUG("main loop iter"); TRACEFN("main loop iter");
branch b = st.pop_branch(); branch b = st.pop_branch();
@ -264,15 +266,15 @@ namespace recfun {
expr * e = stack.back(); expr * e = stack.back();
stack.pop_back(); stack.pop_back();
if (m().is_ite(e)) { if (m.is_ite(e)) {
// need to do a case split on `e`, forking the search space // need to do a case split on `e`, forking the search space
b.to_split = st.cons_ite(to_app(e), b.to_split); b.to_split = st.cons_ite(to_app(e), b.to_split);
} else if (is_app(e)) { }
else if (is_app(e)) {
// explore arguments // explore arguments
app * a = to_app(e); for (expr * arg : *to_app(e)) {
stack.push_back(arg);
for (unsigned i=0; i < a->get_num_args(); ++i) }
stack.push_back(a->get_arg(i));
} }
} }
} }
@ -280,7 +282,8 @@ namespace recfun {
if (b.to_split != nullptr) { if (b.to_split != nullptr) {
// split one `ite`, which will lead to distinct (sets of) cases // split one `ite`, which will lead to distinct (sets of) cases
app * ite = b.to_split->ite; app * ite = b.to_split->ite;
SASSERT(m().is_ite(ite)); expr* c = nullptr, *th = nullptr, *el = nullptr;
VERIFY(m.is_ite(ite, c, th, el));
/* explore both positive choice and negative choice. /* explore both positive choice and negative choice.
* each contains a longer path, with `ite` mapping to `true` (resp. `false), * each contains a longer path, with `ite` mapping to `true` (resp. `false),
@ -291,10 +294,11 @@ namespace recfun {
branch b_pos(st.cons_choice(ite, true, b.path), branch b_pos(st.cons_choice(ite, true, b.path),
b.to_split->next, b.to_split->next,
st.cons_unfold(ite->get_arg(0), ite->get_arg(1), b.to_unfold)); st.cons_unfold(c, th, b.to_unfold));
branch b_neg(st.cons_choice(ite, false, b.path), branch b_neg(st.cons_choice(ite, false, b.path),
b.to_split->next, b.to_split->next,
st.cons_unfold(ite->get_arg(0), ite->get_arg(2), b.to_unfold)); st.cons_unfold(c, el, b.to_unfold));
st.push_branch(b_neg); st.push_branch(b_neg);
st.push_branch(b_pos); st.push_branch(b_pos);
@ -302,20 +306,20 @@ namespace recfun {
else { else {
// leaf of the search tree // leaf of the search tree
expr_ref_vector conditions_raw(m()); expr_ref_vector conditions_raw(m);
expr_substitution subst(m()); expr_substitution subst(m);
convert_path(m(), b.path, conditions_raw, subst); convert_path(m, b.path, conditions_raw, subst);
// substitute, to get rid of `ite` terms // substitute, to get rid of `ite` terms
expr_ref case_rhs = replace_subst(th_rw, m(), subst, rhs); expr_ref case_rhs = replace_subst(th_rw, m, subst, rhs);
expr_ref_vector conditions(m()); expr_ref_vector conditions(m);
for (expr * g : conditions_raw) { for (expr * g : conditions_raw) {
expr_ref g_subst(replace_subst(th_rw, m(), subst, g), m()); expr_ref g_subst(replace_subst(th_rw, m, subst, g), m);
conditions.push_back(g_subst); conditions.push_back(g_subst);
} }
unsigned old_name_len = name.size(); size_t old_name_len = name.size();
{ // TODO: optimize? this does many copies { // TODO: optimize? this does many copies
std::ostringstream sout; std::ostringstream sout;
sout << ((unsigned long) case_idx); sout << ((unsigned long) case_idx);
@ -330,7 +334,7 @@ namespace recfun {
} }
} }
DEBUG("done analysing " << get_name()); TRACEFN("done analysing " << get_name());
} }
/* /*

13
src/ast/recfun_decl_plugin.h
View file

@ -33,12 +33,12 @@ namespace recfun {
OP_DEPTH_LIMIT, // predicate enforcing some depth limit OP_DEPTH_LIMIT, // predicate enforcing some depth limit
}; };
/*! A predicate `p(t1…tn)`, that, if true, means `f(t1…tn)` is following /*! A predicate `p(t1...tn)`, that, if true, means `f(t1...tn)` is following
a given path of its control flow and can be unrolled. a given path of its control flow and can be unrolled.
For example, `fact n := if n<2 then 1 else n * fact(n-1)` would have two cases, For example, `fact n := if n<2 then 1 else n * fact(n-1)` would have two cases,
and therefore two case predicates `C_fact_0` and `C_fact_1`, where and therefore two case predicates `C_fact_0` and `C_fact_1`, where
`C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `¬(t<2)` (second path). `C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `not (t<2)` (second path).
*/ */
class case_pred { class case_pred {
friend class case_def; friend class case_def;
@ -98,7 +98,7 @@ namespace recfun {
friend class promise_def; friend class promise_def;
typedef vector<case_def> cases; typedef vector<case_def> cases;
ast_manager & m_manager; ast_manager & m;
symbol m_name; //<! name of function symbol m_name; //<! name of function
sort_ref_vector m_domain; //<! type of arguments sort_ref_vector m_domain; //<! type of arguments
sort_ref m_range; //<! return type sort_ref m_range; //<! return type
@ -116,7 +116,6 @@ namespace recfun {
void add_case(std::string & name, unsigned n_conds, expr ** conditions, expr* rhs, bool is_imm = false); void add_case(std::string & name, unsigned n_conds, expr ** conditions, expr* rhs, bool is_imm = false);
bool contains_ite(expr* e); // expression contains a test? bool contains_ite(expr* e); // expression contains a test?
public: public:
ast_manager & m() const { return m_manager; }
symbol const & get_name() const { return m_name; } symbol const & get_name() const { return m_name; }
vars const & get_vars() const { return m_vars; } vars const & get_vars() const { return m_vars; }
cases & get_cases() { return m_cases; } cases & get_cases() { return m_cases; }
@ -237,9 +236,9 @@ namespace recfun {
ast_manager & m() { return m_manager; } ast_manager & m() { return m_manager; }
th_rewriter & get_th_rewriter() { return m_th_rw; } th_rewriter & get_th_rewriter() { return m_th_rw; }
bool is_case_pred(app * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); } bool is_case_pred(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); }
bool is_defined(app * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); } bool is_defined(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); }
bool is_depth_limit(app * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); } bool is_depth_limit(expr * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
bool owns_app(app * e) const { return e->get_family_id() == m_family_id; } bool owns_app(app * e) const { return e->get_family_id() == m_family_id; }
//<! add a function declaration //<! add a function declaration

4
src/smt/smt_context.h
View file

@ -859,6 +859,10 @@ namespace smt {
void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr); void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr);
void mk_th_axiom(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params);
}
/* /*
* Provide a hint to the core solver that the specified literals form a "theory case split". * Provide a hint to the core solver that the specified literals form a "theory case split".
* The core solver will enforce the condition that exactly one of these literals can be * The core solver will enforce the condition that exactly one of these literals can be

133
src/smt/theory_recfun.cpp
View file

@ -29,6 +29,7 @@ namespace smt {
theory_recfun::theory_recfun(ast_manager & m) theory_recfun::theory_recfun(ast_manager & m)
: theory(m.mk_family_id("recfun")), : theory(m.mk_family_id("recfun")),
m(m),
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),
@ -42,8 +43,8 @@ namespace smt {
theory_recfun::~theory_recfun() { theory_recfun::~theory_recfun() {
reset_queues(); reset_queues();
for (auto & kv : m_guards) { for (expr* g : m_guards) {
m().dec_ref(kv.m_key); m.dec_ref(g);
} }
m_guards.reset(); m_guards.reset();
} }
@ -61,28 +62,26 @@ 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();
for (expr * arg : *atom) { for (expr * arg : *atom) {
ctx.internalize(arg, false); ctx().internalize(arg, false);
} }
if (!ctx.e_internalized(atom)) { 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());
} }
return true; return true;
} }
bool theory_recfun::internalize_term(app * term) { bool theory_recfun::internalize_term(app * term) {
context & ctx = get_context();
for (expr* e : *term) { for (expr* e : *term) {
ctx.internalize(e, false); 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)) {
ctx.mk_enode(term, false, false, true); ctx().mk_enode(term, false, false, true);
} }
return true; return true;
} }
@ -108,7 +107,7 @@ namespace smt {
void theory_recfun::relevant_eh(app * n) { void theory_recfun::relevant_eh(app * n) {
SASSERT(ctx().relevancy()); SASSERT(ctx().relevancy());
if (u().is_defined(n)) { if (u().is_defined(n)) {
TRACEFN("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));
} }
@ -143,7 +142,7 @@ namespace smt {
for (literal_vector & c : m_q_clauses) { for (literal_vector & c : m_q_clauses) {
TRACEFN("add axiom " << pp_lits(ctx(), c)); 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);
} }
m_q_clauses.clear(); m_q_clauses.clear();
@ -176,8 +175,8 @@ namespace smt {
c.push_back(~mk_literal(dlimit)); c.push_back(~mk_literal(dlimit));
SASSERT(ctx().get_assignment(c.back()) == l_true); SASSERT(ctx().get_assignment(c.back()) == l_true);
} }
for (auto& kv : m_guards) { for (expr * g : m_guards) {
c.push_back(~ mk_literal(kv.m_key)); c.push_back(~ mk_literal(g));
} }
TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c)); 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
@ -185,18 +184,21 @@ namespace smt {
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 = ctx().bool_var2expr(v);
if (!is_true || !is_app(e)) return; if (!is_true || !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)) {
TRACEFN("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
SASSERT(!m_guards.contains(e)); SASSERT(!m_guards.contains(e));
m_guards.insert(e, empty()); m_guards.insert(e);
m().inc_ref(e); m.inc_ref(e);
insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m(), m_guards, e); insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m, m_guards, e);
m_trail.push(trail_elt); m_trail.push(trail_elt);
if (m_guards.size() > get_max_depth()) { if (m_guards.size() > get_max_depth()) {
@ -215,10 +217,9 @@ namespace smt {
expr_ref theory_recfun::apply_args(recfun::vars const & vars, expr_ref theory_recfun::apply_args(recfun::vars const & vars,
ptr_vector<expr> const & args, ptr_vector<expr> const & args,
expr * e) { expr * e) {
// check that var order is standard SASSERT(is_standard_order(vars));
SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0); var_subst subst(m, true);
var_subst subst(m(), true); expr_ref new_body(m);
expr_ref new_body(m());
new_body = subst(e, args.size(), args.c_ptr()); new_body = subst(e, args.size(), args.c_ptr());
ctx().get_rewriter()(new_body); // simplify ctx().get_rewriter()(new_body); // simplify
return new_body; return new_body;
@ -226,7 +227,7 @@ 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) {
return app_ref(u().mk_case_pred(p, args), m()); return app_ref(u().mk_case_pred(p, args), m);
} }
literal theory_recfun::mk_literal(expr* e) { literal theory_recfun::mk_literal(expr* e) {
@ -242,47 +243,54 @@ namespace smt {
return lit; return lit;
} }
/**
* For functions f(args) that are given as macros f(vs) = rhs
*
* 1. substitute `e.args` for `vs` into the macro rhs
* 2. add unit clause `f(args) = rhs`
*/
void theory_recfun::assert_macro_axiom(case_expansion & e) { void theory_recfun::assert_macro_axiom(case_expansion & e) {
TRACEFN("assert_macro_axiom " << pp_case_expansion(e, m()));
SASSERT(e.m_def->is_fun_macro()); SASSERT(e.m_def->is_fun_macro());
auto & vars = e.m_def->get_vars(); auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m()); expr_ref lhs(e.m_lhs, m);
// 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());
TRACEFN("macro expansion yields" << mk_pp(rhs,m()));
// add unit clause `lhs = rhs`
literal lit = mk_eq_lit(lhs, rhs); literal lit = mk_eq_lit(lhs, rhs);
TRACEFN("assert_macro_axiom: " << pp_lit(ctx(), lit));
ctx().mk_th_axiom(get_id(), 1, &lit); ctx().mk_th_axiom(get_id(), 1, &lit);
TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n" <<
"macro expansion yields " << mk_pp(rhs,m) << "\n" <<
"literal " << pp_lit(ctx(), lit));
} }
/**
* Add case axioms for every case expansion path.
*
* assert `p(args) <=> And(guards)` (with CNF on the fly)
*
* also body-expand paths that do not depend on any defined fun
*/
void theory_recfun::assert_case_axioms(case_expansion & e) { void theory_recfun::assert_case_axioms(case_expansion & e) {
TRACEFN("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());
// add case-axioms for all case-paths // add case-axioms for all case-paths
auto & vars = e.m_def->get_vars(); auto & vars = e.m_def->get_vars();
for (recfun::case_def const & c : e.m_def->get_cases()) { for (recfun::case_def const & c : e.m_def->get_cases()) {
// applied predicate to `args` // applied predicate to `args`
literal_vector guards;
for (auto & g : c.get_guards()) {
expr_ref guard = apply_args(vars, e.m_args, g);
guards.push_back(~mk_literal(guard));
}
app_ref pred_applied = apply_pred(c.get_pred(), e.m_args); app_ref pred_applied = apply_pred(c.get_pred(), e.m_args);
SASSERT(u().owns_app(pred_applied)); SASSERT(u().owns_app(pred_applied));
literal concl = mk_literal(pred_applied); literal concl = mk_literal(pred_applied);
// assert `p(args) <=> And(guards)` (with CNF on the fly) literal_vector guards;
guards.push_back(concl);
for (literal g : guards) { for (auto & g : c.get_guards()) {
literal c[2] = {~ concl, ~g}; expr_ref ga = apply_args(vars, e.m_args, g);
literal guard = mk_literal(ga);
guards.push_back(~guard);
literal c[2] = {~concl, guard};
ctx().mk_th_axiom(get_id(), 2, c); ctx().mk_th_axiom(get_id(), 2, c);
} }
guards.push_back(concl); ctx().mk_th_axiom(get_id(), guards);
ctx().mk_th_axiom(get_id(), guards.size(), guards.c_ptr());
// also body-expand paths that do not depend on any defined fun
if (c.is_immediate()) { if (c.is_immediate()) {
body_expansion be(c, e.m_args); body_expansion be(c, e.m_args);
assert_body_axiom(be); assert_body_axiom(be);
@ -290,20 +298,21 @@ namespace smt {
} }
} }
/**
* For a guarded definition guards => f(vars) = rhs
* and occurrence f(args)
*
* substitute `args` for `vars` in guards, and rhs
* add axiom guards[args/vars] => f(args) = rhs[args/vars]
*
*/
void theory_recfun::assert_body_axiom(body_expansion & e) { void theory_recfun::assert_body_axiom(body_expansion & e) {
TRACEFN("assert_body_axioms "<< pp_body_expansion(e,m()));
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();
auto & args = e.m_args; auto & args = e.m_args;
// check that var order is standard SASSERT(is_standard_order(vars));
SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0); expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref lhs(u().mk_fun_defined(d, args), m());
// substitute `e.args` into the RHS of this particular case
expr_ref rhs = apply_args(vars, args, e.m_cdef->get_rhs()); expr_ref rhs = apply_args(vars, args, e.m_cdef->get_rhs());
// substitute `e.args` into the guard of this particular case, to make
// the `condition` part of the clause `conds => lhs=rhs`
// now build the axiom `conds => lhs = rhs`
literal_vector clause; literal_vector clause;
for (auto & g : e.m_cdef->get_guards()) { for (auto & g : e.m_cdef->get_guards()) {
@ -311,8 +320,9 @@ namespace smt {
clause.push_back(~mk_literal(guard)); clause.push_back(~mk_literal(guard));
} }
clause.push_back(mk_eq_lit(lhs, rhs)); clause.push_back(mk_eq_lit(lhs, rhs));
TRACEFN("assert_body_axiom " << pp_lits(ctx(), clause)); ctx().mk_th_axiom(get_id(), clause);
ctx().mk_th_axiom(get_id(), clause.size(), clause.c_ptr()); TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN("clause " << pp_lits(ctx(), clause));
} }
final_check_status theory_recfun::final_check_eh() { final_check_status theory_recfun::final_check_eh() {
@ -321,15 +331,14 @@ 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());
TRACEFN("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);
} }
// if `dlimit` occurs in unsat core, return "unknown" // if `dlimit` occurs in unsat core, return "unknown"
lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) { lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
for (auto & e : unsat_core) { for (auto & e : unsat_core) {
if (is_app(e) && m_util.is_depth_limit(to_app(e))) if (u().is_depth_limit(e))
return l_undef; return l_undef;
} }
return l_false; return l_false;

18
src/smt/theory_recfun.h
View file

@ -33,7 +33,7 @@ namespace smt {
stats() { reset(); } stats() { reset(); }
}; };
// one case-expansion of `f(t1…tn)` // one case-expansion of `f(t1...tn)`
struct case_expansion { struct case_expansion {
expr * m_lhs; // the term to expand expr * m_lhs; // the term to expand
recfun_def * m_def; recfun_def * m_def;
@ -64,18 +64,16 @@ namespace smt {
friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &); friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &);
// one body-expansion of `f(t1…tn)` using a `C_f_i(t1…tn)` // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
struct body_expansion { struct body_expansion {
recfun_case_def const * m_cdef; recfun_case_def const * m_cdef;
ptr_vector<expr> m_args; ptr_vector<expr> m_args;
body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() { body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() {
SASSERT(u.is_case_pred(n)); SASSERT(u.is_case_pred(n));
func_decl * d = n->get_decl(); m_cdef = &u.get_case_def(n->get_name());
const symbol& name = d->get_name(); for (expr * arg : *n)
m_cdef = &u.get_case_def(name); m_args.push_back(arg);
for (unsigned i = 0; i < n->get_num_args(); ++i)
m_args.push_back(n->get_arg(i));
} }
body_expansion(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {} body_expansion(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {}
body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {} body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {}
@ -90,11 +88,11 @@ namespace smt {
friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &); friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
struct empty{};
typedef trail_stack<theory_recfun> th_trail_stack; typedef trail_stack<theory_recfun> th_trail_stack;
typedef obj_map<expr, empty> guard_set; typedef obj_hashtable<expr> guard_set;
ast_manager& m;
recfun_decl_plugin& m_plugin; recfun_decl_plugin& m_plugin;
recfun_util& m_util; recfun_util& m_util;
stats m_stats; stats m_stats;
@ -107,7 +105,6 @@ namespace smt {
vector<literal_vector> m_q_clauses; vector<literal_vector> m_q_clauses;
recfun_util & u() const { return m_util; } recfun_util & u() const { return m_util; }
ast_manager & m() { return get_manager(); }
bool is_defined(app * f) const { return u().is_defined(f); } bool is_defined(app * f) const { return u().is_defined(f); }
bool is_case_pred(app * f) const { return u().is_case_pred(f); } bool is_case_pred(app * f) const { return u().is_case_pred(f); }
@ -123,6 +120,7 @@ namespace smt {
void max_depth_conflict(void); void max_depth_conflict(void);
literal mk_literal(expr* e); literal mk_literal(expr* e);
literal mk_eq_lit(expr* l, expr* r); 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: protected:
void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); } void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); }
void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); } void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); }