add direct and incremental relevancy propagator

src/sat/smt/CMakeLists.txt

@@ -40,6 +40,7 @@ z3_add_component(sat_smt
     recfun_solver.cpp
     sat_dual_solver.cpp
     sat_th.cpp
+    smt_relevancy.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES
     sat

src/sat/smt/smt_relevancy.cpp

@@ -0,0 +1,228 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    relevancy.cpp
+
+Abstract:
+
+    Relevancy propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-12-27
+
+
+
+--*/
+#include "sat/sat_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/smt_relevancy.h"
+
+
+namespace smt {
+
+    relevancy::relevancy(euf::solver& ctx): ctx(ctx) {
+        m_enabled = ctx.relevancy_enabled();
+    }
+
+    void relevancy::relevant_eh(euf::enode* n) {
+        // callback into ctx.
+    }
+
+    void relevancy::relevant_eh(sat::literal lit) {
+        // callback into ctx.
+    }
+    
+    void relevancy::pop(unsigned n) {
+        if (n <= m_num_scopes) {
+            m_num_scopes -= n;
+            return;
+        }
+        else if (m_num_scopes > 0) {
+            n -= m_num_scopes;
+            m_num_scopes = 0;
+        }
+        SASSERT(n > 0);
+        unsigned sz = m_lim[m_lim.size() - n];
+        for (unsigned i = m_trail.size(); i-- > sz; ) {
+            auto [u, idx] = m_trail[i];
+            switch (u) {
+            case update::relevant_expr:
+                m_relevant_expr_ids[idx] = false;
+                m_queue.pop_back();
+                break;
+            case update::relevant_var:
+                m_relevant_var_ids[idx] = false;
+                m_queue.pop_back();
+                break;
+            case update::add_clause: {
+                sat::clause* c = m_clauses.back();
+                for (sat::literal lit : *c) {
+                    SASSERT(m_occurs[lit.index()] == m_clauses.size() - 1);
+                    m_occurs[lit.index()].pop_back();
+                }
+                m_clauses.pop_back();
+                m_roots.pop_back();
+                m_alloc.del_clause(c);
+                break;
+            }
+            case update::set_root:
+                m_roots[idx] = false;
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        m_trail.shrink(sz);
+        m_lim.shrink(m_lim.size() - n);
+    }
+    
+    void relevancy::add_root(unsigned n, sat::literal const* lits) {
+        if (!m_enabled)
+            return;
+        flush();
+        sat::literal true_lit = sat::null_literal;
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_true) {
+                if (is_relevant(lits[i]))
+                    return;
+                true_lit = lits[i];                
+            }
+        }
+        if (true_lit != sat::null_literal) {
+            mark_relevant(true_lit);
+            return;
+        }
+
+        sat::clause cl = *m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(&cl);
+        m_roots.push_back(true);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : cl) 
+            occurs(lit).push_back(sz);
+    }
+    
+    void relevancy::add_def(unsigned n, sat::literal const* lits) {
+        if (!m_enabled)
+            return;
+        flush();
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) {
+                add_root(n, lits);
+                return;
+            }
+        }
+        sat::clause cl = *m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(&cl);
+        m_roots.push_back(false);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : cl) 
+            occurs(lit).push_back(sz);        
+    }
+
+    void relevancy::assign(sat::literal lit) {
+        if (!m_enabled)
+            return;
+        flush();
+        if (ctx.s().lvl(lit) == 0) {
+            mark_relevant(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);
+            return;
+        next:
+            ;
+        }
+    }
+
+    void relevancy::propagate() {
+        if (!m_enabled)
+            return;
+        flush();
+        if (m_qhead == m_queue.size())
+            return;
+        m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
+        while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
+            auto [lit, n] = m_queue[m_qhead++];
+            SASSERT(n || lit != sat::null_literal);
+            SASSERT(!n || lit == sat::null_literal);
+            if (n)
+                propagate_relevant(n);
+            else 
+                propagate_relevant(lit);            
+        }
+    }
+    
+    void relevancy::mark_relevant(euf::enode* n) {
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(n))
+            return;
+        for (euf::enode* sib : euf::enode_class(n))
+            set_relevant(sib);
+    }
+
+    void relevancy::set_relevant(euf::enode* n) {
+        if (is_relevant(n))
+            return;
+        m_relevant_expr_ids.setx(n->get_expr_id(), true, false);
+        m_trail.push_back(std::make_pair(update::relevant_expr, n->get_expr_id()));
+        m_queue.push_back(std::make_pair(sat::null_literal, n));
+    }
+
+    void relevancy::mark_relevant(sat::literal lit) {
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(lit))
+            return;
+        m_relevant_var_ids.setx(lit.var(), true, false);
+        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
+        m_queue.push_back(std::make_pair(lit, nullptr));
+    }
+
+    void relevancy::propagate_relevant(sat::literal lit) {
+        relevant_eh(lit);
+        for (auto idx : occurs(~lit)) {
+            if (m_roots[idx])
+                continue;
+            sat::clause& cl = *m_clauses[idx];
+            sat::literal true_lit = sat::null_literal;
+            for (sat::literal lit2 : cl) {
+                if (ctx.s().value(lit2) == l_true) {
+                    if (is_relevant(lit2))
+                        goto next;
+                    true_lit = lit2;
+                }
+            }
+
+            if (true_lit != sat::null_literal)
+                mark_relevant(true_lit);
+            else {
+                m_trail.push_back(std::make_pair(update::set_root, idx));
+                m_roots[idx] = true;
+            }
+        next:
+            ;
+        }
+    }
+
+    void relevancy::propagate_relevant(euf::enode* n) {
+        relevant_eh(n);
+        for (euf::enode* arg : euf::enode_args(n))
+            mark_relevant(arg);
+    }
+
+}

