relevancy overhaul

src/ast/euf/euf_egraph.cpp

@@ -785,8 +785,15 @@ namespace euf {
                 out << " " << p->get_expr_id();
             out << "] ";
         }
-        if (n->value() != l_undef) 
+        auto value_of = [&]() {
-            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
+            switch (n->value()) {
+            case l_true: return "T";
+            case l_false: return "F";
+            default: return "?";
+            }
+        };
+        if (n->bool_var() != sat::null_bool_var) 
+            out << "[b" << n->bool_var() << " := " << value_of() << (n->merge_tf() ? "" : " no merge") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
             for (auto const& v : enode_th_vars(n))

src/sat/smt/euf_model.cpp

@@ -161,10 +161,9 @@ namespace euf {
                 default:
                     break;
                 }
-                if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
-                    continue;
                 sat::bool_var v = get_enode(e)->bool_var();
-                SASSERT(v != sat::null_bool_var);
+                if (v == sat::null_bool_var)
+                    continue;
                 switch (s().value(v)) {
                 case l_true:
                     m_values.set(id, m.mk_true());
@@ -224,7 +223,7 @@ namespace euf {
                     enode* earg = get_enode(arg); 
                     expr* val = m_values.get(earg->get_root_id());
                     args.push_back(val);                
-                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
+                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n" << bpp(n) << "\n"; display(tout););
                     SASSERT(val);
                 }
                 SASSERT(args.size() == arity);

src/sat/smt/euf_relevancy.cpp

@@ -21,28 +21,6 @@ Author:
 
 namespace euf {
     
-    relevancy::relevancy(euf::solver& ctx): ctx(ctx) {
-    }
-
-    void relevancy::relevant_eh(euf::enode* n) {
-        SASSERT(is_relevant(n));
-        ctx.relevant_eh(n);
-    }
-
-    void relevancy::relevant_eh(sat::literal lit) {
-        SASSERT(is_relevant(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) {
         if (!m_enabled)
             return;
@@ -61,9 +39,8 @@ namespace euf {
             switch (u) {
             case update::relevant_var:
                 m_relevant_var_ids[idx] = false;
-                m_queue.pop_back();
                 break;
-            case update::relevant_node:
+            case update::add_queue:
                 m_queue.pop_back();
                 break;
             case update::add_clause: {
@@ -124,6 +101,7 @@ namespace euf {
         if (!m_enabled)
             return;
         flush();
+        TRACE("relevancy", tout << "def " << sat::literal_vector(n, lits) << "\n");
         for (unsigned i = 0; i < n; ++i) {
             if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) {
                 add_root(n, lits);
@@ -141,21 +119,42 @@ namespace euf {
         }
     }
 
+    void relevancy::add_to_propagation_queue(sat::literal lit) {
+        m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
+        m_queue.push_back(std::make_pair(lit, nullptr));
+    }
+
+    void relevancy::set_relevant(sat::literal lit) {
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n)
+            mark_relevant(n);        
+        m_relevant_var_ids.setx(lit.var(), true, false);
+        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
+    }
+
     void relevancy::asserted(sat::literal lit) {
+        TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
         if (!m_enabled)
             return;
         flush();
-        if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) {
+        if (is_relevant(lit)) {
-            mark_relevant(lit);
+            add_to_propagation_queue(lit);
             return;
         }
+        if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) {
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
+            return;
+        }
+
         for (auto idx : occurs(lit)) {
             if (!m_roots[idx])
                 continue;
             for (sat::literal lit2 : *m_clauses[idx]) 
                 if (lit2 != lit && ctx.s().value(lit2) == l_true && is_relevant(lit2))
                     goto next;  
-            mark_relevant(lit);
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
             return;
         next:
             ;
@@ -181,6 +180,7 @@ namespace euf {
     }
 
     void relevancy::merge(euf::enode* root, euf::enode* other) {
+        TRACE("relevancy", tout << "merge #" << ctx.bpp(root) << " " << is_relevant(root) << " #" << ctx.bpp(other) << " " << is_relevant(other) << "\n");
         if (is_relevant(root))
             mark_relevant(other);
         else if (is_relevant(other))
@@ -193,28 +193,36 @@ namespace euf {
         flush();
         if (is_relevant(n))
             return;
-        if (ctx.get_si().is_bool_op(n->get_expr()))
+        TRACE("relevancy", tout << "mark #" << ctx.bpp(n) << "\n");
-            return; 
+        m_trail.push_back(std::make_pair(update::add_queue, 0));
-        m_trail.push_back(std::make_pair(update::relevant_node, 0));
         m_queue.push_back(std::make_pair(sat::null_literal, n));
     }
 
     void relevancy::mark_relevant(sat::literal lit) {
+        TRACE("relevancy", tout << "mark " << lit << " " << is_relevant(lit) << " " << ctx.s().value(lit) << " lim: " << m_lim.size() << "\n");
         if (!m_enabled)
             return;
         flush();
         if (is_relevant(lit))
             return;        
-        euf::enode* n = ctx.bool_var2enode(lit.var());
+        set_relevant(lit);
-        if (n)
+        switch (ctx.s().value(lit)) {
-            mark_relevant(n);
+        case l_true:
-        m_relevant_var_ids.setx(lit.var(), true, false);
+            break;
-        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
+        case l_false:
-        m_queue.push_back(std::make_pair(lit, nullptr));
+            lit.neg();
+            break;
+        default:
+            return;               
+        }
+        add_to_propagation_queue(lit);
     }
 
     void relevancy::propagate_relevant(sat::literal lit) {
-        relevant_eh(lit);
+        SASSERT(m_num_scopes == 0);
+        TRACE("relevancy", tout << "propagate " << lit << " lim: " << m_lim.size() << "\n");
+        SASSERT(ctx.s().value(lit) == l_true);
+        SASSERT(is_relevant(lit));
         euf::enode* n = ctx.bool_var2enode(lit.var());
         if (n && !ctx.get_si().is_bool_op(n->get_expr()))
             return;
@@ -231,13 +239,17 @@ namespace euf {
                 }
             }
 
-            if (true_lit != sat::null_literal)
+            if (true_lit != sat::null_literal) {
-                mark_relevant(true_lit);
+                set_relevant(true_lit);
+                add_to_propagation_queue(true_lit);
+                ctx.asserted(true_lit);
+            }
             else {
                 m_trail.push_back(std::make_pair(update::set_root, idx));
                 m_roots[idx] = true;
             }
         next:
+            TRACE("relevancy", tout << "propagate " << lit << " " << true_lit << " " << m_roots[idx] << "\n");
             ;
         }
     }
@@ -247,22 +259,25 @@ namespace euf {
         while (!m_todo.empty()) {
             n = m_todo.back();
             m_todo.pop_back();
+            TRACE("relevancy", tout << "propagate #" << ctx.bpp(n) << " lim: " << m_lim.size() << "\n");
             if (n->is_relevant())
                 continue;
-            if (ctx.get_si().is_bool_op(n->get_expr()))
-                continue;
             m_stack.push_back(n);
             while (!m_stack.empty()) {
                 n = m_stack.back();
                 unsigned sz = m_stack.size();
-                for (euf::enode* arg : euf::enode_args(n))
+                bool is_bool_op = ctx.get_si().is_bool_op(n->get_expr());
-                    if (!arg->is_relevant())
+                if (!is_bool_op)
-                        m_stack.push_back(arg);
+                    for (euf::enode* arg : euf::enode_args(n))
+                        if (!arg->is_relevant())
+                            m_stack.push_back(arg);
                 if (sz != m_stack.size())
                     continue;
                 if (!n->is_relevant()) {
                     ctx.get_egraph().set_relevant(n);
-                    relevant_eh(n);
+                    ctx.relevant_eh(n);
+                    if (n->bool_var() != sat::null_bool_var) 
+                        mark_relevant(sat::literal(n->bool_var()));
                     for (euf::enode* sib : euf::enode_class(n))
                         if (!sib->is_relevant())
                             m_todo.push_back(sib);

src/sat/smt/euf_relevancy.h

@@ -91,6 +91,16 @@ Do we need full watch lists instead of 2-watch lists?
    roots.
 
 
+   State machine for literals: relevant(lit), assigned(lit)
+
+relevant(lit) transitions false -> true
+   if assigned(lit):     add to propagation queue
+   if not assigned(lit): no-op (or mark enodes as relevant)
+
+assigned(lit) transitions false -> true
+   if relevant(lit):      add to propagation queue
+   if not relevant(lit):  set relevant if member of root, add to propagation queue
+
 
 --*/
 #pragma once
@@ -105,7 +115,7 @@ namespace euf {
     class relevancy {
         euf::solver&         ctx;
 
-        enum class update { relevant_var, relevant_node, add_clause, set_root, set_qhead };
+        enum class update { relevant_var, add_queue, add_clause, set_root, set_qhead };
        
         bool                                 m_enabled = false;
         svector<std::pair<update, unsigned>> m_trail;
@@ -120,10 +130,6 @@ namespace euf {
         svector<std::pair<sat::literal, euf::enode*>> m_queue;    // propagation queue for relevancy
         euf::enode_vector                    m_stack, m_todo;
 
-        // callbacks during propagation
-        void relevant_eh(euf::enode* n);
-        void relevant_eh(sat::literal lit);
-
         void push_core() { m_lim.push_back(m_trail.size()); }
         void flush() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }
 
@@ -131,10 +137,14 @@ namespace euf {
 
         void propagate_relevant(sat::literal lit);
 
+        void add_to_propagation_queue(sat::literal lit);        
+
         void propagate_relevant(euf::enode* n);
 
+        void set_relevant(sat::literal lit);
+
     public:
-        relevancy(euf::solver& ctx);
+        relevancy(euf::solver& ctx): ctx(ctx) {}
 
         void push() { if (m_enabled) ++m_num_scopes; }
         void pop(unsigned n);

src/sat/smt/euf_solver.cpp

@@ -297,11 +297,9 @@ namespace euf {
 
     void solver::asserted(literal l) {
 
-        if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) {
+        m_relevancy.asserted(l);
-            m_relevancy.asserted(l);
+        if (!m_relevancy.is_relevant(l))
-            if (!m_relevancy.is_relevant(l))
+            return;        
-                return;
-        }
 
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
         TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);

src/sat/tactic/goal2sat.cpp

@@ -126,20 +126,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         return m_top_level && relevancy_enabled();
     }
     
-    void add_dual_def(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_aux(n, lits);        
-    }
-
-    void add_dual_root(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_root(n, lits);
-    }
-
-    void add_dual_root(sat::literal lit) {
-        add_dual_root(1, &lit);
-    }
-    
     void mk_clause(sat::literal l) {
         mk_clause(1, &l);
     }
@@ -156,7 +142,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_def(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_aux(n, lits);
         m_solver.add_clause(n, lits, mk_status());
     }
 
@@ -176,7 +163,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_root_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_root(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_root(n, lits);
         m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
     }