mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix - change assumption tracking to be granular based on disabled guards

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-13 19:06:12 -07:00
parent e1027790ae
commit fe7146d93b
6 changed files with 102 additions and 73 deletions

13
src/ast/ast.h
View file

@ -1887,6 +1887,10 @@ public:
return mk_app(decl, args.size(), args.c_ptr());
}
app* mk_app(func_decl* decl, ref_buffer<expr, ast_manager> const& args) {
return mk_app(decl, args.size(), args.c_ptr());
}
app* mk_app(func_decl* decl, ref_vector<app, ast_manager> const& args) {
return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
}
@ -2191,6 +2195,15 @@ public:
app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2, arg3); }
app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(m_basic_family_id, OP_OR, 4, args); }
app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); }
app * mk_and(ref_vector<expr, ast_manager> const& args) { return mk_and(args.size(), args.c_ptr()); }
app * mk_and(ptr_vector<expr> const& args) { return mk_and(args.size(), args.c_ptr()); }
app * mk_and(ref_buffer<expr, ast_manager> const& args) { return mk_and(args.size(), args.c_ptr()); }
app * mk_and(ptr_buffer<expr> const& args) { return mk_and(args.size(), args.c_ptr()); }
app * mk_or(ref_vector<expr, ast_manager> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_or(ptr_vector<expr> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_or(ref_buffer<expr, ast_manager> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_or(ptr_buffer<expr> const& args) { return mk_or(args.size(), args.c_ptr()); }
app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); }
app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }
app * mk_distinct(unsigned num_args, expr * const * args);

6
src/ast/recfun_decl_plugin.cpp
View file

