na

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

src/ast/recfun_decl_plugin.cpp

@@ -404,6 +404,10 @@ namespace recfun {
             }
         }
 
+        bool plugin::has_defs() const {
+            return !m_case_defs.empty();            
+        }
+
         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));

src/ast/recfun_decl_plugin.h

@@ -174,7 +174,7 @@ 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_defs() const { return !m_defs.empty(); }
+            bool has_defs() const;
             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]); }
@@ -207,6 +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; }
 
+        //<! don't use native theory if recursive function declarations are not populated with defs
         bool has_defs() const { return m_plugin->has_defs(); }
 
         //<! add a function declaration

src/cmd_context/cmd_context.cpp

@@ -909,7 +909,7 @@ recfun_decl_plugin * cmd_context::get_recfun_plugin() {
 }
 
 
-recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) {
+recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) {        
     SASSERT(logic_has_recfun());
     recfun_decl_plugin* p = get_recfun_plugin();
     recfun::promise_def def = p->mk_def(name, arity, domain, range);
@@ -950,7 +950,6 @@ void cmd_context::insert_rec_fun_as_axiom(func_decl *f, expr_ref_vector const& b
 
 
 void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* rhs) {
-    TRACE("recfun", tout<< "define recfun " << f->get_name()  << " = " << mk_pp(rhs, m()) << "\n";);
 
     if (gparams::get_value("smt.recfun.native") != "true") {
         // just use an axiom
@@ -958,6 +957,8 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
         return;
     }
 
+    TRACE("recfun", tout<< "define recfun " << f->get_name()  << " = " << mk_pp(rhs, m()) << "\n";);
+
     recfun_decl_plugin* p = get_recfun_plugin();
 
     var_ref_vector vars(m());

src/smt/smt_context.cpp

@@ -1773,7 +1773,7 @@ namespace smt {
 
     void context::set_conflict(const b_justification & js, literal not_l) {
         if (!inconsistent()) {
-            TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
+            TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); );
             m_conflict = js;
             m_not_l    = not_l;
         }

src/smt/theory_recfun.cpp

@@ -62,6 +62,9 @@ namespace smt {
 
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
         TRACEFN(mk_pp(atom, m));
+        if (!u().has_defs()) {
+            return false;
+        }
         for (expr * arg : *atom) {
             ctx().internalize(arg, false);
         }
@@ -76,6 +79,9 @@ namespace smt {
     }
 
     bool theory_recfun::internalize_term(app * term) {
+        if (!u().has_defs()) {
+            return false;
+        }
         for (expr* e : *term) {
             ctx().internalize(e, false);
         }
@@ -111,26 +117,26 @@ namespace smt {
      */
     void theory_recfun::relevant_eh(app * n) {
         SASSERT(ctx().relevancy());
-        if (u().is_defined(n)) {
+        if (u().is_defined(n) && u().has_defs()) {
             TRACEFN("relevant_eh: (defined) " <<  mk_pp(n, m));        
             push_case_expand(alloc(case_expansion, u(), n));
         }
     }
 
     void theory_recfun::push_scope_eh() {
-        TRACEFN("push_scope");
         theory::push_scope_eh();
         m_preds_lim.push_back(m_preds.size());
     }
 
     void theory_recfun::pop_scope_eh(unsigned num_scopes) {
-        TRACEFN("pop_scope " << num_scopes);
         theory::pop_scope_eh(num_scopes);
         reset_queues();
         
         // restore depth book-keeping
         unsigned new_lim = m_preds_lim.size()-num_scopes;
 #if 0
+        // depth tracking of recursive unfolding is 
+        // turned off when enabling this code:
         unsigned start = m_preds_lim[new_lim];
         for (unsigned i = start; i < m_preds.size(); ++i) {
             m_pred_depth.remove(m_preds.get(i));
@@ -337,7 +343,6 @@ namespace smt {
                 continue;
             }
 
-
             literal_vector guards;
             guards.push_back(concl);
             for (auto & g : c.get_guards()) {
@@ -354,6 +359,8 @@ namespace smt {
                 assert_body_axiom(be);
             }
         }
+        // the disjunction of branches is asserted
+        // to close the available cases. 
         ctx().mk_th_axiom(get_id(), preds);
     }