mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

depth

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-22 04:59:51 -07:00
parent cd9c752834
commit 66f2a7636b
3 changed files with 12 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -96,6 +96,5 @@ def_module_params(module_name='smt',
('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'), ('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'), ('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'), ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
('recfun.native', BOOL, False, 'use native rec-fun solver'), ('recfun.native', BOOL, False, 'use native rec-fun solver')
('recfun.max_depth', UINT, 2, 'maximum depth of unrolling for recursive functions')
)) ))

26
src/smt/theory_recfun.cpp
View file

@ -34,7 +34,7 @@ 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_preds(m), m_preds(m),
m_max_depth(UINT_MAX), m_max_depth(2),
m_q_case_expand(), m_q_case_expand(),
m_q_body_expand() m_q_body_expand()
{ {
@ -46,14 +46,6 @@ namespace smt {
char const * theory_recfun::get_name() const { return "recfun"; } char const * theory_recfun::get_name() const { return "recfun"; }
unsigned theory_recfun::get_max_depth() {
if (m_max_depth == UINT_MAX) {
smt_params_helper p(ctx().get_params());
set_max_depth(p.recfun_max_depth());
}
return m_max_depth;
}
theory* theory_recfun::mk_fresh(context* new_ctx) { theory* theory_recfun::mk_fresh(context* new_ctx) {
return alloc(theory_recfun, new_ctx->get_manager()); return alloc(theory_recfun, new_ctx->get_manager());
} }
@ -177,7 +169,7 @@ namespace smt {
void theory_recfun::assert_max_depth_limit(expr* guard) { void theory_recfun::assert_max_depth_limit(expr* guard) {
TRACEFN("max-depth limit"); TRACEFN("max-depth limit");
literal_vector c; literal_vector c;
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
c.push_back(~mk_literal(dlimit)); c.push_back(~mk_literal(dlimit));
c.push_back(~mk_literal(guard)); c.push_back(~mk_literal(guard));
TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c)); TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
@ -202,8 +194,10 @@ namespace smt {
unsigned m_depth; unsigned m_depth;
insert_c(theory_recfun& th, unsigned d): th(th), m_depth(d) {} insert_c(theory_recfun& th, unsigned d): th(th), m_depth(d) {}
void operator()(app* e) { void operator()(app* e) {
if ((th.u().is_defined(e) || th.u().is_case_pred(e)) && !th.m_pred_depth.contains(e)) { if (th.u().is_defined(e) && !th.m_pred_depth.contains(e)) {
th.m_pred_depth.insert(e, m_depth); th.m_pred_depth.insert(e, m_depth);
th.m_preds.push_back(e);
TRACEFN("depth " << m_depth << " : " << mk_pp(e, th.m));
} }
} }
void operator()(quantifier*) {} void operator()(quantifier*) {}
@ -238,6 +232,7 @@ namespace smt {
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
set_depth(depth + 1, new_body);
return new_body; return new_body;
} }
@ -303,8 +298,8 @@ namespace smt {
app_ref pred_applied = c.apply_case_predicate(e.m_args); app_ref pred_applied = c.apply_case_predicate(e.m_args);
// cut off cases below max-depth // cut off cases below max-depth
unsigned depth = get_depth(pred_applied); unsigned depth = get_depth(e.m_lhs);
if (depth >= get_max_depth()) { if (depth >= m_max_depth) {
assert_max_depth_limit(pred_applied); assert_max_depth_limit(pred_applied);
continue; continue;
} }
@ -375,7 +370,7 @@ namespace smt {
void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
if (u().has_def()) { if (u().has_def()) {
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); app_ref dlimit = m_util.mk_depth_limit_pred(m_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);
} }
@ -385,8 +380,7 @@ namespace smt {
bool theory_recfun::should_research(expr_ref_vector & unsat_core) { bool theory_recfun::should_research(expr_ref_vector & unsat_core) {
for (auto & e : unsat_core) { for (auto & e : unsat_core) {
if (u().is_depth_limit(e)) { if (u().is_depth_limit(e)) {
unsigned new_depth = (3 * (1 + get_max_depth())) / 2; m_max_depth = (3 * m_max_depth) / 2;
set_max_depth(new_depth);
return true; return true;
} }
} }

4
src/smt/theory_recfun.h
View file

@ -149,13 +149,11 @@ namespace smt {
void new_diseq_eh(theory_var v1, theory_var v2) override {} void new_diseq_eh(theory_var v1, theory_var v2) override {}
void add_theory_assumptions(expr_ref_vector & assumptions) override; void add_theory_assumptions(expr_ref_vector & assumptions) override;
void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
unsigned get_max_depth();
public: public:
theory_recfun(ast_manager & m); theory_recfun(ast_manager & m);
~theory_recfun() override; ~theory_recfun() override;
theory * mk_fresh(context * new_ctx) override; theory * mk_fresh(context * new_ctx) override;
void init_search_eh() override { m_max_depth = 2; }
void display(std::ostream & out) const override; void display(std::ostream & out) const override;
void collect_statistics(::statistics & st) const override; void collect_statistics(::statistics & st) const override;
}; };