working on relevancy=3

src/ast/euf/euf_egraph.cpp

@@ -767,6 +767,8 @@ namespace euf {
     }
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
+        if (!n->is_relevant())
+            out << "n";
         out << "#" << n->get_expr_id() << " := ";
         expr* f = n->get_expr();
         if (is_app(f))

src/sat/smt/arith_solver.cpp

@@ -953,6 +953,7 @@ namespace arith {
             if (n1->get_root() == n2->get_root())
                 continue;
             literal eq = eq_internalize(n1, n2);
+            ctx.mark_relevant(eq);
             if (s().value(eq) != l_true)
                 return true;
         }

src/sat/smt/array_axioms.cpp

@@ -57,8 +57,6 @@ namespace array {
 
     bool solver::assert_axiom(unsigned idx) {
         axiom_record& r = m_axiom_trail[idx];
-        if (!is_relevant(r))
-            return false;
         switch (r.m_kind) {
         case axiom_record::kind_t::is_store:
             return assert_store_axiom(to_app(r.n->get_expr()));
@@ -92,29 +90,6 @@ namespace array {
             return false;                
     }
 
-
-    bool solver::is_relevant(axiom_record const& r) const {
-        return true;
-#if 0
-        // relevancy propagation is currently incomplete on terms
-
-        expr* child = r.n->get_expr();
-        switch (r.m_kind) {
-        case axiom_record::kind_t::is_select: {
-            app* select = r.select->get_app();
-            for (unsigned i = 1; i < select->get_num_args(); ++i)
-                if (!ctx.is_relevant(select->get_arg(i)))
-                    return false;
-            return ctx.is_relevant(child);            
-        }
-        case axiom_record::kind_t::is_default:
-            return ctx.is_relevant(child);            
-        default:
-            return true;
-        }
-#endif
-    }
-
     bool solver::assert_select(unsigned idx, axiom_record& r) {
         expr* child = r.n->get_expr();
         app* select = r.select->get_app();
@@ -215,10 +190,17 @@ namespace array {
             return new_prop;
         
         sat::literal sel_eq = sat::null_literal;
+        auto ensure_relevant = [&](sat::literal lit) {
+            if (ctx.is_relevant(lit))
+                return;
+            new_prop = true;
+            ctx.mark_relevant(lit);            
+        };
         auto init_sel_eq = [&]() {
             if (sel_eq != sat::null_literal) 
                 return true;
             sel_eq = mk_literal(sel_eq_e);
+            ensure_relevant(sel_eq);
             return s().value(sel_eq) != l_true;
         };
 
@@ -235,6 +217,7 @@ namespace array {
                 break;
             }
             sat::literal idx_eq = eq_internalize(idx1, idx2);
+            ensure_relevant(idx_eq);
             if (s().value(idx_eq) == l_true)
                 continue;
             if (s().value(idx_eq) == l_undef)
@@ -598,13 +581,12 @@ namespace array {
                 expr* e2 = var2expr(v2);
                 if (e1->get_sort() != e2->get_sort())
                     continue;
-                if (must_have_different_model_values(v1, v2)) {
+                if (must_have_different_model_values(v1, v2)) 
-                    continue;
+                    continue;                
-                }
+                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) 
-                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) {
+                    continue;                
-                    continue;
-                }
                 sat::literal lit = eq_internalize(e1, e2);
+                ctx.mark_relevant(lit);
                 if (s().value(lit) == l_undef) 
                     prop = true;
             }
@@ -616,8 +598,7 @@ namespace array {
         ptr_buffer<euf::enode> to_unmark;
         unsigned num_vars = get_num_vars();
         for (unsigned i = 0; i < num_vars; i++) {
-            euf::enode * n = var2enode(i);
+            euf::enode * n = var2enode(i);            
-            
             if (!is_array(n)) 
                 continue;
             if (!ctx.is_relevant(n))

src/sat/smt/array_internalize.cpp

@@ -58,6 +58,7 @@ namespace array {
     }
 
     void solver::internalize_store(euf::enode* n) {
+        //std::cout << "store th-var " << n->get_th_var(get_id()) << "\n";
         add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);   
         push_axiom(store_axiom(n));
         add_lambda(n->get_th_var(get_id()), n);
@@ -71,7 +72,7 @@ namespace array {
         }
         push_axiom(default_axiom(n));
         add_lambda(n->get_th_var(get_id()), n);
-        SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
+        //SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
     }
 
     void solver::internalize_lambda(euf::enode* n) {

src/sat/smt/array_solver.h

@@ -157,7 +157,6 @@ namespace array {
         bool assert_axiom(unsigned idx);
         bool assert_select(unsigned idx, axiom_record & r);
         bool assert_default(axiom_record & r);
-        bool is_relevant(axiom_record const& r) const;
         void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); }
         bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); }
         bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); }

