remove case-pred and depth-limit classes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<builtin_name>& 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));
 }

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) {
+        : m_pred(m),
-        for (unsigned i = 0; i < num_guards; ++i) {
+          m_guards(m, num_guards, guards), 
-            m_guards.push_back(guards[i]);
+          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<decl::plugin*>(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);
+        parameter p(d);
-        app_ref res(m().mk_const(p->get_decl()), m());
+        func_decl_info info(m_family_id, OP_DEPTH_LIMIT, 1, &p);
-        return res;
+        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(); }

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; //<! symbol for the predicate
-        std::string                 m_name_buf; //<! memory for m_name
-        sort_ref_vector const &     m_domain;
-        func_decl_ref               m_decl; //<! declaration for the predicate
-
-        case_pred(ast_manager & m, family_id fid, std::string const & s, sort_ref_vector const & args);
-    public:
-        symbol const & get_name() const { return m_name; }
-        sort_ref_vector const & get_domain() const { return m_domain; }
-        func_decl * get_decl() const { return m_decl.get(); }
-        unsigned get_arity() const { return m_domain.size(); }
-    };
 
     typedef var_ref_vector vars;
 
     class case_def {
         friend class def;
-        case_pred           m_pred; //<! predicate used for this case
+        func_decl_ref       m_pred; //<! predicate used for this case
         expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
         expr_ref            m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds
         def *               m_def; //<! definition this is a part of
@@ -76,8 +62,13 @@ namespace recfun {
 
         void add_guard(expr_ref && e) { m_guards.push_back(e); }
     public:
-        symbol const& get_name() const { return m_pred.get_name(); }
+        symbol const& get_name() const { return m_pred->get_name(); }
-        case_pred const & get_pred() const { return m_pred; }
+
+        app_ref apply_case_predicate(ptr_vector<expr> 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, util> 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<int, depth_limit_pred *, int_hash, default_eq<int>> 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<expr> const & args) {
             return mk_fun_defined(d, args.size(), args.c_ptr());
         }
-        app* mk_case_pred(case_pred const & p, ptr_vector<expr> 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;

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 <symbol> <sort>) to disumbiguate ", s);
+            throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disambiguate ", s);
         func_decl * f = fs.first();
         if (f == nullptr) {
             throw cmd_exception("unknown constant ", s);
         }
-        if (f->get_arity() != 0)
+        if (f->get_arity() != 0) {
-            throw cmd_exception("invalid function application, missing arguments ", s);
+            result = array_util(m()).mk_as_array(f);
-        result = m().mk_const(f);
+        }
+        else {
+            result = m().mk_const(f);
+        }
     }
     else {
         func_decl * f = fs.find(m(), num_args, args, range);

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,
+            local l;
-                         num_args,
+            if (m_env.find(fr->m_f, l)) {
-                         expr_stack().c_ptr() + fr->m_expr_spos,
+                push_local(l);
-                         num_indices,
+                t_ref = expr_stack().back();
-                         m_param_stack.c_ptr() + fr->m_param_spos,
+                for (unsigned i = 0; i < num_args; ++i) {
-                         fr->m_as_sort ? sort_stack().back() : nullptr,
+                    expr* arg = expr_stack().get(fr->m_expr_spos + i);
-                         t_ref);
+                    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)

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')
                           ))

src/smt/smt_setup.cpp

@@ -964,6 +964,7 @@ namespace smt {
             setup_seq_str(st);
             setup_card();
             setup_fpa();
+            setup_recfuns();
             return;
         }
 

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) {
+        for (unsigned i = 0; i < m_q_body_expand.size(); ++i) {
-            assert_body_axiom(e);
+            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<expr> 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" <<
+        TRACEFN("macro expansion yields " << mk_pp(rhs,m) << "\n" <<
-                "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;
     }
 

src/smt/theory_recfun.h

@@ -108,7 +108,6 @@ namespace smt {
 
         void reset_queues();
         expr_ref apply_args(recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
-        app_ref apply_pred(recfun::case_pred const & p, ptr_vector<expr> const & args); //<! apply predicate to args
         void assert_macro_axiom(case_expansion & e);
         void assert_case_axioms(case_expansion & e);
         void assert_body_axiom(body_expansion & e);