fix #5016

src/sat/smt/dt_solver.cpp

@@ -222,6 +222,8 @@ namespace dt {
         else if (is_update_field(n)) {
             assert_update_field_axioms(n);
         }
+        else if (is_recognizer(n))
+            ;
         else {
             sort* s = n->get_expr()->get_sort();
             if (dt.get_datatype_num_constructors(s) == 1)
@@ -251,7 +253,9 @@ namespace dt {
 
         TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
 
+
         enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr);
+                               
         if (recognizer == nullptr)
             r = dt.get_constructor_is(non_rec_c);
         else if (ctx.value(recognizer) != l_false)
@@ -263,13 +267,15 @@ namespace dt {
             unsigned idx = 0;
             ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(srt);
             for (enode* curr : d->m_recognizers) {
+
                 if (curr == nullptr) {
                     // found empty slot...
                     r = dt.get_constructor_is(constructors[idx]);
                     break;
                 }
-                else if (ctx.value(curr) != l_false)
+                else if (ctx.value(curr) != l_false) {
                     return;
+                }
                 ++idx;
             }
             if (r == nullptr)
@@ -342,6 +348,7 @@ namespace dt {
     }
 
     void solver::add_recognizer(theory_var v, enode* recognizer) {
+        TRACE("dt", tout << "add recognizer " << v << " " << mk_pp(recognizer->get_expr(), m) << "\n";);
         SASSERT(is_recognizer(recognizer));
         v = m_find.find(v);
         var_data* d = m_var_data[v];
@@ -596,7 +603,7 @@ namespace dt {
        a3 = cons(v3, a1)
     */
     bool solver::occurs_check(enode* n) {
-        TRACE("dt", tout << "occurs check: " << ctx.bpp(n) << "\n";);
+        TRACE("dt_verbose", tout << "occurs check: " << ctx.bpp(n) << "\n";);
         m_stats.m_occurs_check++;
 
         bool res = false;
@@ -611,7 +618,7 @@ namespace dt {
             if (oc_cycle_free(app))
                 continue;
 
-            TRACE("dt", tout << "occurs check loop: " << ctx.bpp(app) << (op == ENTER ? " enter" : " exit") << "\n";);
+            TRACE("dt_verbose", tout << "occurs check loop: " << ctx.bpp(app) << (op == ENTER ? " enter" : " exit") << "\n";);
 
             switch (op) {
             case ENTER:
@@ -627,6 +634,7 @@ namespace dt {
         if (res) {
             clear_mark();
             ctx.set_conflict(euf::th_propagation::mk(*this, m_used_eqs));
+            TRACE("dt", tout << "occurs check conflict: " << ctx.bpp(n) << "\n";);
         }
         return res;
     }
@@ -741,17 +749,21 @@ namespace dt {
                 }
             }
             mk_var(n);
+            
         }
         else if (is_recognizer(term)) {
+            mk_var(n);
             enode* arg = n->get_arg(0);
             theory_var v = mk_var(arg);
-            add_recognizer(v, n);           
+            add_recognizer(v, n);   
+            
         }
         else {
             SASSERT(is_accessor(term));
             SASSERT(n->num_args() == 1);
             mk_var(n->get_arg(0));
         }
+       
         return true;
     }
 

src/sat/smt/euf_solver.cpp

@@ -27,9 +27,16 @@ Author:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/fpa_solver.h"
 #include "sat/smt/dt_solver.h"
+#include "sat/smt/recfun_solver.h"
 
 namespace euf {
 
+    std::ostream& clause_pp::display(std::ostream& out) const {
+        for (auto lit : lits)
+            out << s.literal2expr(lit) << " ";
+        return out;
+    }
+
     solver::solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p) :
         extension(symbol("euf"), m.mk_family_id("euf")),
         m(m),
@@ -103,6 +110,7 @@ namespace euf {
         fpa_util fpa(m);
         arith_util arith(m);
         datatype_util dt(m);
+        recfun::util rf(m);
         if (pb.get_family_id() == fid)
             ext = alloc(sat::ba_solver, *this, fid);
         else if (bvu.get_family_id() == fid)
@@ -115,6 +123,8 @@ namespace euf {
             ext = alloc(arith::solver, *this, fid);
         else if (dt.get_family_id() == fid)
             ext = alloc(dt::solver, *this, fid);
+        else if (rf.get_family_id() == fid)
+            ext = alloc(recfun::solver, *this);
         
         if (ext) 
             add_solver(ext);        
@@ -430,6 +440,7 @@ namespace euf {
         if (!init_relevancy())
             give_up = true;
 
+
         for (auto* e : m_solvers) {
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
@@ -558,6 +569,26 @@ namespace euf {
         if (m_ackerman)
             m_ackerman->propagate();
     }
+    
+    bool solver::should_research(sat::literal_vector const& core) {
+        bool result = false;
+        for (auto* e : m_solvers)
+            if (e->should_research(core))
+                result = true;
+        return result;
+    }
+
+    void solver::add_assumptions() {
+        for (auto* e : m_solvers)
+            e->add_assumptions();
+    }
+
+    bool solver::tracking_assumptions() {
+        for (auto* e : m_solvers)
+            if (e->tracking_assumptions())
+                return true;
+        return false;
+    }
 
     void solver::clauses_modifed() {
         for (auto* e : m_solvers)

src/sat/smt/euf_solver.h

@@ -51,6 +51,14 @@ namespace euf {
         size_t to_index() const { return sat::constraint_base::mem2base(this); }
     };
 
+    class clause_pp {
+        solver& s;
+        sat::literal_vector const& lits;
+    public:
+        clause_pp(solver& s, sat::literal_vector const& lits):s(s), lits(lits) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
     class solver : public sat::extension, public th_internalizer, public th_decompile {
         typedef top_sort<euf::enode> deps_t;
         friend class ackerman;
@@ -266,6 +274,9 @@ namespace euf {
         bool is_external(bool_var v) override;
         bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override;
+        bool should_research(sat::literal_vector const& core) override;
+        void add_assumptions() override;
+        bool tracking_assumptions() override;
 
         void propagate(literal lit, ext_justification_idx idx);
         bool propagate(enode* a, enode* b, ext_justification_idx idx);
@@ -297,6 +308,7 @@ namespace euf {
         std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
         euf::egraph::b_pp bpp(enode* n) { return m_egraph.bpp(n); }
+        clause_pp pp(literal_vector const& lits) { return clause_pp(*this, lits); }
         void collect_statistics(statistics& st) const override;
         extension* copy(sat::solver* s) override;
         enode* copy(solver& dst_ctx, enode* src_n);
@@ -396,8 +408,14 @@ namespace euf {
 
 
     };
+
+    inline std::ostream& operator<<(std::ostream& out, clause_pp const& p) {
+        return p.display(out);
+    }
+
 };
 
 inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) {
     return s.display(out);
 }
+

src/sat/smt/recfun_solver.cpp

@@ -66,6 +66,7 @@ namespace recfun {
      */
     void solver::assert_macro_axiom(case_expansion & e) {
         m_stats.m_macro_expansions++;
+        TRACEFN("case expansion " << e);
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
         auto lhs = e.m_lhs;
@@ -84,6 +85,14 @@ namespace recfun {
      * also body-expand paths that do not depend on any defined fun
      */
     void solver::assert_case_axioms(case_expansion & e) {
+        if (e.m_def->is_fun_macro()) {
+            assert_macro_axiom(e);
+            return;
+        }
+
+        ++m_stats.m_case_expansions;
+        TRACEFN("assert_case_axioms " << e
+                << " with " << e.m_def->get_cases().size() << " cases");
         SASSERT(e.m_def->is_fun_defined());
         // add case-axioms for all case-paths
         // assert this was not defined before.
@@ -106,36 +115,41 @@ namespace recfun {
                 disable_guard(pred_applied, guards);
                 continue;
             }
-            activate_guard(pred_applied, guards);
+            assert_guard(pred_applied, guards);
         }
         add_clause(preds);
     }
     
-    void solver::activate_guard(expr* pred_applied, expr_ref_vector const& guards) {
+    void solver::assert_guard(expr* pred_applied, expr_ref_vector const& guards) {
         sat::literal_vector lguards;
         for (expr* ga : guards) 
             lguards.push_back(mk_literal(ga));
         add_equiv_and(mk_literal(pred_applied), lguards);
     }
 
+    void solver::block_core(expr_ref_vector const& core) {
+        sat::literal_vector clause;
+        for (expr* e : core)
+            clause.push_back(~mk_literal(e));
+        add_clause(clause);
+    }
+
     /**
      * make clause `depth_limit => ~guard`
      * the guard appears at a depth below the current cutoff.
      */
     void solver::disable_guard(expr* guard, expr_ref_vector const& guards) {
-        expr_ref nguard(m.mk_not(guard), m);
-        if (is_disabled_guard(nguard)) 
-            return;
-        SASSERT(!is_enabled_guard(nguard));
-        sat::literal_vector c;
+        SASSERT(!is_enabled_guard(guard));
         app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
-        c.push_back(~mk_literal(dlimit));
-        c.push_back(~mk_literal(guard)); 
-        m_disabled_guards.push_back(nguard);
-        SASSERT(!m_guard2pending.contains(nguard));
-        m_guard2pending.insert(nguard, alloc(expr_ref_vector, guards));
-        TRACEFN("add clause\n" << c);
-        m_propagation_queue.push_back(alloc(propagation_item, c));
+        expr_ref_vector core(m);
+        core.push_back(dlimit);
+        core.push_back(guard);
+        if (!m_guard2pending.contains(guard)) {
+            m_disabled_guards.push_back(guard);
+            m_guard2pending.insert(guard, alloc(expr_ref_vector, guards));
+        }
+        TRACEFN("add clause\n" << core);
+        push_core(core);
     }
 
     /**
@@ -147,6 +161,7 @@ namespace recfun {
      *
      */
     void solver::assert_body_axiom(body_expansion & e) {
+        ++m_stats.m_body_expansions;
         recfun::def & d = *e.m_cdef->get_def();
         auto & vars = d.get_vars();
         auto & args = e.m_args;
@@ -184,11 +199,6 @@ namespace recfun {
         return out << "disabled guards:\n" << m_disabled_guards << "\n";
     }
 
-    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
-        UNREACHABLE();
-        return out;
-    }
-
     void solver::collect_statistics(statistics& st) const {
         st.update("recfun macro expansion", m_stats.m_macro_expansions);
         st.update("recfun case expansion", m_stats.m_case_expansions);
@@ -196,53 +206,35 @@ namespace recfun {
     }
 
     euf::th_solver* solver::clone(euf::solver& ctx) {
-        return nullptr;
+        return alloc(solver, ctx);
     }
 
     bool solver::unit_propagate() {
+        force_push();
         if (m_qhead == m_propagation_queue.size())
             return false;
         ctx.push(value_trail<unsigned>(m_qhead));
         for (; m_qhead < m_propagation_queue.size() && !s().inconsistent(); ++m_qhead) {
             auto& p = *m_propagation_queue[m_qhead];
-            if (p.is_guard()) {
-                expr* ng = nullptr;
-                VERIFY(m.is_not(p.m_guard, ng));
-                activate_guard(ng, *m_guard2pending[p.m_guard]);
-            }
-            else if (p.is_clause()) {
-                add_clause(p.m_clause);
-            }
-            else if (p.is_case()) {
-                recfun::case_expansion& e = *p.m_case;
-                if (e.m_def->is_fun_macro()) 
-                    assert_macro_axiom(e);
-                else 
-                    assert_case_axioms(e);                
-                ++m_stats.m_case_expansions;
-            } 
-            else {
-                SASSERT(p.is_body());
-                assert_body_axiom(*p.m_body);
-                ++m_stats.m_body_expansions;
-            }                
+            if (p.is_guard()) 
+                assert_guard(p.guard(), *m_guard2pending[p.guard()]);
+            else if (p.is_core()) 
+                block_core(p.core());
+            else if (p.is_case()) 
+                assert_case_axioms(p.case_ex());
+            else 
+                assert_body_axiom(p.body());
         }
         return true;
     }
 
-    void solver::push_body_expand(expr* e) {
-        auto* b = alloc(body_expansion, u(), to_app(e));
-        m_propagation_queue.push_back(alloc(propagation_item, b));
-        ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue));
-    }
-
-    void solver::push_case_expand(expr* e) {
-        auto* c = alloc(case_expansion, u(), to_app(e));
-        m_propagation_queue.push_back(alloc(propagation_item, c));
+    void solver::push(propagation_item* p) {
+        m_propagation_queue.push_back(p);         
         ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue));        
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        force_push();
         SASSERT(m.is_bool(e));
         if (!visit_rec(m, e, sign, root, redundant)) {
             TRACE("array", tout << mk_pp(e, m) << "\n";);
@@ -255,6 +247,7 @@ namespace recfun {
     }
 
     void solver::internalize(expr* e, bool redundant) {
+        force_push();
         visit_rec(m, e, false, false, redundant);
     }
 
@@ -268,8 +261,6 @@ namespace recfun {
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
             ctx.internalize(e, m_is_redundant);
-            euf::enode* n = expr2enode(e);
-            // TODO ensure_var(n);
             return true;
         }
         m_stack.push_back(sat::eframe(e));
@@ -284,35 +275,57 @@ namespace recfun {
             n = mk_enode(e, false);
         SASSERT(!n->is_attached_to(get_id()));
         mk_var(n);
-#if 0
-        for (auto* arg : euf::enode_args(n))
-            ensure_var(arg);  
-        switch (a->get_decl_kind()) {
-        default:
-            UNREACHABLE();
-            break;            
-        }
-#endif
         if (u().is_defined(e) && u().has_defs()) 
             push_case_expand(e);
-
         return true;
     }
 
-
-
-    euf::theory_var solver::mk_var(euf::enode* n) {
-        return euf::null_theory_var;
-    }
-
-    void solver::init_search() {
-
+    void solver::add_assumptions() {
+        if (u().has_defs() || m_disabled_guards.empty()) {
+            app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
+            TRACEFN("add_theory_assumption " << dlimit);
+            s().assign_scoped(mk_literal(dlimit));
+            for (auto g : m_disabled_guards)
+                s().assign_scoped(~mk_literal(g));
+        }
     }
     
-    void solver::finalize_model(model& mdl) {
-        
+    bool solver::should_research(sat::literal_vector const& core) {
+        bool found = false;
+        unsigned min_gen = UINT_MAX;
+        expr* to_delete = nullptr;
+        unsigned n = 0;
+        for (sat::literal lit : core) {
+            expr* e = ctx.bool_var2expr(lit.var());
+            if (lit.sign() && is_disabled_guard(e)) {
+                found = true;
+                unsigned gen = ctx.get_max_generation(e);
+                if (gen < min_gen) 
+                    n = 0;
+
+                if (gen <= min_gen && s().rand()() % (++n) == 0) {
+                    to_delete = e;
+                    min_gen = gen;
+                }
+            }
+            else if (u().is_num_rounds(e)) 
+                found = true;
+        }
+        if (found) {
+            ++m_num_rounds;
+            if (to_delete) {
+                m_disabled_guards.erase(to_delete);
+                m_enabled_guards.push_back(to_delete);
+                push_guard(to_delete);
+                IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n");
+            }
+            else {
+                IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n");
+            }
+            for (expr* g : m_enabled_guards)
+                push_guard(g);
+        }
+        return found;
     }
-
-
     
 }

src/sat/smt/recfun_solver.h

@@ -49,44 +49,16 @@ namespace recfun {
         unsigned_vector          m_preds_lim;
         unsigned                 m_num_rounds { 0 };
 
-        struct propagation_item {
-            case_expansion*            m_case { nullptr };
-            body_expansion*            m_body { nullptr };
-            sat::literal_vector        m_clause;
-            expr*                      m_guard { nullptr };
-
-            ~propagation_item() {
-                dealloc(m_case);
-                dealloc(m_body);
-            }
-
-            propagation_item(expr* guard):
-                m_guard(guard) 
-            {}
-
-            propagation_item(sat::literal_vector const& clause):
-                m_clause(clause)
-            {}
-
-            propagation_item(body_expansion* b):
-                m_body(b)
-            {}
-            propagation_item(case_expansion* c):
-                m_case(c)
-            {}
-
-            bool is_guard() const { return m_guard != nullptr; }
-            bool is_clause() const { return !m_clause.empty(); }
-            bool is_case() const { return m_case != nullptr; }
-            bool is_body() const { return m_body != nullptr; }            
-        };
         scoped_ptr_vector<propagation_item> m_propagation_queue;
         unsigned                            m_qhead { 0 };
 
-        void push_body_expand(expr* e);
-        void push_case_expand(expr* e);
+        void push_body_expand(expr* e) { push(alloc(propagation_item, alloc(body_expansion, u(), to_app(e)))); }
+        void push_case_expand(expr* e) { push(alloc(propagation_item, alloc(case_expansion, u(), to_app(e)))); }
+        void push_guard(expr* e) { push(alloc(propagation_item, e)); }
+        void push_core(expr_ref_vector const& core) { push(alloc(propagation_item, core)); }
+        void push(propagation_item* p);
 
-        bool is_enabled_guard(expr* guard) { expr_ref ng(m.mk_not(guard), m); return m_enabled_guards.contains(ng); }
+        bool is_enabled_guard(expr* guard) { return m_enabled_guards.contains(guard); }
         bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); }
 
         recfun::util & u() const { return m_util; }
@@ -96,20 +68,15 @@ namespace recfun {
         bool is_defined(euf::enode * e) const { return is_defined(e->get_expr()); }
         bool is_case_pred(euf::enode * e) const { return is_case_pred(e->get_expr()); }
 
-        void activate_guard(expr* guard, expr_ref_vector const& guards);
 
-        expr_ref apply_args(vars const & vars, expr_ref_vector const & args, expr * e); //!< substitute variables by args
+        expr_ref apply_args(vars const & vars, expr_ref_vector const & args, expr * e); 
         void assert_macro_axiom(case_expansion & e);
         void assert_case_axioms(case_expansion & e);
         void assert_body_axiom(body_expansion & e);
-
-        void add_induction_lemmas(unsigned depth);
+        void assert_guard(expr* guard, expr_ref_vector const& guards);
+        void block_core(expr_ref_vector const& core);
         void disable_guard(expr* guard, expr_ref_vector const& guards);
-        unsigned get_depth(expr* e);
-        void set_depth(unsigned d, expr* e);
-        void set_depth_rec(unsigned d, expr* e);
         
-        sat::literal mk_eq_lit(expr* l, expr* r);
         bool is_standard_order(recfun::vars const& vars) const { 
             return vars.empty() || vars[vars.size()-1]->get_idx() == 0;
         }
@@ -130,15 +97,16 @@ namespace recfun {
         sat::check_result check() override;
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return display_constraint(out, idx); }
-        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out; }
         void collect_statistics(statistics& st) const override;
         euf::th_solver* clone(euf::solver& ctx) override;
         bool unit_propagate() override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
-        euf::theory_var mk_var(euf::enode* n) override;
-        void init_search() override;
-        void finalize_model(model& mdl) override;
         bool is_shared(euf::theory_var v) const override { return true; }
+        void init_search() override {}
+        bool should_research(sat::literal_vector const& core) override;
+        void add_assumptions() override;
+        bool tracking_assumptions() override { return true; }
     };
 }