From 06e0b12700b85f90dfa344958642bc1e0fd2ab9b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 6 Dec 2017 13:01:54 +0100 Subject: [PATCH] add a predicate for depth limit assumptions --- src/ast/recfun_decl_plugin.cpp | 29 +++++++++++++++++++++++++- src/ast/recfun_decl_plugin.h | 38 ++++++++++++++++++++++++++++++++++ src/smt/params/smt_params.h | 2 +- 3 files changed, 67 insertions(+), 2 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 331114910..b8bf1637a 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -342,7 +342,7 @@ 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_manager(m), m_family_id(id), m_th_rw(m), m_plugin(0), m_dlimit_map() { m_plugin = dynamic_cast(m.get_plugin(m_family_id)); } @@ -354,6 +354,15 @@ namespace recfun { d.set_definition(n_vars, vars, rhs); } + // get or create predicate for depth limit + depth_limit_pred_ref util::get_depth_limit_pred(unsigned d) { + depth_limit_pred * pred = nullptr; + if (! m_dlimit_map.find(d, pred)) { + pred = alloc(depth_limit_pred, m(), m_family_id, d); + m_dlimit_map.insert(d, pred); + } + return depth_limit_pred_ref(pred, *this); + } // used to know which `app` are from this theory struct is_imm_pred : is_immediate_pred { @@ -387,6 +396,17 @@ namespace recfun { d->compute_cases(is_i, u->get_th_rewriter(), n_vars, vars, rhs); } + 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; + 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); + } + namespace decl { plugin::plugin() : decl_plugin(), m_defs(), m_case_defs(), m_def_block() {} plugin::~plugin() { finalize(); } @@ -424,6 +444,13 @@ 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)); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index e9b75a409..677a44302 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -30,6 +30,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 }; /*! A predicate `p(t1…tn)`, that, if true, means `f(t1…tn)` is following @@ -145,6 +146,27 @@ namespace recfun { def * get_def() const { return d; } }; + // predicate for limiting unrolling depth, to be used in assumptions and conflicts + class depth_limit_pred { + friend class util; + std::string m_name_buf; + symbol m_name; + unsigned m_depth; + func_decl_ref m_decl; + unsigned m_refcount; + + void inc_ref() { m_refcount ++; } + void dec_ref() { SASSERT(m_refcount > 0); m_refcount --; } + public: + depth_limit_pred(ast_manager & m, family_id fid, unsigned d); + unsigned get_depth() const { return m_depth; } + symbol const & get_name() const { return m_name; } + func_decl * get_decl() const { return m_decl.get(); } + }; + + // A reference to `depth_limit_pred` + typedef obj_ref depth_limit_pred_ref; + namespace decl { class plugin : public decl_plugin { @@ -186,6 +208,7 @@ 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); @@ -198,11 +221,14 @@ namespace recfun { // Varus utils for recursive functions class util { friend class decl::plugin; + + typedef map> depth_limit_map; ast_manager & m_manager; family_id m_family_id; th_rewriter m_th_rw; decl::plugin * m_plugin; + depth_limit_map m_dlimit_map; bool compute_is_immediate(expr * rhs); void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); @@ -237,10 +263,22 @@ namespace recfun { app* mk_case_pred(case_pred const & p, ptr_vector const & args) { return m().mk_app(p.get_decl(), args.size(), args.c_ptr()); } + + void inc_ref(depth_limit_pred * p) { p->inc_ref(); } + void dec_ref(depth_limit_pred * p) { + p->dec_ref(); + if (p->m_refcount == 0) { + m_dlimit_map.remove(p->m_depth); + dealloc(p); + } + } + + depth_limit_pred_ref get_depth_limit_pred(unsigned d); }; } typedef recfun::def recfun_def; typedef recfun::case_def recfun_case_def; +typedef recfun::depth_limit_pred recfun_depth_limit_pred; typedef recfun::decl::plugin recfun_decl_plugin; typedef recfun::util recfun_util; diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index e46b89401..330d284c4 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -261,7 +261,7 @@ struct smt_params : public preprocessor_params, m_display_features(false), m_new_core2th_eq(true), m_ematching(true), - m_recfun_max_depth(500), + m_recfun_max_depth(50), m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), m_lookahead_diseq(false),