src/sat/smt/smt_relevancy.h

@@ -0,0 +1,143 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    relevancy.h
+
+Abstract:
+
+    Relevancy propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-12-27
+
+
+Clauses are split into two parts:
+
+- Roots
+- Defs
+
+The state transitions are:
+
+- A literal lit is assigned:
+  lit appears positively in a Root clause R and no other literal in R are relevant.
+  ->
+  lit is set relevant
+
+  lit is justified at level 0
+  -> 
+  lit is set relevant
+
+- An equality n1 = n2 is assigned:
+  n1 is relevant
+  -> 
+  n2 is marked as relevant
+
+- A lit is set relevant:
+  -> 
+  all clauses C in Defs where lit appears negatively are added to Roots
+
+ - When a clause R is added to Roots:
+  R contains a positive literal lit that is relevant
+  ->
+  skip adding R to Roots
+
+- When a clause R is added to Roots:
+  R contains a positive literal lit, no positive literal in R are relevant
+  ->
+  lit is set relevant 
+
+- When a clause C is added to Defs:
+  C contains a negative literal that is relevant
+  -> 
+  Add C to Roots
+
+- When an expression is set relevant:
+  All non-relevant children above Boolean connectives are set relevant
+  If nodes are treated as Boolean connectives because they are clausified
+  to (=> cond (= n then)) and (=> (not cond) (= n else))
+
+Replay:
+  - literals that are replayed in clauses that are marked relevant are 
+    marked relevant again.
+
+  - expressions corresponding to auxiliary clauses are added as auxiliary clauses.
+  
+  - TBD: Are root clauses added under a scope discarded?
+    The SAT solver re-initializes clauses on its own, should we just use this mechanism?
+
+Can a literal that is not in a root be set relevant?
+ - yes, if we propagate over expressions
+
+Do we need full watch lists instead of 2-watch lists?
+ - probably, but unclear. The dual SAT solver only uses 2-watch lists, but has uses a large clause for tracking 
+   roots.
+
+
+
+--*/
+#pragma once
+#include "sat/sat_solver.h"
+#include "sat/smt/sat_th.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace smt {
+
+    class relevancy {
+        euf::solver&         ctx;
+
+        enum class update { relevant_expr, relevant_var, add_clause, set_root, set_qhead };
+       
+        bool                                 m_enabled = false;
+        svector<std::pair<update, unsigned>> m_trail;
+        unsigned_vector                      m_lim;
+        unsigned                             m_num_scopes = 0;
+        bool_vector                          m_relevant_expr_ids; // identifiers of relevant expressions
+        bool_vector                          m_relevant_var_ids;  // identifiers of relevant Boolean variables
+        sat::clause_allocator                m_alloc;
+        sat::clause_vector                   m_clauses;           // clauses
+        bool_vector                          m_roots;             // indicate if clause is a root
+        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
+
+        // 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(); }
+
+        unsigned_vector& occurs(sat::literal lit) { m_occurs.reserve(lit.index() + 1); return m_occurs[lit.index()]; }
+
+        void propagate_relevant(sat::literal lit);
+
+        void propagate_relevant(euf::enode* n);
+
+        void set_relevant(euf::enode* n);
+
+    public:
+        relevancy(euf::solver& ctx);
+
+        void push() { ++m_num_scopes; }
+        void pop(unsigned n);
+
+        void add_root(unsigned n, sat::literal const* lits);
+        void add_def(unsigned n, sat::literal const* lits);
+        void assign(sat::literal lit);
+        void propagate();
+
+        void mark_relevant(euf::enode* n);
+        void mark_relevant(sat::literal lit);
+
+        bool is_relevant(sat::literal lit) const { return !m_enabled || m_relevant_var_ids.get(lit.var(), false); }
+        bool is_relevant(euf::enode* n) const { return !m_enabled || m_relevant_expr_ids.get(n->get_expr_id(), false); }
+        bool is_relevant(expr* e) const { return !m_enabled || m_relevant_expr_ids.get(e->get_id(), false); }
+               
+    };
+}