src/sat/smt/bv_delay_internalize.cpp

@@ -250,7 +250,7 @@ namespace bv {
             return;
         expr_ref tmp = literal2expr(bits.back());
         for (unsigned i = bits.size() - 1; i-- > 0; ) {
-            auto b = bits[i];
+            sat::literal b = bits[i];
             tmp = m.mk_or(literal2expr(b), tmp);
             xs.push_back(tmp);
         }

src/sat/smt/euf_internalize.cpp

@@ -248,7 +248,7 @@ namespace euf {
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
             s().mk_clause(1, &lit, st);
-            add_root(1, &lit);
+            add_root(lit);
         }
     }
 
@@ -351,7 +351,7 @@ namespace euf {
         // contains a parent application.
         
         family_id th_id = m.get_basic_family_id();
-        for (auto p : euf::enode_th_vars(n)) {
+        for (auto const& p : euf::enode_th_vars(n)) {
             family_id id = p.get_id();
             if (m.get_basic_family_id() != id) {
                 if (th_id != m.get_basic_family_id())

src/sat/smt/euf_model.cpp

@@ -271,6 +271,8 @@ namespace euf {
 
     void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
         out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
+        s().display(out);
+        return;
         euf::enode_vector nodes;
         nodes.push_back(n);
         for (unsigned i = 0; i < nodes.size(); ++i) {
@@ -289,7 +291,6 @@ namespace euf {
         for (euf::enode* r : nodes)
             r->unmark1();
         out << mdl << "\n";
-        s().display(out);
     }
 
     void solver::validate_model(model& mdl) {
@@ -322,6 +323,8 @@ namespace euf {
             IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
             CTRACE("euf", first, display_validation_failure(tout, mdl, n););
             (void)first;
+            first = false;
+            return;
             exit(1);
             first = false;
         }        

src/sat/smt/euf_relevancy.cpp

@@ -22,7 +22,7 @@ Author:
 
 namespace euf {
 
-    void solver::add_auto_relevant(sat::literal lit) {
+    void solver::mark_relevant(sat::literal lit) {
         if (m_relevancy.enabled()) {
             m_relevancy.mark_relevant(lit);
             return;

src/sat/smt/euf_solver.cpp

@@ -193,7 +193,7 @@ namespace euf {
     }
 
     void solver::propagate(literal lit, ext_justification_idx idx) {
-        add_auto_relevant(lit);
+        mark_relevant(lit);
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 

src/sat/smt/euf_solver.h

@@ -385,7 +385,6 @@ namespace euf {
         void add_root(unsigned n, sat::literal const* lits);
         void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
         void add_root(sat::literal lit) { add_root(1, &lit); }
-        void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
         void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
         void add_aux(unsigned n, sat::literal const* lits);
         void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
@@ -394,7 +393,8 @@ namespace euf {
         void track_relevancy(sat::bool_var v);
         bool is_relevant(enode* n) const;
         bool is_relevant(bool_var v) const;
-        void add_auto_relevant(sat::literal lit);
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
+        void mark_relevant(sat::literal lit);
         void pop_relevant(unsigned n);
         void push_relevant();
         void relevant_eh(euf::enode* n);

src/sat/smt/pb_solver.cpp

@@ -2006,7 +2006,7 @@ namespace pb {
             s().pop_to_base_level();
         if (s().inconsistent())
             return;
-        unsigned trail_sz, count = 0;
+        unsigned trail_sz = 0, count = 0;
         do {
             trail_sz = s().init_trail_size();
             m_simplify_change = false;

src/sat/smt/recfun_solver.cpp

@@ -68,8 +68,8 @@ namespace recfun {
         TRACEFN("case expansion " << e);
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
-        auto lhs = e.m_lhs;
+        app_ref lhs = e.m_lhs;
-        auto rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
+        expr_ref rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
         unsigned generation = std::max(ctx.get_max_generation(lhs), ctx.get_max_generation(rhs));
         euf::solver::scoped_generation _sgen(ctx, generation + 1);
         auto eq = eq_internalize(lhs, rhs);

src/sat/smt/smt_relevant.cpp

@@ -30,9 +30,17 @@ namespace smt {
     }
 
     void relevancy::relevant_eh(sat::literal lit) {
-        SASSERT(ctx.s().value(lit) == l_true);
         SASSERT(is_relevant(lit));
-        ctx.asserted(lit);
+        switch (ctx.s().value(lit)) {
+        case l_true:
+            ctx.asserted(lit);
+            break;
+        case l_false:
+            ctx.asserted(~lit);
+            break;
+        default:
+            break;
+        }
     }
     
     void relevancy::pop(unsigned n) {
@@ -53,6 +61,9 @@ namespace smt {
                 m_relevant_var_ids[idx] = false;
                 m_queue.pop_back();
                 break;
+            case update::relevant_node:
+                m_queue.pop_back();
+                break;
             case update::add_clause: {
                 sat::clause* c = m_clauses.back();
                 for (sat::literal lit : *c) {
@@ -182,14 +193,7 @@ namespace smt {
             return;
         if (ctx.get_si().is_bool_op(n->get_expr()))
             return; 
-        for (euf::enode* sib : euf::enode_class(n))
+        m_trail.push_back(std::make_pair(update::relevant_node, 0));
-            set_relevant(sib);
-    }
-
-    void relevancy::set_relevant(euf::enode* n) {
-        if (n->is_relevant())
-            return;
-        ctx.get_egraph().set_relevant(n);
         m_queue.push_back(std::make_pair(sat::null_literal, n));
     }
 
@@ -237,9 +241,22 @@ namespace smt {
     }
 
     void relevancy::propagate_relevant(euf::enode* n) {
-        relevant_eh(n);
+        m_stack.push_back(n);
-        for (euf::enode* arg : euf::enode_args(n))
+        while (!m_stack.empty()) {
-            mark_relevant(arg);
+            n = m_stack.back();
+            unsigned sz = m_stack.size();
+            for (euf::enode* arg : euf::enode_args(n)) 
+                if (!arg->is_relevant())                  
+                    m_stack.push_back(arg);                            
+            if (sz == m_stack.size()) {
+                ctx.get_egraph().set_relevant(n);
+                relevant_eh(n);
+                for (euf::enode* sib : euf::enode_class(n))
+                    if (!sib->is_relevant())
+                        mark_relevant(sib);
+                m_stack.pop_back();
+            }
+        }
     }
 
     void relevancy::set_enabled(bool e) {

src/sat/smt/smt_relevant.h

@@ -106,7 +106,7 @@ namespace smt {
     class relevancy {
         euf::solver&         ctx;
 
-        enum class update { relevant_var, add_clause, set_root, set_qhead };
+        enum class update { relevant_var, relevant_node, add_clause, set_root, set_qhead };
        
         bool                                 m_enabled = false;
         svector<std::pair<update, unsigned>> m_trail;
@@ -119,6 +119,7 @@ namespace smt {
         vector<unsigned_vector>              m_occurs;            // where do literals occur
         unsigned                             m_qhead = 0;         // queue head for relevancy
         svector<std::pair<sat::literal, euf::enode*>> m_queue;    // propagation queue for relevancy
+        euf::enode_vector                    m_stack;
 
         // callbacks during propagation
         void relevant_eh(euf::enode* n);
@@ -133,8 +134,6 @@ namespace smt {
 
         void propagate_relevant(euf::enode* n);
 
-        void set_relevant(euf::enode* n);
-
     public:
         relevancy(euf::solver& ctx);