debug relevancy mode

src/sat/smt/euf_relevancy.cpp

@@ -73,6 +73,13 @@ namespace euf {
         return m_relevant_expr_ids.get(n->get_expr_id(), true); 
     }
 
+    bool solver::is_relevant(bool_var v) const {
+        if (m_relevancy.enabled())
+            return m_relevancy.is_relevant(v);
+        expr* e = bool_var2expr(v);
+        return !e || is_relevant(e);
+    }
+
     void solver::ensure_dual_solver() {
         if (m_relevancy.enabled())
             return;

src/sat/smt/euf_solver.cpp

@@ -813,7 +813,7 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             expr* e = m_bool_var2expr[v];
-            out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
+            out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);

src/sat/smt/euf_solver.h

@@ -257,7 +257,7 @@ namespace euf {
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) const { return m_egraph.find(e); }
         enode* bool_var2enode(sat::bool_var b) const {
-            expr* e = m_bool_var2expr.get(b);
+            expr* e = m_bool_var2expr.get(b, nullptr);
             return e ? get_enode(e) : nullptr;
         }
         sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); }
@@ -394,6 +394,7 @@ namespace euf {
         void track_relevancy(sat::bool_var v);
         bool is_relevant(expr* e) const;
         bool is_relevant(enode* n) const;
+        bool is_relevant(bool_var v) const;
         void add_auto_relevant(sat::literal lit);
         void pop_relevant(unsigned n);
         void push_relevant();

src/sat/smt/q_ematch.cpp

@@ -589,7 +589,7 @@ namespace q {
             return m_inst_queue.propagate() || propagated;
         ctx.push(value_trail<unsigned>(m_qhead));
         ptr_buffer<binding> to_remove;
-        for (; m_qhead < m_clause_queue.size(); ++m_qhead) {
+        for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) {
             unsigned idx = m_clause_queue[m_qhead];
             clause& c = *m_clauses[idx];
             binding* b = c.m_bindings;

src/sat/smt/smt_relevant.cpp

@@ -61,7 +61,7 @@ namespace smt {
             case update::add_clause: {
                 sat::clause* c = m_clauses.back();
                 for (sat::literal lit : *c) {
-                    SASSERT(m_occurs[lit.index()] == m_clauses.size() - 1);
+                    SASSERT(m_occurs[lit.index()].back() == m_clauses.size() - 1);
                     m_occurs[lit.index()].pop_back();
                 }
                 m_clauses.pop_back();

src/sat/smt/smt_relevant.h

@@ -19,6 +19,21 @@ Clauses are split into two parts:
 - Roots
 - Defs
 
+The goal is to establish a labeling of literals as "relevant" such that
+- the set of relevant literals satisfies Roots
+- there is a set of blocked literals that can be used to satisfy the clauses in Defs
+  independent of their real assignment.
+
+The idea is that the Defs clauses are obtained from Tseitin transformation so they can be
+grouped by the blocked literal that was used to introduce them.
+For example, when clausifying (and a b) we have the clauses
+(=> (and a b) a)
+(=> (and a b) b)
+(or (not a) (not b) (and a b))
+then the literal for "(and a b)" is blocked.
+And recursively for clauses introduced for a, b if they use a Boolean connectives
+at top level.
+
 The state transitions are:
 
 - A literal lit is assigned:
@@ -37,7 +52,7 @@ The state transitions are:
 
 - A lit is set relevant:
   -> 
-  all clauses C in Defs where lit appears negatively are added to Roots
+  all clauses D 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
@@ -49,10 +64,10 @@ The state transitions are:
   ->
   lit is set relevant 
 
-- When a clause C is added to Defs:
-  C contains a negative literal that is relevant
+- When a clause D is added to Defs:
+  D contains a negative literal that is relevant
   -> 
-  Add C to Roots
+  Add D to Roots
 
 - When an expression is set relevant:
   All non-relevant children above Boolean connectives are set relevant
@@ -138,7 +153,8 @@ namespace smt {
         void mark_relevant(sat::literal lit);
         void merge(euf::enode* n1, euf::enode* n2);
 
-        bool is_relevant(sat::literal lit) const { return !m_enabled || m_relevant_var_ids.get(lit.var(), false); }
+        bool is_relevant(sat::bool_var v) const { return !m_enabled || m_relevant_var_ids.get(v, false); }
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
         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); }