diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index af451f9c5..868b35d00 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -517,6 +517,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters void array_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT)); + sort_names.push_back(builtin_name("=>", ARRAY_SORT)); // TBD: this could easily break users even though it is already used in CVC4: // sort_names.push_back(builtin_name("Set", _SET_SORT)); } diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 1cd9a4fb8..cdd1cec92 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -27,13 +27,7 @@ Revision History: #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) - { - m_name = symbol(m_name_buf.c_str()); - func_decl_info info(fid, OP_FUN_CASE_PRED); - m_decl = m.mk_func_decl(m_name, domain.size(), domain.c_ptr(), m.mk_bool_sort(), info); - } + case_def::case_def(ast_manager &m, family_id fid, @@ -41,21 +35,20 @@ namespace recfun { std::string & name, sort_ref_vector const & arg_sorts, unsigned num_guards, expr ** guards, expr* rhs) - : m_pred(m, fid, name, arg_sorts), m_guards(m), m_rhs(expr_ref(rhs,m)), m_def(d) { - for (unsigned i = 0; i < num_guards; ++i) { - m_guards.push_back(guards[i]); - } + : m_pred(m), + m_guards(m, num_guards, guards), + m_rhs(expr_ref(rhs,m)), + m_def(d) { + func_decl_info info(fid, OP_FUN_CASE_PRED); + m_pred = m.mk_func_decl(symbol(name.c_str()), arg_sorts.size(), arg_sorts.c_ptr(), m.mk_bool_sort(), info); } def::def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort* const * domain, sort* range) : m(m), m_name(s), - m_domain(m), m_range(range, m), m_vars(m), m_cases(), + m_domain(m, arity, domain), m_range(range, m), m_vars(m), m_cases(), m_decl(m), m_fid(fid), m_macro(false) { - for (unsigned i = 0; i < arity; ++i) - m_domain.push_back(domain[i]); - SASSERT(arity == get_arity()); func_decl_info info(fid, OP_FUN_DEFINED); @@ -199,10 +192,11 @@ namespace recfun { void def::compute_cases(is_immediate_pred & is_i, th_rewriter & th_rw, unsigned n_vars, var *const * vars, expr* rhs0) { - if (m_cases.size() != 0) { + if (!m_cases.empty()) { TRACEFN("bug: " << m_name << " has cases already"); UNREACHABLE(); } + SASSERT(m_cases.empty()); SASSERT(n_vars == m_domain.size()); TRACEFN("compute cases " << mk_pp(rhs0, m)); @@ -343,14 +337,11 @@ 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_dlimit_map() { + : m_manager(m), m_family_id(id), m_th_rw(m), m_plugin(0) { m_plugin = dynamic_cast(m.get_plugin(m_family_id)); } util::~util() { - for (auto & kv : m_dlimit_map) { - dealloc(kv.m_value); - } } def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) { @@ -361,20 +352,11 @@ 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); - } - 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; + parameter p(d); + func_decl_info info(m_family_id, 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()); } // used to know which `app` are from this theory @@ -409,18 +391,6 @@ 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; - 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_const_decl(m_name, m.mk_bool_sort(), info); - } - namespace decl { plugin::plugin() : decl_plugin(), m_defs(), m_case_defs(), m_def_block() {} plugin::~plugin() { finalize(); } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index f2da9d053..cadbccfec 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -40,26 +40,12 @@ namespace recfun { and therefore two case predicates `C_fact_0` and `C_fact_1`, where `C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `not (t<2)` (second path). */ - class case_pred { - friend class case_def; - symbol m_name; //get_name(); } + + app_ref apply_case_predicate(ptr_vector const & args) const { + ast_manager& m = m_pred.get_manager(); + return app_ref(m.mk_app(m_pred, args.size(), args.c_ptr()), m); + } + def * get_def() const { return m_def; } expr_ref_vector const & get_guards() const { return m_guards; } expr * get_guards_c_ptr() const { return *m_guards.c_ptr(); } @@ -145,27 +136,6 @@ 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 { @@ -220,17 +190,15 @@ 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); + public: util(ast_manager &m, family_id); virtual ~util(); @@ -268,26 +236,12 @@ namespace recfun { app* mk_fun_defined(def const & d, ptr_vector const & args) { return mk_fun_defined(d, args.size(), args.c_ptr()); } - 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); app_ref mk_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/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 18b47d012..188e2331e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1135,14 +1135,17 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg if (num_args == 0 && range == nullptr) { if (fs.more_than_one()) - throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as ) to disumbiguate ", s); + throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as ) to disambiguate ", s); func_decl * f = fs.first(); if (f == nullptr) { throw cmd_exception("unknown constant ", s); } - if (f->get_arity() != 0) - throw cmd_exception("invalid function application, missing arguments ", s); - result = m().mk_const(f); + if (f->get_arity() != 0) { + result = array_util(m()).mk_as_array(f); + } + else { + result = m().mk_const(f); + } } else { func_decl * f = fs.find(m(), num_args, args, range); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 7458fc578..e60608ad3 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1439,6 +1439,12 @@ namespace smt2 { // compute match condition and substitution // t is shifted by size of subst. expr_ref bind_match(expr* t, expr* pattern, expr_ref_vector& subst) { + if (m().get_sort(t) != m().get_sort(pattern)) { + std::ostringstream str; + str << "sorts of pattern " << expr_ref(pattern, m()) << " and term " + << expr_ref(t, m()) << " are not aligned"; + throw parser_exception(str.str()); + } expr_ref tsh(m()); if (is_var(pattern)) { shifter()(t, 1, tsh); @@ -1894,13 +1900,31 @@ namespace smt2 { unsigned num_args = expr_stack().size() - fr->m_expr_spos; unsigned num_indices = m_param_stack.size() - fr->m_param_spos; expr_ref t_ref(m()); - m_ctx.mk_app(fr->m_f, - num_args, - expr_stack().c_ptr() + fr->m_expr_spos, - num_indices, - m_param_stack.c_ptr() + fr->m_param_spos, - fr->m_as_sort ? sort_stack().back() : nullptr, - t_ref); + local l; + if (m_env.find(fr->m_f, l)) { + push_local(l); + t_ref = expr_stack().back(); + for (unsigned i = 0; i < num_args; ++i) { + expr* arg = expr_stack().get(fr->m_expr_spos + i); + expr* args[2] = { t_ref.get(), arg }; + m_ctx.mk_app(symbol("select"), + 2, + args, + 0, + nullptr, + nullptr, + t_ref); + } + } + else { + m_ctx.mk_app(fr->m_f, + num_args, + expr_stack().c_ptr() + fr->m_expr_spos, + num_indices, + m_param_stack.c_ptr() + fr->m_param_spos, + fr->m_as_sort ? sort_stack().back() : nullptr, + t_ref); + } expr_stack().shrink(fr->m_expr_spos); m_param_stack.shrink(fr->m_param_spos); if (fr->m_as_sort) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 828e4f7de..c927b3214 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, 500, 'maximum depth of unrolling for recursive functions') + ('recfun.max_depth', UINT, 50, 'maximum depth of unrolling for recursive functions') )) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 5b02c5bbb..99ec09d1d 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -964,6 +964,7 @@ namespace smt { setup_seq_str(st); setup_card(); setup_fpa(); + setup_recfuns(); return; } diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 059a34f29..0a91074ec 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -83,6 +83,7 @@ namespace smt { void theory_recfun::reset_queues() { m_q_case_expand.reset(); m_q_body_expand.reset(); + m_q_clauses.clear(); } void theory_recfun::reset_eh() { @@ -146,7 +147,8 @@ namespace smt { } m_q_clauses.clear(); - for (case_expansion & e : m_q_case_expand) { + 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()) { // body expand immediately assert_macro_axiom(e); @@ -159,8 +161,8 @@ namespace smt { } m_q_case_expand.clear(); - for (body_expansion & e : m_q_body_expand) { - assert_body_axiom(e); + for (unsigned i = 0; i < m_q_body_expand.size(); ++i) { + assert_body_axiom(m_q_body_expand[i]); } m_q_body_expand.clear(); } @@ -173,6 +175,8 @@ namespace smt { // first literal must be the depth limit one app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); 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) { @@ -208,12 +212,7 @@ namespace smt { ctx().get_rewriter()(new_body); // simplify return new_body; } - - app_ref theory_recfun::apply_pred(recfun::case_pred const & p, - ptr_vector const & args) { - return app_ref(u().mk_case_pred(p, args), m); - } - + literal theory_recfun::mk_literal(expr* e) { ctx().internalize(e, false); literal lit = ctx().get_literal(e); @@ -246,14 +245,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"); 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("case expansion " << pp_case_expansion(e, m) << "\n" << - "macro expansion yields " << mk_pp(rhs,m) << "\n" << + TRACEFN("macro expansion yields " << mk_pp(rhs,m) << "\n" << "literal " << pp_lit(ctx(), lit)); } @@ -272,7 +271,7 @@ namespace smt { auto & vars = e.m_def->get_vars(); for (recfun::case_def const & c : e.m_def->get_cases()) { // applied predicate to `args` - app_ref pred_applied = apply_pred(c.get_pred(), e.m_args); + app_ref pred_applied = c.apply_case_predicate(e.m_args); SASSERT(u().owns_app(pred_applied)); literal concl = mk_literal(pred_applied); @@ -331,6 +330,11 @@ namespace smt { } final_check_status theory_recfun::final_check_eh() { + TRACEFN("final\n"); + if (can_propagate()) { + propagate(); + return FC_CONTINUE; + } return FC_DONE; } diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 265d8f305..f4783dcdc 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -108,7 +108,6 @@ namespace smt { void reset_queues(); expr_ref apply_args(recfun::vars const & vars, ptr_vector const & args, expr * e); //!< substitute variables by args - app_ref apply_pred(recfun::case_pred const & p, ptr_vector const & args); //