@ -341,10 +341,10 @@ namespace recfun {
d.set_definition(subst, n_vars, vars, rhs1);
}
app_ref util::mk_depth_limit_pred(unsigned d) {
app_ref util::mk_num_rounds_pred(unsigned d) {
parameter p(d);
func_decl_info info(m_fid, OP_DEPTH_LIMIT, 1, &p);
func_decl* decl = m().mk_const_decl(symbol("recfun-depth-limit"), m().mk_bool_sort(), info);
func_decl_info info(m_fid, OP_NUM_ROUNDS, 1, &p);
func_decl* decl = m().mk_const_decl(symbol("recfun-num-rounds"), m().mk_bool_sort(), info);
return app_ref(m().mk_const(decl), m());
}

6
src/ast/recfun_decl_plugin.h
View file

@ -32,7 +32,7 @@ namespace recfun {
enum op_kind {
OP_FUN_DEFINED, // defined function with one or more cases, possibly recursive
OP_FUN_CASE_PRED, // predicate guarding a given control flow path
OP_DEPTH_LIMIT, // predicate enforcing some depth limit
OP_NUM_ROUNDS // predicate round
};
/*! A predicate `p(t1...tn)`, that, if true, means `f(t1...tn)` is following
@ -226,7 +226,7 @@ namespace recfun {
bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); }
bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); }
bool is_generated(func_decl* f) const { return is_defined(f) && f->get_parameter(0).get_int() == 1; }
bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); }
bool is_num_rounds(expr * e) const { return is_app_of(e, m_fid, OP_NUM_ROUNDS); }
bool owns_app(app * e) const { return e->get_family_id() == m_fid; }
//<! don't use native theory if recursive function declarations are not populated with defs
@ -257,7 +257,7 @@ namespace recfun {
return m_plugin->get_rec_funs();
}
app_ref mk_depth_limit_pred(unsigned d);
app_ref mk_num_rounds_pred(unsigned d);
};
}

3
src/smt/params/smt_params_helper.pyg
View file

@ -119,6 +119,5 @@ def_module_params(module_name='smt',
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
('recfun.depth', UINT, 2, 'initial depth for maxrec expansion')
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
))

138
src/smt/theory_recfun.cpp
View file

@ -34,10 +34,11 @@ namespace smt {
m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()),
m_preds(m),
m_max_depth(0),
m_disabled_guards(m),
m_enabled_guards(m),
m_num_rounds(0),
m_q_case_expand(),
m_q_body_expand()
{
m_q_body_expand() {
}
theory_recfun::~theory_recfun() {
@ -52,9 +53,7 @@ namespace smt {
void theory_recfun::init(context* ctx) {
theory::init(ctx);
smt_params_helper p(ctx->get_params());
m_max_depth = p.recfun_depth();
if (m_max_depth < 2) m_max_depth = 2;
m_num_rounds = 0;
}
void theory_recfun::init_search_eh() {
@ -115,6 +114,8 @@ namespace smt {
reset_queues();
m_stats.reset();
theory::reset_eh();
m_disabled_guards.reset();
m_enabled_guards.reset();
}
/*
@ -160,19 +161,20 @@ namespace smt {
}
bool theory_recfun::can_propagate() {
return ! (m_q_case_expand.empty() &&
m_q_body_expand.empty() &&
m_q_clauses.empty());
return
!m_q_case_expand.empty() ||
!m_q_body_expand.empty() ||
!m_q_clauses.empty();
}
void theory_recfun::propagate() {
for (literal_vector & c : m_q_clauses) {
TRACEFN("add axiom " << pp_lits(ctx(), c));
ctx().mk_th_axiom(get_id(), c);
}
m_q_clauses.clear();
for (unsigned i = 0; i < m_q_case_expand.size(); ++i) {
case_expansion* e = m_q_case_expand[i];
if (e->m_def->is_fun_macro()) {
@ -203,12 +205,16 @@ namespace smt {
* make clause `depth_limit => ~guard`
* the guard appears at a depth below the current cutoff.
*/
void theory_recfun::assert_max_depth_limit(expr* guard) {
void theory_recfun::disable_guard(expr* guard) {
expr_ref nguard(m.mk_not(guard), m);
if (is_disabled_guard(nguard))
return;
literal_vector c;
app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
c.push_back(~mk_literal(dlimit));
c.push_back(~mk_literal(guard));
TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
c.push_back(~mk_literal(guard));
m_disabled_guards.push_back(nguard);
TRACEFN("add clause\n" << pp_lits(ctx(), c));
m_q_clauses.push_back(std::move(c));
}
@ -219,7 +225,6 @@ namespace smt {
SASSERT(u().is_defined(e) || u().is_case_pred(e));
unsigned d = 0;
m_pred_depth.find(e, d);
TRACEFN("depth " << d << " " << mk_pp(e, m));
return d;
}
@ -243,7 +248,6 @@ namespace smt {
if ((u().is_defined(e) || u().is_case_pred(e)) && !m_pred_depth.contains(e)) {
m_pred_depth.insert(e, depth);
m_preds.push_back(e);
TRACEFN("depth " << depth << " : " << mk_pp(e, m));
}
}
@ -308,18 +312,17 @@ namespace smt {
*/
void theory_recfun::assert_macro_axiom(case_expansion & e) {
m_stats.m_macro_expansions++;
TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n");
TRACEFN("case expansion " << pp_case_expansion(e, m));
SASSERT(e.m_def->is_fun_macro());
auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m);
unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
if (m.has_trace_stream()) log_axiom_instantiation(ctx().bool_var2expr(lit.var()));
std::function<expr*(void)> fn = [&]() { return ctx().bool_var2expr(lit.var()); };
scoped_trace_stream _tr(*this, fn);
ctx().mk_th_axiom(get_id(), 1, &lit);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<
"literal " << pp_lit(ctx(), lit));
TRACEFN("macro expansion yields " << pp_lit(ctx(), lit));
}
/**
@ -331,9 +334,10 @@ namespace smt {
*/
void theory_recfun::assert_case_axioms(case_expansion & e) {
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());
// add case-axioms for all case-paths
// assert this was not defined before.
auto & vars = e.m_def->get_vars();
literal_vector preds;
expr_ref_vector pred_exprs(m);
@ -341,7 +345,6 @@ namespace smt {
// applied predicate to `args`
app_ref pred_applied = c.apply_case_predicate(e.m_args);
// cut off cases below max-depth
unsigned depth = get_depth(e.m_lhs);
set_depth(depth, pred_applied);
SASSERT(u().owns_app(pred_applied));
@ -351,13 +354,12 @@ namespace smt {
if (c.is_immediate()) {
body_expansion be(pred_applied, c, e.m_args);
assert_body_axiom(be);
assert_body_axiom(be);
}
else if (depth >= m_max_depth) {
assert_max_depth_limit(pred_applied);
else if (!is_enabled_guard(pred_applied)) {
disable_guard(pred_applied);
continue;
}
literal_vector guards;
expr_ref_vector exprs(m);
guards.push_back(concl);
@ -367,31 +369,19 @@ namespace smt {
guards.push_back(~guard);
exprs.push_back(m.mk_not(ga));
literal c[2] = {~concl, guard};
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(pred_applied, ga);
log_axiom_instantiation(body);
}
std::function<expr*(void)> fn = [&]() { return m.mk_implies(pred_applied, ga); };
scoped_trace_stream _tr(*this, fn);
ctx().mk_th_axiom(get_id(), 2, c);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr()));
log_axiom_instantiation(body);
}
std::function<expr*(void)> fn1 = [&]() { return m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs)); };
scoped_trace_stream _tr1(*this, fn1);
ctx().mk_th_axiom(get_id(), guards);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
// the disjunction of branches is asserted
// to close the available cases.
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_or(pred_exprs.size(), pred_exprs.c_ptr());
log_axiom_instantiation(body);
}
std::function<expr*(void)> fn2 = [&]() { return m.mk_or(pred_exprs); };
scoped_trace_stream _tr2(*this, fn2);
ctx().mk_th_axiom(get_id(), preds);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
/**
@ -410,7 +400,6 @@ namespace smt {
unsigned depth = get_depth(e.m_pred);
expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
literal_vector clause;
expr_ref_vector exprs(m);
for (auto & g : e.m_cdef->get_guards()) {
@ -426,14 +415,10 @@ namespace smt {
}
}
clause.push_back(mk_eq_lit(lhs, rhs));
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs));
log_axiom_instantiation(body);
}
std::function<expr*(void)> fn = [&]() { return m.mk_implies(m.mk_and(exprs), m.mk_eq(lhs, rhs)); };
scoped_trace_stream _tr(*this, fn);
ctx().mk_th_axiom(get_id(), clause);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN(pp_lits(ctx(), clause));
}
@ -447,27 +432,54 @@ namespace smt {
}
void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
if (u().has_defs()) {
app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
if (u().has_defs() || !m_disabled_guards.empty()) {
app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
assumptions.push_back(dlimit);
assumptions.append(m_disabled_guards);
}
}
// if `dlimit` occurs in unsat core, return 'true'
// if `dlimit` or a disabled guard occurs in unsat core, return 'true'
bool theory_recfun::should_research(expr_ref_vector & unsat_core) {
bool found = false;
expr* to_delete = nullptr;
unsigned n = 0;
unsigned current_depth = UINT_MAX;
for (auto & e : unsat_core) {
if (u().is_depth_limit(e)) {
m_max_depth = (3 * m_max_depth) / 2;
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increase-depth " << m_max_depth << ")\n");
return true;
if (is_disabled_guard(e)) {
found = true;
expr* ne = nullptr;
VERIFY(m.is_not(e, ne));
unsigned depth = get_depth(ne);
if (depth < current_depth)
n = 0;
if (depth <= current_depth && (get_context().get_random_value() % (++n)) == 0) {
to_delete = e;
current_depth = depth;
}
}
else if (u().is_num_rounds(e)) {
found = true;
}
}
return false;
if (found) {
m_num_rounds++;
if (to_delete) {
m_disabled_guards.erase(to_delete);
m_enabled_guards.push_back(to_delete);
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard)\n");
}
else {
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increment-round)\n");
}
}
return found;
}
void theory_recfun::display(std::ostream & out) const {
out << "recfun{}\n";
out << "recfun\n";
out << "disabled guards:\n" << m_disabled_guards << "\n";
}
void theory_recfun::collect_statistics(::statistics & st) const {

9
src/smt/theory_recfun.h
View file

@ -95,15 +95,20 @@ namespace smt {
stats m_stats;
// book-keeping for depth of predicates
expr_ref_vector m_disabled_guards;
expr_ref_vector m_enabled_guards;
obj_map<expr, unsigned> m_pred_depth;
expr_ref_vector m_preds;
unsigned_vector m_preds_lim;
unsigned m_max_depth; // for fairness and termination
unsigned m_num_rounds;
ptr_vector<case_expansion> m_q_case_expand;
ptr_vector<body_expansion> m_q_body_expand;
vector<literal_vector> m_q_clauses;
bool is_enabled_guard(expr* guard) { expr_ref ng(m.mk_not(guard), m); return m_enabled_guards.contains(ng); }
bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); }
recfun::util & u() const { return m_util; }
bool is_defined(app * f) const { return u().is_defined(f); }
bool is_case_pred(app * f) const { return u().is_case_pred(f); }
@ -118,7 +123,7 @@ namespace smt {
void assert_body_axiom(body_expansion & e);
literal mk_literal(expr* e);
void assert_max_depth_limit(expr* guard);
void disable_guard(expr* guard);
unsigned get_depth(expr* e);
void set_depth(unsigned d, expr* e);
void set_depth_rec(unsigned d, expr* e);