From b5676413e42db8094544c5b67d265b7d00ddca9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Oct 2018 18:25:27 -0700 Subject: [PATCH] recfun Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 1 + src/ast/recfun_decl_plugin.cpp | 60 ++++++++++++++-------------- src/ast/recfun_decl_plugin.h | 31 ++++++-------- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_context.h | 5 ++- src/smt/theory_recfun.cpp | 44 +++++++++++--------- src/smt/theory_recfun.h | 5 +-- 7 files changed, 75 insertions(+), 73 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d466d2e77..63b5a9e72 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1,4 +1,5 @@ + ############################################ # Copyright (c) 2012 Microsoft Corporation # diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 6ee0ddc39..e5796b119 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -15,6 +15,7 @@ Revision History: --*/ + #include #include #include "ast/expr_functors.h" @@ -29,14 +30,15 @@ Revision History: namespace recfun { - case_def::case_def(ast_manager &m, - family_id fid, - def * d, - std::string & name, - unsigned case_index, - sort_ref_vector const & arg_sorts, - expr_ref_vector const& guards, - expr* rhs) + case_def::case_def( + ast_manager &m, + family_id fid, + def * d, + std::string & name, + unsigned case_index, + sort_ref_vector const & arg_sorts, + expr_ref_vector const& guards, + expr* rhs) : m_pred(m), m_guards(guards), m_rhs(expr_ref(rhs,m)), @@ -52,11 +54,9 @@ namespace recfun { m_domain(m, arity, domain), m_range(range, m), m_vars(m), m_cases(), m_decl(m), - m_fid(fid), - m_macro(false) + m_fid(fid) { - SASSERT(arity == get_arity()); - + SASSERT(arity == get_arity()); func_decl_info info(fid, OP_FUN_DEFINED); m_decl = m.mk_func_decl(s, arity, domain, range, info); } @@ -124,7 +124,6 @@ namespace recfun { case_state() : m_reg(), m_branches() {} bool empty() const { return m_branches.empty(); } - region & reg() { return m_reg; } branch pop_branch() { branch res = m_branches.back(); @@ -135,7 +134,7 @@ namespace recfun { void push_branch(branch const & b) { m_branches.push_back(b); } unfold_lst const * cons_unfold(expr * e, unfold_lst const * next) { - return new (reg()) unfold_lst{e, next}; + return new (m_reg) unfold_lst{e, next}; } unfold_lst const * cons_unfold(expr * e1, expr * e2, unfold_lst const * next) { return cons_unfold(e1, cons_unfold(e2, next)); @@ -145,11 +144,11 @@ namespace recfun { } ite_lst const * cons_ite(app * ite, ite_lst const * next) { - return new (reg()) ite_lst{ite, next}; + return new (m_reg) ite_lst{ite, next}; } choice_lst const * cons_choice(app * ite, bool sign, choice_lst const * next) { - return new (reg()) choice_lst{ite, sign, next}; + return new (m_reg) choice_lst{ite, sign, next}; } }; @@ -203,21 +202,17 @@ namespace recfun { unsigned case_idx = 0; - std::string name; - name.append("case_"); + std::string name("case-"); name.append(m_name.bare_str()); - name.append("_"); m_vars.append(n_vars, vars); - // is the function a macro (unconditional body)? - m_macro = n_vars == 0 || !contains_ite(rhs); expr_ref_vector conditions(m); - if (m_macro) { + // is the function a macro (unconditional body)? + if (n_vars == 0 || !contains_ite(rhs)) { // constant function or trivial control flow, only one (dummy) case - name.append("dummy"); add_case(name, 0, conditions, rhs); return; } @@ -311,15 +306,15 @@ namespace recfun { */ util::util(ast_manager & m, family_id id) - : m_manager(m), m_family_id(id), m_th_rw(m), m_plugin(0) { - m_plugin = dynamic_cast(m.get_plugin(m_family_id)); + : m_manager(m), m_fid(id), m_th_rw(m), + m_plugin(dynamic_cast(m.get_plugin(m_fid))) { } util::~util() { } def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) { - return alloc(def, m(), m_family_id, name, n, domain, range); + return alloc(def, m(), m_fid, name, n, domain, range); } void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { @@ -328,7 +323,7 @@ namespace recfun { app_ref util::mk_depth_limit_pred(unsigned d) { parameter p(d); - func_decl_info info(m_family_id, OP_DEPTH_LIMIT, 1, &p); + 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); return app_ref(m().mk_const(decl), m()); } @@ -376,13 +371,13 @@ namespace recfun { m_defs.reset(); // m_case_defs does not own its data, no need to deallocate m_case_defs.reset(); - m_util = 0; // force deletion + m_util = nullptr; // force deletion } util & plugin::u() const { SASSERT(m_manager); SASSERT(m_family_id != null_family_id); - if (m_util.get() == 0) { + if (!m_util.get()) { m_util = alloc(util, *m_manager, m_family_id); } return *(m_util.get()); @@ -398,7 +393,7 @@ namespace recfun { void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { u().set_definition(d, n_vars, vars, rhs); for (case_def & c : d.get_def()->get_cases()) { - m_case_defs.insert(c.get_name(), &c); + m_case_defs.insert(c.get_decl(), &c); } } @@ -434,7 +429,10 @@ namespace recfun { func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - switch(k) { + UNREACHABLE(); + // TBD: parameter usage seems inconsistent with other uses. + IF_VERBOSE(0, verbose_stream() << "mk-func-decl " << k << "\n"); + switch (k) { case OP_FUN_CASE_PRED: return mk_fun_pred_decl(num_parameters, parameters, arity, domain, range); case OP_FUN_DEFINED: diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 2bfae9e4e..1e6f873e2 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -19,6 +19,7 @@ Revision History: #include "ast/ast.h" #include "ast/rewriter/th_rewriter.h" +#include "util/obj_hashtable.h" namespace recfun { class case_def; //get_name(); } + func_decl* get_decl() const { return m_pred; } app_ref apply_case_predicate(ptr_vector const & args) const { ast_manager& m = m_pred.get_manager(); @@ -97,7 +98,6 @@ namespace recfun { cases m_cases; //!< possible cases func_decl_ref m_decl; //!< generic declaration family_id m_fid; - bool m_macro; def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range); @@ -115,11 +115,10 @@ namespace recfun { sort_ref const & get_range() const { return m_range; } func_decl * get_decl() const { return m_decl.get(); } - bool is_fun_macro() const { return m_macro; } + bool is_fun_macro() const { return m_cases.size() == 1; } bool is_fun_defined() const { return !is_fun_macro(); } expr * get_macro_rhs() const { - SASSERT(is_fun_macro()); return m_cases[0].get_rhs(); } }; @@ -140,7 +139,7 @@ namespace recfun { class plugin : public decl_plugin { typedef map def_map; - typedef map case_def_map; + typedef obj_map case_def_map; mutable scoped_ptr m_util; def_map m_defs; // function->def @@ -175,8 +174,8 @@ namespace recfun { def const& get_def(const symbol& s) const { return *(m_defs[s]); } promise_def get_promise_def(const symbol &s) const { return promise_def(&u(), m_defs[s]); } def& get_def(symbol const& s) { return *(m_defs[s]); } - 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 has_case_def(func_decl* f) const { return m_case_defs.contains(f); } + case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); } bool is_declared(symbol const& s) const { return m_defs.contains(s); } private: func_decl * mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters, @@ -192,7 +191,7 @@ namespace recfun { friend class decl::plugin; ast_manager & m_manager; - family_id m_family_id; + family_id m_fid; th_rewriter m_th_rw; decl::plugin * m_plugin; @@ -205,10 +204,10 @@ namespace recfun { ast_manager & m() { return m_manager; } th_rewriter & get_th_rewriter() { return m_th_rw; } - bool is_case_pred(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); } - bool is_defined(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); } - 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 is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); } + bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); } + bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); } + bool owns_app(app * e) const { return e->get_family_id() == m_fid; } bool has_def() const { return m_plugin->has_def(); } @@ -222,17 +221,13 @@ namespace recfun { case_def& get_case_def(expr* e) { SASSERT(is_case_pred(e)); - return get_case_def(to_app(e)->get_name()); - } - - case_def& get_case_def(symbol const & s) { - SASSERT(m_plugin->has_case_def(s)); - return m_plugin->get_case_def(s); + return m_plugin->get_case_def(to_app(e)->get_decl()); } app* mk_fun_defined(def const & d, unsigned n_args, expr * const * args) { return m().mk_app(d.get_decl(), n_args, args); } + app* mk_fun_defined(def const & d, ptr_vector const & args) { return mk_fun_defined(d, args.size(), args.c_ptr()); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 52e8f664c..37ed061b4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -97,5 +97,5 @@ def_module_params(module_name='smt', ('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.native', BOOL, False, 'use native rec-fun solver'), - ('recfun.max_depth', UINT, 50, 'maximum depth of unrolling for recursive functions') + ('recfun.max_depth', UINT, 2, 'maximum depth of unrolling for recursive functions') )) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 45341d368..f628b6e95 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1639,13 +1639,14 @@ namespace smt { }; inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) { - out << "clause{"; + out << "{"; bool first = true; for (unsigned i = 0; i < pp.len; ++i) { - if (first) { first = false; } else { out << " ∨ "; } + if (first) { first = false; } else { out << " or\n"; } pp.ctx.display_detailed_literal(out, pp.lits[i]); } return out << "}"; + } }; diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 0a91074ec..79060c631 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -33,7 +33,7 @@ namespace smt { m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))), m_util(m_plugin.u()), m_guard_preds(m), - m_max_depth(0), + m_max_depth(UINT_MAX), m_q_case_expand(), m_q_body_expand() { @@ -45,10 +45,12 @@ namespace smt { char const * theory_recfun::get_name() const { return "recfun"; } - void theory_recfun::init_search_eh() { - // obtain max depth via parameters - smt_params_helper p(ctx().get_params()); - set_max_depth(p.recfun_max_depth()); + 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) { @@ -121,7 +123,7 @@ namespace smt { unsigned new_lim = m_guard_preds_lim.size()-num_scopes; unsigned start = m_guard_preds_lim[new_lim]; for (unsigned i = start; i < m_guard_preds.size(); ++i) { - m_guards[m_guard_preds.get(i)->get_decl()].pop_back(); + m_guards[m_guard_preds.get(i)].pop_back(); } m_guard_preds.resize(start); m_guard_preds_lim.shrink(new_lim); @@ -177,7 +179,6 @@ namespace smt { c.push_back(~mk_literal(dlimit)); enable_trace("recfun"); TRACE("recfun", ctx().display(tout << c.back() << " " << dlimit << "\n");); - SASSERT(ctx().get_assignment(c.back()) == l_false); for (expr * g : guards) { c.push_back(mk_literal(g)); @@ -194,17 +195,17 @@ namespace smt { expr* e = ctx().bool_var2expr(v); if (is_true && u().is_case_pred(e)) { TRACEFN("assign_case_pred_true " << mk_pp(e, m)); - app* a = to_app(e); // body-expand - body_expansion b_e(u(), a); + body_expansion b_e(u(), to_app(e)); push_body_expand(std::move(b_e)); } } // replace `vars` by `args` in `e` - expr_ref theory_recfun::apply_args(recfun::vars const & vars, - ptr_vector const & args, - expr * e) { + expr_ref theory_recfun::apply_args( + recfun::vars const & vars, + ptr_vector const & args, + expr * e) { SASSERT(is_standard_order(vars)); var_subst subst(m, true); expr_ref new_body(m); @@ -245,14 +246,14 @@ namespace smt { * 2. add unit clause `f(args) = rhs` */ void theory_recfun::assert_macro_axiom(case_expansion & e) { - TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n"); + TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n"); SASSERT(e.m_def->is_fun_macro()); auto & vars = e.m_def->get_vars(); expr_ref lhs(e.m_lhs, m); expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m); literal lit = mk_eq_lit(lhs, rhs); ctx().mk_th_axiom(get_id(), 1, &lit); - TRACEFN("macro expansion yields " << mk_pp(rhs,m) << "\n" << + TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" << "literal " << pp_lit(ctx(), lit)); } @@ -291,9 +292,10 @@ namespace smt { assert_body_axiom(be); // add to set of local assumptions, for depth-limit purpose - func_decl* d = pred_applied->get_decl(); + + // func_decl* d = pred_applied->get_decl(); m_guard_preds.push_back(pred_applied); - auto& vec = m_guards.insert_if_not_there2(d, ptr_vector())->get_data().m_value; + auto& vec = m_guards.insert_if_not_there2(e.m_lhs, ptr_vector())->get_data().m_value; vec.push_back(pred_applied); if (vec.size() == get_max_depth()) { max_depth_limit(vec); @@ -322,11 +324,17 @@ namespace smt { for (auto & g : e.m_cdef->get_guards()) { expr_ref guard = apply_args(vars, args, g); clause.push_back(~mk_literal(guard)); + if (clause.back() == true_literal) { + return; + } + if (clause.back() == false_literal) { + clause.pop_back(); + } } clause.push_back(mk_eq_lit(lhs, rhs)); ctx().mk_th_axiom(get_id(), clause); TRACEFN("body " << pp_body_expansion(e,m)); - TRACEFN("clause " << pp_lits(ctx(), clause)); + TRACEFN(pp_lits(ctx(), clause)); } final_check_status theory_recfun::final_check_eh() { @@ -373,7 +381,7 @@ namespace smt { } std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) { - out << "body_exp(" << e.e.m_cdef->get_name(); + out << "body_exp(" << e.e.m_cdef->get_decl()->get_name(); for (auto* t : e.e.m_args) { out << " " << mk_pp(t,e.m); } diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index f4783dcdc..68e2609d7 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -90,7 +90,7 @@ namespace smt { recfun_decl_plugin& m_plugin; recfun_util& m_util; stats m_stats; - obj_map > m_guards; + obj_map > m_guards; app_ref_vector m_guard_preds; unsigned_vector m_guard_preds_lim; unsigned m_max_depth; // for fairness and termination @@ -138,12 +138,11 @@ namespace smt { 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() const { return m_max_depth; } + unsigned get_max_depth(); public: theory_recfun(ast_manager & m); ~theory_recfun() override; - void init_search_eh() override; theory * mk_fresh(context * new_ctx) override; void display(std::ostream & out) const override; void collect_statistics(::statistics & st) const override;