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

wip: conflicts for pruning branches with too many unrollings

Browse source 
use the local assumption on depth to ensure the conflict clause is valid
This commit is contained in:
Simon Cruanes 2017-12-06 14:05:14 +01:00
parent 06e0b12700
commit 7b1e1d52e7
3 changed files with 85 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/ast/recfun_decl_plugin.cpp
View file

@ -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));

2
src/ast/recfun_decl_plugin.h
View file

@ -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);
};
}

81
src/smt/theory_recfun.cpp
View file

@ -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 {