working with incremental depth

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

src/ast/ast.cpp

@@ -1548,7 +1548,8 @@ void ast_manager::raise_exception(std::string const&  msg) {
 std::ostream& ast_manager::display(std::ostream& out, parameter const& p) {
     switch (p.get_kind()) {
     case parameter::PARAM_AST:
-        return out << ast_ref(p.get_ast(), *this);
+        std::cout << "ast: " << p.get_ast() << "\n";
+        return out << mk_pp(p.get_ast(), *this);
     default:
         return p.display(out);
     }

src/ast/expr_functors.cpp

@@ -69,7 +69,11 @@ void check_pred::visit(expr* e) {
         case AST_QUANTIFIER: {
             quantifier* q = to_quantifier(e);
             expr* arg = q->get_expr();
-            if (m_visited.is_marked(arg)) {
+            if (!m_check_quantifiers) {
+                todo.pop_back();
+                m_visited.mark(e, true);
+            }
+            else if (m_visited.is_marked(arg)) {
                 todo.pop_back();
                 if (m_pred_holds.is_marked(arg)) {
                     m_pred_holds.mark(e, true);

src/ast/expr_functors.h

@@ -53,8 +53,10 @@ class check_pred {
     ast_mark        m_pred_holds;
     ast_mark        m_visited;
     expr_ref_vector m_refs;
+    bool            m_check_quantifiers;
 public:        
-    check_pred(i_expr_pred& p, ast_manager& m) : m_pred(p), m_refs(m) {}
+    check_pred(i_expr_pred& p, ast_manager& m, bool check_quantifiers = true) : 
+        m_pred(p), m_refs(m), m_check_quantifiers(check_quantifiers) {}
         
     bool operator()(expr* e);
 

src/ast/recfun_decl_plugin.cpp

@@ -1,4 +1,6 @@
 /*++
+Copyright (c) 2017 Microsoft Corporation, Simon Cruanes
+
 Module Name:
 
     recfun_decl_plugin.cpp
@@ -68,8 +70,11 @@ namespace recfun {
             ite_find_p(ast_manager & m) : m(m) {}
             virtual bool operator()(expr * e) { return m.is_ite(e); }
         };
+        // ignore ites under quantifiers.
+        // this is redundant as the code
+        // that unfolds ites uses quantifier-free portion.
         ite_find_p p(m);
-        check_pred cp(p, m);
+        check_pred cp(p, m, false);
         return cp(e);
     }
 
@@ -249,7 +254,9 @@ namespace recfun {
                     else if (is_app(e)) {
                         // explore arguments
                         for (expr * arg : *to_app(e)) {
-                            stack.push_back(arg);
+                            if (contains_ite(arg)) {
+                                stack.push_back(arg);
+                            }
                         }
                     } 
                 }
@@ -298,7 +305,7 @@ namespace recfun {
             }
         }
 
-        TRACEFN("done analysing " << get_name());
+        TRACEFN("done analyzing " << get_name());
     }
 
     /*
@@ -405,42 +412,12 @@ namespace recfun {
             return d.get_def();
         }
 
-        func_decl * plugin::mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters, 
-                                             unsigned arity, sort * const * domain, sort * range)
-        {
-            VALIDATE_PARAM(m(), m().is_bool(range) && num_parameters == 1 && parameters[0].is_ast());
-            func_decl_info info(m_family_id, OP_FUN_CASE_PRED, num_parameters, parameters);
-            info.m_private_parameters = true;
-            return m().mk_func_decl(symbol(parameters[0].get_symbol()), arity, domain, range, info);
-        }
-
-        func_decl * plugin::mk_fun_defined_decl(decl_kind k, unsigned num_parameters,
-                                                parameter const * parameters, 
-                                                unsigned arity, sort * const * domain, sort * range)
-        {
-            VALIDATE_PARAM(m(), num_parameters == 1 && parameters[0].is_ast());
-            func_decl_info info(m_family_id, k, num_parameters, parameters);
-            info.m_private_parameters = true;
-            return m().mk_func_decl(symbol(parameters[0].get_symbol()), arity,
-                                    domain, range, info);
-        }
-
         // generic declaration of symbols
         func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                          unsigned arity, sort * const * domain, sort * range)
         {
             UNREACHABLE();
-            // TBD: parameter usage seems inconsistent with other uses.
+            return nullptr;            
-            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:
-                    return mk_fun_defined_decl(k, num_parameters, parameters, arity, domain, range);
-                default:
-                    UNREACHABLE(); 
-                    return nullptr;
-            }
         }
     }
 }

src/ast/recfun_decl_plugin.h

@@ -1,4 +1,6 @@
 /*++
+Copyright (c) 2017 Microsoft Corporation, Simon Cruanes
+
 Module Name:
 
     recfun_decl_plugin.h
@@ -149,19 +151,21 @@ namespace recfun {
             ast_manager & m() { return *m_manager; }
         public:
             plugin();
-            virtual ~plugin() override;
+            ~plugin() override;
-            virtual void finalize() override;
+            void finalize() override;
 
             util & u() const; // build or return util
 
-            virtual bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts
+            bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts
         
-            virtual decl_plugin * mk_fresh() override { return alloc(plugin); }
+            decl_plugin * mk_fresh() override { return alloc(plugin); }
         
-            virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { UNREACHABLE(); return 0; }
+            sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { 
+                UNREACHABLE(); return nullptr; 
+            }
         
-            virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+            func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
-                                             unsigned arity, sort * const * domain, sort * range) override;
+                                     unsigned arity, sort * const * domain, sort * range) override;
             
             promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
             
@@ -170,19 +174,13 @@ namespace recfun {
             def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
 
             bool has_def(const symbol& s) const { return m_defs.contains(s); }
-            bool has_def() const { return !m_defs.empty(); }
+            bool has_defs() const { return !m_defs.empty(); }
             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(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, 
-                                         unsigned arity, sort * const * domain, sort * range);
-            func_decl * mk_fun_defined_decl(decl_kind k,
-                                            unsigned num_parameters, parameter const * parameters, 
-                                            unsigned arity, sort * const * domain, sort * range);
         };
     }
 
@@ -200,7 +198,7 @@ namespace recfun {
 
     public:
         util(ast_manager &m, family_id);
-        virtual ~util();
+        ~util();
 
         ast_manager & m() { return m_manager; }
         th_rewriter & get_th_rewriter() { return m_th_rw; }
@@ -209,7 +207,7 @@ namespace recfun {
         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(); }
+        bool has_defs() const { return m_plugin->has_defs(); }
 
         //<! add a function declaration
         def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);

src/cmd_context/cmd_context.cpp

@@ -797,9 +797,11 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
     if (contains_macro(s, f)) {
         throw cmd_exception("invalid declaration, named expression already defined with this name ", s);
     }
+#if 0
     if (m_builtin_decls.contains(s)) {
         throw cmd_exception("invalid declaration, builtin symbol ", s);
     }
+#endif
     dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
     func_decls & fs = e->get_data().m_value;
     if (!fs.insert(m(), f)) {
@@ -834,9 +836,11 @@ void cmd_context::insert(symbol const & s, psort_decl * p) {
 
 void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
     expr_ref _t(t, m());
+#if 0
     if (m_builtin_decls.contains(s)) {
         throw cmd_exception("invalid macro/named expression, builtin symbol ", s);
     }
+#endif
     if (contains_macro(s, arity, domain)) {
         throw cmd_exception("named expression already defined");
     }
@@ -967,6 +971,15 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
 }
 
 func_decl * cmd_context::find_func_decl(symbol const & s) const {
+    if (contains_macro(s)) {
+        throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
+    }
+    func_decls fs;
+    if (m_func_decls.find(s, fs)) {
+        if (fs.more_than_one())
+            throw cmd_exception("ambiguous function declaration reference, provide full signature to disumbiguate (<symbol> (<sort>*) <sort>) ", s);
+        return fs.first();
+    }
     builtin_decl d;
     if (m_builtin_decls.find(s, d)) {
         try {
@@ -980,15 +993,6 @@ func_decl * cmd_context::find_func_decl(symbol const & s) const {
         }
         throw cmd_exception("invalid function declaration reference, must provide signature for builtin symbol ", s);
     }
-    if (contains_macro(s)) {
-        throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
-    }
-    func_decls fs;
-    if (m_func_decls.find(s, fs)) {
-        if (fs.more_than_one())
-            throw cmd_exception("ambiguous function declaration reference, provide full signature to disumbiguate (<symbol> (<sort>*) <sort>) ", s);
-        return fs.first();
-    }
     throw cmd_exception("invalid function declaration reference, unknown function ", s);
     return nullptr;
 }
@@ -1013,6 +1017,18 @@ static builtin_decl const & peek_builtin_decl(builtin_decl const & first, family
 
 func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                         unsigned arity, sort * const * domain, sort * range) const {
+
+    if (domain && contains_macro(s, arity, domain))
+        throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
+
+    func_decl * f = nullptr;
+    func_decls fs;
+    if (num_indices == 0 && m_func_decls.find(s, fs)) {
+        f = fs.find(arity, domain, range);
+    }
+    if (f) {
+        return f;
+    }
     builtin_decl d;
     if (domain && m_builtin_decls.find(s, d)) {
         family_id fid = d.m_fid;
@@ -1037,21 +1053,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
             throw cmd_exception("invalid function declaration reference, invalid builtin reference ", s);
         return f;
     }
-
+    throw cmd_exception("invalid function declaration reference, unknown function ", s);
-    if (domain && contains_macro(s, arity, domain))
-        throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
-
-    if (num_indices > 0)
-        throw cmd_exception("invalid indexed function declaration reference, unknown builtin function ", s);
-
-    func_decl * f = nullptr;
-    func_decls fs;
-    if (m_func_decls.find(s, fs)) {
-        f = fs.find(arity, domain, range);
-    }
-    if (f == nullptr)
-        throw cmd_exception("invalid function declaration reference, unknown function ", s);
-    return f;
 }
 
 psort_decl * cmd_context::find_psort_decl(symbol const & s) const {
@@ -1088,29 +1090,6 @@ void cmd_context::mk_const(symbol const & s, expr_ref & result) const {
 
 void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range,
                          expr_ref & result) const {
-    builtin_decl d;
-    if (m_builtin_decls.find(s, d)) {
-        family_id fid = d.m_fid;
-        decl_kind k   = d.m_decl;
-        // Hack: if d.m_next != 0, we use the sort of args[0] (if available) to decide which plugin we use.
-        if (d.m_decl != 0 && num_args > 0) {
-            builtin_decl const & d2 = peek_builtin_decl(d, m().get_sort(args[0])->get_family_id());
-            fid = d2.m_fid;
-            k   = d2.m_decl;
-        }
-        if (num_indices == 0) {
-            result = m().mk_app(fid, k, 0, nullptr, num_args, args, range);
-        }
-        else {
-            result = m().mk_app(fid, k, num_indices, indices, num_args, args, range);
-        }
-        if (result.get() == nullptr)
-            throw cmd_exception("invalid builtin application ", s);
-        CHECK_SORT(result.get());
-        return;
-    }
-    if (num_indices > 0)
-        throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s);
     expr* _t;
     if (macros_find(s, num_args, args, _t)) {
         TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n";
@@ -1126,6 +1105,31 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
 
     func_decls fs;
     if (!m_func_decls.find(s, fs)) {
+
+        builtin_decl d;
+        if (m_builtin_decls.find(s, d)) {
+            family_id fid = d.m_fid;
+            decl_kind k   = d.m_decl;
+            // Hack: if d.m_next != 0, we use the sort of args[0] (if available) to decide which plugin we use.
+            if (d.m_decl != 0 && num_args > 0) {
+                builtin_decl const & d2 = peek_builtin_decl(d, m().get_sort(args[0])->get_family_id());
+                fid = d2.m_fid;
+                k   = d2.m_decl;
+            }
+            if (num_indices == 0) {
+                result = m().mk_app(fid, k, 0, nullptr, num_args, args, range);
+            }
+            else {
+                result = m().mk_app(fid, k, num_indices, indices, num_args, args, range);
+        }
+            if (result.get() == nullptr)
+                throw cmd_exception("invalid builtin application ", s);
+            CHECK_SORT(result.get());
+            return;
+        }
+        if (num_indices > 0)
+            throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s);
+        
         if (num_args == 0) {
             throw cmd_exception("unknown constant ", s);
         }

src/smt/theory_recfun.cpp

@@ -34,7 +34,7 @@ namespace smt {
           m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
           m_preds(m),
-          m_max_depth(2),
+          m_max_depth(0),
           m_q_case_expand(), 
           m_q_body_expand()
         {
@@ -50,11 +50,15 @@ namespace smt {
         return alloc(theory_recfun, new_ctx->get_manager());
     }
 
-    void theory_recfun::init_search_eh() {
+    void theory_recfun::init(context* ctx) {
-        smt_params_helper p(ctx().get_params());
+        theory::init(ctx);
+        smt_params_helper p(ctx->get_params());
         m_max_depth = p.recfun_depth();
+        if (m_max_depth < 2) m_max_depth = 2;
     }
 
+    void theory_recfun::init_search_eh() {
+    }
 
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
         TRACEFN(mk_pp(atom, m));
@@ -199,26 +203,22 @@ namespace smt {
      * retrieve depth associated with predicate or expression.
      */
     unsigned theory_recfun::get_depth(expr* e) {
+        SASSERT(u().is_defined(e) || u().is_case_pred(e));
         unsigned d = 0;
         m_pred_depth.find(e, d);
+        TRACEFN("depth " << d << " " << mk_pp(e, m));
         return d;
     }
 
     /**
      * Update depth of subterms of e with respect to d.
      */
-    void theory_recfun::set_depth(unsigned d, expr* e) {
+    void theory_recfun::set_depth_rec(unsigned d, expr* e) {
         struct insert_c {
             theory_recfun& th;
             unsigned m_depth;
             insert_c(theory_recfun& th, unsigned d): th(th), m_depth(d) {}
-            void operator()(app* e) {
+            void operator()(app* e) { th.set_depth(m_depth, e); }
-                if (th.u().is_defined(e) && !th.m_pred_depth.contains(e)) {
-                    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()(var*) {}
         };
@@ -226,6 +226,14 @@ namespace smt {
         for_each_expr(proc, e);
     }
 
+    void theory_recfun::set_depth(unsigned depth, expr* e) {        
+        if ((u().is_defined(e) || u().is_case_pred(e)) && !m_pred_depth.contains(e)) {
+            m_pred_depth.insert(e, depth);
+            m_preds.push_back(e);
+            TRACEFN("depth " << depth << " : " << mk_pp(e, m));
+        }
+    }
+
     /**
      * if `is_true` and `v = C_f_i(t1...tn)`, 
      *    then body-expand i-th case of `f(t1...tn)`
@@ -250,7 +258,7 @@ namespace smt {
         expr_ref new_body(m);
         new_body = subst(e, args.size(), args.c_ptr());
         ctx().get_rewriter()(new_body); // simplify
-        set_depth(depth + 1, new_body);
+        set_depth_rec(depth + 1, new_body);
         return new_body;
     }
         
@@ -312,19 +320,23 @@ namespace smt {
         SASSERT(e.m_def->is_fun_defined());
         // add case-axioms for all case-paths
         auto & vars = e.m_def->get_vars();
+        literal_vector preds;
         for (recfun::case_def const & c : e.m_def->get_cases()) {
             // applied predicate to `args`
             app_ref pred_applied = c.apply_case_predicate(e.m_args);
 
             // cut off cases below max-depth
             unsigned depth = get_depth(e.m_lhs);
+            set_depth(depth, pred_applied);
+            SASSERT(u().owns_app(pred_applied));
+            literal concl = mk_literal(pred_applied);
+            preds.push_back(concl);
+
             if (depth >= m_max_depth) {
                 assert_max_depth_limit(pred_applied);
                 continue;
             }
 
-            SASSERT(u().owns_app(pred_applied));
-            literal concl = mk_literal(pred_applied);
 
             literal_vector guards;
             guards.push_back(concl);
@@ -338,10 +350,11 @@ namespace smt {
             ctx().mk_th_axiom(get_id(), guards);
 
             if (c.is_immediate()) {
-                body_expansion be(e.m_lhs, c, e.m_args);
+                body_expansion be(pred_applied, c, e.m_args);
                 assert_body_axiom(be);
             }
         }
+        ctx().mk_th_axiom(get_id(), preds);
     }
 
     /**
@@ -357,7 +370,7 @@ namespace smt {
         auto & vars = d.get_vars();
         auto & args = e.m_args;
         SASSERT(is_standard_order(vars));
-        unsigned depth = get_depth(e.m_lhs);
+        unsigned depth = get_depth(e.m_pred);
         expr_ref lhs(u().mk_fun_defined(d, args), m);
         expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
 
@@ -388,7 +401,7 @@ namespace smt {
     }
 
     void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
-        if (u().has_def()) {
+        if (u().has_defs()) {
             app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
             TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
             assumptions.push_back(dlimit);

src/smt/theory_recfun.h

@@ -66,20 +66,20 @@ namespace smt {
 
         // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
         struct body_expansion {
-            app*                    m_lhs;
+            app*                    m_pred;
             recfun_case_def const * m_cdef;
             ptr_vector<expr>        m_args;
 
-            body_expansion(recfun_util& u, app * n) : m_lhs(n), m_cdef(0), m_args() {
+            body_expansion(recfun_util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
                 m_cdef = &u.get_case_def(n);
                 m_args.append(n->get_num_args(), n->get_args());
             }
-            body_expansion(app* lhs, recfun_case_def const & d, ptr_vector<expr> & args) : 
+            body_expansion(app* pred, recfun_case_def const & d, ptr_vector<expr> & args) : 
-                m_lhs(lhs), m_cdef(&d), m_args(args) {}
+                m_pred(pred), m_cdef(&d), m_args(args) {}
             body_expansion(body_expansion const & from): 
-                m_lhs(from.m_lhs), m_cdef(from.m_cdef), m_args(from.m_args) {}
+                m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
             body_expansion(body_expansion && from) : 
-                m_lhs(from.m_lhs), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
+                m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
         };
 
         struct pp_body_expansion {
@@ -122,6 +122,7 @@ namespace smt {
         void assert_max_depth_limit(expr* guard);
         unsigned get_depth(expr* e);
         void set_depth(unsigned d, expr* e);
+        void set_depth_rec(unsigned d, expr* e);
         
         literal mk_eq_lit(expr* l, expr* r);
         bool is_standard_order(recfun::vars const& vars) const { 
@@ -148,6 +149,7 @@ namespace smt {
         void new_eq_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 init(context* ctx) override;
 
     public:
         theory_recfun(ast_manager & m);