guard

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

src/smt/theory_recfun.cpp

@@ -19,6 +19,7 @@ Revision History:
 
 #include "util/stats.h"
 #include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
 #include "smt/theory_recfun.h"
 #include "smt/params/smt_params_helper.hpp"
 
@@ -32,7 +33,7 @@ namespace smt {
           m(m),
           m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
-          m_guard_preds(m),
+          m_preds(m),
           m_max_depth(UINT_MAX), 
           m_q_case_expand(), 
           m_q_body_expand()
@@ -111,7 +112,7 @@ namespace smt {
     void theory_recfun::push_scope_eh() {
         TRACEFN("push_scope");
         theory::push_scope_eh();
-        m_guard_preds_lim.push_back(m_guard_preds.size());
+        m_preds_lim.push_back(m_preds.size());
     }
 
     void theory_recfun::pop_scope_eh(unsigned num_scopes) {
@@ -119,14 +120,14 @@ namespace smt {
         theory::pop_scope_eh(num_scopes);
         reset_queues();
         
-        // restore guards
+        // restore depth book-keeping
-        unsigned new_lim = m_guard_preds_lim.size()-num_scopes;
+        unsigned new_lim = m_preds_lim.size()-num_scopes;
-        unsigned start = m_guard_preds_lim[new_lim];
+        unsigned start = m_preds_lim[new_lim];
-        for (unsigned i = start; i < m_guard_preds.size(); ++i) {
+        for (unsigned i = start; i < m_preds.size(); ++i) {
-            m_guards[m_guard_preds.get(i)].pop_back();
+            m_pred_depth.remove(m_preds.get(i));
         }
-        m_guard_preds.resize(start);
+        m_preds.resize(start);
-        m_guard_preds_lim.shrink(new_lim);
+        m_preds_lim.shrink(new_lim);
     }
     
     void theory_recfun::restart_eh() {
@@ -169,24 +170,49 @@ namespace smt {
         m_q_body_expand.clear();
     }
 
-    void theory_recfun::max_depth_limit(ptr_vector<expr> const& guards) {
+    /**
+     * make clause `depth_limit => ~guard`
+     * the guard appears at a depth below the current cutoff.
+     */
+    void theory_recfun::assert_max_depth_limit(expr* guard) {
         TRACEFN("max-depth limit");
         literal_vector c;
-        // make clause `depth_limit => V_{g : guards of non-recursive cases} g`
-
-        // 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");
+        c.push_back(~mk_literal(guard));        
-        TRACE("recfun", ctx().display(tout << c.back() << " " << dlimit << "\n"););
-
-        for (expr * g : guards) {
-            c.push_back(mk_literal(g));
-        }
         TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
         m_q_clauses.push_back(std::move(c));
     }
 
+    /**
+     * retrieve depth associated with predicate or expression.
+     */
+    unsigned theory_recfun::get_depth(expr* e) {
+        unsigned d = 0;
+        m_pred_depth.find(e, d);
+        return d;
+    }
+
+    /**
+     * Update depth of subterms of e with respect to d.
+     */
+    void theory_recfun::set_depth(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) {
+                if ((th.u().is_defined(e) || th.u().is_case_pred(e)) && !th.m_pred_depth.contains(e)) {
+                    th.m_pred_depth.insert(e, m_depth);
+                }
+            }
+            void operator()(quantifier*) {}
+            void operator()(var*) {}
+        };
+        insert_c proc(*this, d);
+        for_each_expr(proc, e);
+    }
+
     /**
      * if `is_true` and `v = C_f_i(t1...tn)`, 
      *    then body-expand i-th case of `f(t1...tn)`
@@ -203,6 +229,7 @@ namespace smt {
 
      // replace `vars` by `args` in `e`
     expr_ref theory_recfun::apply_args(
+        unsigned depth,
         recfun::vars const & vars,
         ptr_vector<expr> const & args,
         expr * e) {
@@ -250,7 +277,8 @@ namespace smt {
         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);
+        unsigned depth = get_depth(e.m_lhs);
+        expr_ref rhs(apply_args(depth, 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" <<
@@ -273,13 +301,21 @@ namespace smt {
         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(pred_applied);
+            if (depth >= get_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);
             for (auto & g : c.get_guards()) {
-                expr_ref ga = apply_args(vars, e.m_args, g);
+                expr_ref ga = apply_args(depth, vars, e.m_args, g);
                 literal guard = mk_literal(ga);
                 guards.push_back(~guard);
                 literal c[2] = {~concl, guard};
@@ -288,18 +324,8 @@ namespace smt {
             ctx().mk_th_axiom(get_id(), guards);
 
             if (c.is_immediate()) {
-                body_expansion be(c, e.m_args);
+                body_expansion be(e.m_lhs, c, e.m_args);
                 assert_body_axiom(be);
-
-                // add to set of local assumptions, for depth-limit purpose
-                
-                // func_decl* d = pred_applied->get_decl();
-                m_guard_preds.push_back(pred_applied);
-                auto& vec = m_guards.insert_if_not_there2(e.m_lhs, ptr_vector<expr>())->get_data().m_value;
-                vec.push_back(pred_applied);
-                if (vec.size() == get_max_depth()) {
-                    max_depth_limit(vec);
-                }
             }
         }
     }
@@ -317,12 +343,13 @@ namespace smt {
         auto & vars = d.get_vars();
         auto & args = e.m_args;
         SASSERT(is_standard_order(vars));
+        unsigned depth = get_depth(e.m_lhs);
         expr_ref lhs(u().mk_fun_defined(d, args), m);
-        expr_ref rhs = apply_args(vars, args, e.m_cdef->get_rhs());
+        expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
 
         literal_vector clause;
         for (auto & g : e.m_cdef->get_guards()) {
-            expr_ref guard = apply_args(vars, args, g);
+            expr_ref guard = apply_args(depth, vars, args, g);
             clause.push_back(~mk_literal(guard));
             if (clause.back() == true_literal) {
                 return;

src/smt/theory_recfun.h

@@ -35,11 +35,11 @@ namespace smt {
 
         // one case-expansion of `f(t1...tn)`
         struct case_expansion {
-            expr *              m_lhs; // the term to expand
+            app *              m_lhs; // the term to expand
             recfun_def *        m_def;
             ptr_vector<expr>    m_args;
-            case_expansion(recfun_util& u, app * n) : m_lhs(n), m_def(0), m_args()
+            case_expansion(recfun_util& u, app * n) : 
-            {
+            m_lhs(n), m_def(nullptr), m_args()  {
                 SASSERT(u.is_defined(n));
                 func_decl * d = n->get_decl();
                 const symbol& name = d->get_name();
@@ -66,16 +66,20 @@ namespace smt {
 
         // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
         struct body_expansion {
+            app*                    m_lhs;
             recfun_case_def const * m_cdef;
             ptr_vector<expr>        m_args;
 
-            body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() {
+            body_expansion(recfun_util& u, app * n) : m_lhs(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(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {}
+            body_expansion(app* lhs, recfun_case_def const & d, ptr_vector<expr> & args) : 
-            body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {}
+                m_lhs(lhs), m_cdef(&d), m_args(args) {}
-            body_expansion(body_expansion && from) : m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
+            body_expansion(body_expansion const & from): 
+                m_lhs(from.m_lhs), 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)) {}
         };
 
         struct pp_body_expansion {
@@ -86,14 +90,16 @@ namespace smt {
 
         friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
         
-        ast_manager&           m;
+        ast_manager&            m;
-        recfun_decl_plugin&    m_plugin;
+        recfun_decl_plugin&     m_plugin;
-        recfun_util&           m_util;
+        recfun_util&            m_util;
-        stats                  m_stats;
+        stats                   m_stats;
-        obj_map<expr, ptr_vector<expr> > m_guards;
+
-        app_ref_vector         m_guard_preds;
+        // book-keeping for depth of predicates
-        unsigned_vector        m_guard_preds_lim;
+        obj_map<expr, unsigned>  m_pred_depth;
-        unsigned               m_max_depth; // for fairness and termination
+        expr_ref_vector          m_preds;
+        unsigned_vector          m_preds_lim;
+        unsigned                 m_max_depth; // for fairness and termination
 
         vector<case_expansion> m_q_case_expand;
         vector<body_expansion> m_q_body_expand;
@@ -107,14 +113,20 @@ namespace smt {
         bool is_case_pred(enode * e) const { return is_case_pred(e->get_owner()); }
 
         void reset_queues();
-        expr_ref apply_args(recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
+        expr_ref apply_args(unsigned depth, recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
         void assert_macro_axiom(case_expansion & e);
         void assert_case_axioms(case_expansion & e);
         void assert_body_axiom(body_expansion & e);
         literal mk_literal(expr* e);
-        void max_depth_limit(ptr_vector<expr> const& guards);
+
+        void assert_max_depth_limit(expr* guard);
+        unsigned get_depth(expr* e);
+        void set_depth(unsigned d, expr* e);
+        
         literal mk_eq_lit(expr* l, expr* r);
-        bool is_standard_order(recfun::vars const& vars) const { return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; }
+        bool is_standard_order(recfun::vars const& vars) const { 
+            return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; 
+        }
     protected:
         void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); }
         void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); }