mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

validate unsat cores in recfun

Browse source
This commit is contained in:
Simon Cruanes 2017-12-25 23:35:54 +01:00
parent f7e5977b9e
commit cfcff78754
3 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/recfun_decl_plugin.h
View file

@ -239,6 +239,7 @@ namespace recfun {
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(app * 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(app * 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 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

14
src/smt/theory_recfun.cpp
View file

@ -193,14 +193,14 @@ namespace smt {
app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth()); app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth());
ctx.internalize(dlimit, false); ctx.internalize(dlimit, false);
c.push_back(~ ctx.get_literal(dlimit)); c.push_back(~ ctx.get_literal(dlimit));
//SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true); SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
} }
for (auto& kv : m_guards) { for (auto& kv : m_guards) {
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())); DEBUG("max-depth limit: 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 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));
} }
@ -373,6 +373,16 @@ namespace smt {
assumptions.push_back(dlimit); assumptions.push_back(dlimit);
} }
// if `dlimit` occurs in unsat core, return "unknown"
lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
for (auto & e : unsat_core) {
if (is_app(e) && m_util->is_depth_limit(to_app(e)))
return l_undef;
}
return l_false;
}
void theory_recfun::display(std::ostream & out) const { void theory_recfun::display(std::ostream & out) const {
out << "recfun{}"; out << "recfun{}";
} }

1
src/smt/theory_recfun.h
View file

@ -136,6 +136,7 @@ namespace smt {
void restart_eh() override; void restart_eh() override;
bool can_propagate() override; bool can_propagate() override;
void propagate() override; void propagate() override;
lbool validate_unsat_core(expr_ref_vector &) override;
void new_eq_eh(theory_var v1, theory_var v2) override {} void new_eq_eh(theory_var v1, theory_var v2) override {}
void new_diseq_eh(theory_var v1, theory_var v2) override {} void new_diseq_eh(theory_var v1, theory_var v2) override {}