iterative deepening

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

src/ast/recfun_decl_plugin.cpp

@@ -184,7 +184,8 @@ namespace recfun {
         return res;
     }
 
-    void def::add_case(std::string & name, unsigned n_conditions, expr ** conditions, expr * rhs, bool is_imm) {
+    void def::add_case(std::string & name, unsigned n_conditions, 
+                       expr ** conditions, expr * rhs, bool is_imm) {
         case_def c(m, m_fid, this, name, get_domain(), n_conditions, conditions, rhs);
         c.set_is_immediate(is_imm);
         TRACEFN("add_case " << name << " " << mk_pp(rhs, m)
@@ -202,7 +203,7 @@ namespace recfun {
             TRACEFN("bug: " << m_name << " has cases already");
             UNREACHABLE();
         }
-        SASSERT(n_vars = m_domain.size());
+        SASSERT(n_vars == m_domain.size());
 
         TRACEFN("compute cases " << mk_pp(rhs0, m));
 
@@ -235,7 +236,7 @@ namespace recfun {
         if (m_macro) {
             // constant function or trivial control flow, only one (dummy) case
             name.append("dummy");
-            add_case(name, 0, 0, rhs);
+            add_case(name, 0, nullptr, rhs);
             return;
         }
         

src/smt/smt_context.cpp

@@ -3266,6 +3266,18 @@ namespace smt {
         m_assumptions.reset();
     }
 
+    bool context::should_research(lbool r) {
+        if (r != l_false || m_unsat_core.empty()) { 
+            return false;
+        }
+        for (theory* th : m_theory_set) {
+            if (th->should_research(m_unsat_core)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
     lbool context::mk_unsat_core(lbool r) {        
         if (r != l_false) return r;
         SASSERT(inconsistent());
@@ -3353,7 +3365,7 @@ namespace smt {
         add_theory_assumptions(theory_assumptions);
         if (!theory_assumptions.empty()) {
             TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
-            return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
+            return check(0, nullptr, reset_cancel);
         }
 
         internalize_assertions();
@@ -3407,19 +3419,23 @@ namespace smt {
         }
     }
 
-    lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
+    lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(at_base_level());
         setup_context(false);
         expr_ref_vector asms(m_manager, num_assumptions, assumptions);
-        if (!already_did_theory_assumptions) add_theory_assumptions(asms);                
+        add_theory_assumptions(asms);                
         // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
         TRACE("unsat_core_bug", tout << asms << "\n";);        
         internalize_assertions();
         init_assumptions(asms);
         TRACE("before_search", display(tout););
-        lbool r = search();
+        lbool r;
-        r = mk_unsat_core(r);        
+        do {
+            r = search();
+            r = mk_unsat_core(r);        
+        }
+        while (should_research(r));
         r = check_finalize(r);
         return r;
     }
@@ -3435,8 +3451,12 @@ namespace smt {
         internalize_assertions();
         init_assumptions(asms);
         for (auto const& clause : clauses) init_clause(clause);
-        lbool r = search();   
+        lbool r;
-        r = mk_unsat_core(r);             
+        do {
+            r = search();   
+            r = mk_unsat_core(r);             
+        }
+        while (should_research(r));
         r = check_finalize(r);
         return r;           
     }

src/smt/smt_context.h

@@ -1138,6 +1138,8 @@ namespace smt {
 
         lbool mk_unsat_core(lbool result);
         
+        bool should_research(lbool result);
+
         void validate_unsat_core();
 
         void init_search();
@@ -1524,7 +1526,7 @@ namespace smt {
 
         void pop(unsigned num_scopes);
 
-        lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false);
+        lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true);
 
         lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
 

src/smt/smt_theory.h

@@ -194,6 +194,15 @@ namespace smt {
             return l_false;
         }
 
+        /**
+           \brief This method is called from the smt_context when an unsat core is generated.
+           The theory may tell the solver to perform iterative deepening by invalidating
+           this unsat core and increasing some resource constraints.
+        */
+        virtual bool should_research(expr_ref_vector & unsat_core) {
+            return false;
+        }
+
         /**
            \brief This method is invoked before the search starts.
         */

src/smt/theory_recfun.cpp

@@ -32,12 +32,10 @@ namespace smt {
           m(m),
           m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
-          m_trail(*this),
+          m_guards(m), 
-          m_guards(), 
           m_max_depth(0), 
           m_q_case_expand(), 
-          m_q_body_expand(), 
+          m_q_body_expand()
-          m_q_clauses()
         {
         }
 
@@ -89,11 +87,9 @@ namespace smt {
     void theory_recfun::reset_queues() {
         m_q_case_expand.reset();
         m_q_body_expand.reset();
-        m_q_clauses.reset();
     }
 
     void theory_recfun::reset_eh() {
-        m_trail.reset();
         reset_queues();   
         m_stats.reset();
         theory::reset_eh();
@@ -116,12 +112,10 @@ namespace smt {
     void theory_recfun::push_scope_eh() {
         TRACEFN("push_scope");
         theory::push_scope_eh();
-        m_trail.push_scope();
     }
 
     void theory_recfun::pop_scope_eh(unsigned num_scopes) {
         TRACEFN("pop_scope " << num_scopes);
-        m_trail.pop_scope(num_scopes);
         theory::pop_scope_eh(num_scopes);
         reset_queues();
     }
@@ -179,7 +173,7 @@ namespace smt {
             c.push_back(~ mk_literal(g));
         }
         TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
-        SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict
+       SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict
 
         m_q_clauses.push_back(std::move(c));
     }
@@ -190,26 +184,23 @@ namespace smt {
      */
     void theory_recfun::assign_eh(bool_var v, bool is_true) {
         expr* e = ctx().bool_var2expr(v);
-        if (!is_true || !is_app(e)) return;
+        if (is_true && u().is_case_pred(e)) {
-        app* a = to_app(e);
+            app* a = to_app(e);
-        if (u().is_case_pred(a)) {
+            TRACEFN("assign_case_pred_true " << mk_pp(e, m));
-            TRACEFN("assign_case_pred_true "<< mk_pp(e,m));
             // add to set of local assumptions, for depth-limit purpose
-            SASSERT(!m_guards.contains(e));
+            SASSERT(!m_guards.contains(a));
-            m_guards.insert(e);
+            m_guards.push_back(a);
-            m.inc_ref(e);
+            ctx().push_trail(push_back_vector<context, app_ref_vector>(m_guards));
-            insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m, m_guards, e);
-            m_trail.push(trail_elt);
             
-            if (m_guards.size() > get_max_depth()) {
+            if (m_guards.size() <= get_max_depth()) {
-                // too many body-expansions: depth-limit conflict
-                max_depth_conflict();
-            }
-            else {
                 // body-expand
                 body_expansion b_e(u(), a);
                 push_body_expand(std::move(b_e));
             }
+            else {
+                // too many body-expansions: depth-limit conflict
+                max_depth_conflict();
+            }
         }
     }
 
@@ -238,7 +229,19 @@ namespace smt {
     }
 
     literal theory_recfun::mk_eq_lit(expr* l, expr* r) {
-        literal lit = mk_eq(l, r, false);
+        literal lit;
+        if (m.is_true(r) || m.is_false(r)) {
+            std::swap(l, r);
+        }
+        if (m.is_true(l)) {
+            lit = mk_literal(r);
+        }
+        else if (m.is_false(l)) {
+            lit = ~mk_literal(r);
+        }
+        else {
+            lit = mk_eq(l, r, false);        
+        }
         ctx().mark_as_relevant(lit);
         return lit;
     }
@@ -326,6 +329,21 @@ namespace smt {
     }
     
     final_check_status theory_recfun::final_check_eh() {
+        if (m_guards.size() > get_max_depth()) {
+#if 1
+            return FC_GIVEUP;
+#else
+            for (unsigned i = get_max_depth(); i < m_guards.size(); ++i) {
+                app* a = m_guards.get(i);
+                body_expansion b_e(u(), a);
+                push_body_expand(std::move(b_e));
+            }
+            unsigned new_depth = m_guards.size() + 1;
+            IF_VERBOSE(2, verbose_stream() << "(smt.recfun :new-depth " << new_depth << ")\n");
+            set_max_depth(new_depth);
+            return FC_CONTINUE;
+#endif
+        }
         return FC_DONE;
     }
 
@@ -335,13 +353,16 @@ namespace smt {
         assumptions.push_back(dlimit);
     }
 
-    // if `dlimit` occurs in unsat core, return "unknown"
+    // if `dlimit` occurs in unsat core, return 'true'
-    lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
+    bool theory_recfun::should_research(expr_ref_vector & unsat_core) {
         for (auto & e : unsat_core) {
-            if (u().is_depth_limit(e)) 
+            if (u().is_depth_limit(e)) {
-                return l_undef;
+                unsigned new_depth = (3 * (1 + get_max_depth())) / 2;
+                set_max_depth(new_depth);
+                return true;
+            }
         }
-        return l_false;
+        return false;
     }
 
     void theory_recfun::display(std::ostream & out) const {

src/smt/theory_recfun.h

@@ -72,8 +72,7 @@ namespace smt {
             body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() {
                 SASSERT(u.is_case_pred(n));
                 m_cdef = &u.get_case_def(n->get_name());
-                for (expr * arg : *n) 
+                m_args.append(n->get_num_args(), n->get_args());
-                    m_args.push_back(arg);
             }
             body_expansion(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {}
             body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {}
@@ -88,16 +87,11 @@ namespace smt {
 
         friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
         
-
-        typedef trail_stack<theory_recfun>  th_trail_stack;
-        typedef obj_hashtable<expr> guard_set;
-
         ast_manager&        m;
         recfun_decl_plugin& m_plugin;
         recfun_util&        m_util;
         stats               m_stats;
-        th_trail_stack      m_trail;
+        app_ref_vector      m_guards;  // true case-preds
-        guard_set           m_guards; // true case-preds
         unsigned            m_max_depth; // for fairness and termination
 
         vector<case_expansion>      m_q_case_expand;
@@ -117,8 +111,8 @@ namespace smt {
         void assert_macro_axiom(case_expansion & e);
         void assert_case_axioms(case_expansion & e);
         void assert_body_axiom(body_expansion & e);
-        void max_depth_conflict(void);
         literal mk_literal(expr* e);
+        void max_depth_conflict();
         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; }
     protected:
@@ -137,7 +131,7 @@ namespace smt {
         void restart_eh() override;
         bool can_propagate() override;
         void propagate() override;
-        lbool validate_unsat_core(expr_ref_vector &) override;
+        bool should_research(expr_ref_vector &) override;
 
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
@@ -152,6 +146,7 @@ namespace smt {
         virtual void collect_statistics(::statistics & st) const override;
         unsigned get_max_depth() const { return m_max_depth; }
         void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
+        void inc_max_depth() { ++m_max_depth; }
     };
 }