revert relevancy2

src/sat/smt/euf_relevancy.cpp

@@ -89,7 +89,7 @@ namespace euf {
         m_dual_solver->track_relevancy(v);
     }
 
-    bool solver::init_relevancy1() {
+    bool solver::init_relevancy() {
         m_relevant_expr_ids.reset();
         if (!relevancy_enabled())
             return true;
@@ -113,51 +113,6 @@ namespace euf {
             m_relevant_todo.push_back(e);
     }
 
-
-    bool solver::init_relevancy2() {
-        m_relevant_expr_ids.reset();
-        if (!relevancy_enabled())
-            return true;
-        init_relevant_expr_ids();
-        for (unsigned i = 0; i < s().trail_size(); ++i) {
-            sat::literal l = s().trail_literal(i);
-            auto v = l.var();
-            auto j = s().get_justification(v);
-            switch (j.get_kind()) {
-            case sat::justification::kind::BINARY:
-            case sat::justification::kind::TERNARY:
-            case sat::justification::kind::CLAUSE:
-            case sat::justification::kind::EXT_JUSTIFICATION:
-                push_relevant(l.var());
-                break;
-            case sat::justification::kind::NONE: 
-                for (auto const& w : s().get_wlist(~l)) {
-                    if (w.is_binary_non_learned_clause()) {
-                        if (is_propagated(w.get_literal()))
-                            continue;
-                    }
-                    else if (w.is_binary_clause())
-                        continue;
-                    else if (w.is_ternary_clause()) {
-                        if (is_propagated(w.get_literal1()))
-                            continue;
-                        if (is_propagated(w.get_literal2()))
-                            continue;
-                    }
-                    else if (w.is_clause()) {
-                        if (is_propagated(w.get_blocked_literal()))
-                            continue;
-                    }
-                    push_relevant(l.var());
-                    break;
-                }
-                break;            
-            }
-        }
-        relevant_subterms();
-        return true;
-    }
-
     bool solver::is_propagated(sat::literal lit) {
         return s().value(lit) == l_true && !s().get_justification(lit.var()).is_none();
     }

src/sat/smt/euf_solver.cpp

@@ -459,7 +459,7 @@ namespace euf {
         if (unit_propagate())
             return sat::check_result::CR_CONTINUE;
 
-        if (!init_relevancy1())
+        if (!init_relevancy())
             give_up = true;
         
         unsigned num_nodes = m_egraph.num_nodes();

src/sat/smt/euf_solver.h

@@ -185,8 +185,7 @@ namespace euf {
         bool_vector m_relevant_visited;
         ptr_vector<expr> m_relevant_todo;
         void ensure_dual_solver();
-        bool init_relevancy1();
+        bool init_relevancy();
-        bool init_relevancy2();
         void relevant_subterms();
         void init_relevant_expr_ids();
         void push_relevant(sat::bool_var v);

src/sat/smt/sat_dual_solver.cpp

@@ -149,6 +149,7 @@ namespace sat {
         if (is_sat == l_true) {
             TRACE("dual", display(s, tout); s.display(tout););
             IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
+            IF_VERBOSE(0, display(s, verbose_stream()); s.display(verbose_stream()););
             UNREACHABLE();
             return false;
         }