From 62bb234251916dd7ef95f5c101742c1c770415c2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 Jan 2022 11:56:44 -0800
Subject: [PATCH] expose extract roots as separate

---
 src/sat/sat_scc.cpp | 35 +++++++++++++++++++++--------------
 src/sat/sat_scc.h   |  4 ++++
 2 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index e7adc33ec..c21f67ce5 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -67,15 +67,8 @@ namespace sat {
         }
     };
 
-    unsigned scc::operator()() {
-        if (m_solver.m_inconsistent)
-            return 0;
-        if (!m_scc)
-            return 0;
-        CASSERT("scc_bug", m_solver.check_invariant());
-        report rpt(*this);
-        TRACE("scc", m_solver.display(tout););
-        TRACE("scc_details", m_solver.display_watches(tout););
+    bool scc::extract_roots(literal_vector& roots, bool_var_vector& to_elim) {
+        literal_vector lits;
         unsigned_vector index;
         unsigned_vector lowlink;
         unsigned_vector s;
@@ -84,11 +77,9 @@ namespace sat {
         index.resize(num_lits, UINT_MAX);
         lowlink.resize(num_lits, UINT_MAX);
         in_s.resize(num_lits, false);
-        literal_vector roots, lits;
         roots.resize(m_solver.num_vars(), null_literal);
         unsigned next_index = 0;
         svector<frame>   frames;
-        bool_var_vector  to_elim;
         
         for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
             if (index[l_idx] != UINT_MAX)
@@ -182,7 +173,7 @@ namespace sat {
                             j--;
                             if (to_literal(l2_idx) == ~l) {
                                 m_solver.set_conflict();
-                                return 0;
+                                return false;
                             }
                             if (m_solver.is_external(to_literal(l2_idx).var())) {
                                 r = to_literal(l2_idx);
@@ -226,6 +217,23 @@ namespace sat {
                 roots[i] = literal(i, false);
             }
         }
+        return true;
+    }
+
+
+    unsigned scc::operator()() {
+        if (m_solver.m_inconsistent)
+            return 0;
+        if (!m_scc)
+            return 0;
+        CASSERT("scc_bug", m_solver.check_invariant());
+        report rpt(*this);
+        TRACE("scc", m_solver.display(tout););
+        TRACE("scc_details", m_solver.display_watches(tout););
+        literal_vector roots;
+        bool_var_vector to_elim;
+        if (!extract_roots(roots, to_elim))
+            return 0;
         TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
               tout << "to_elim: "; for (unsigned v : to_elim) tout << v << " "; tout << "\n";);
         m_num_elim += to_elim.size();
@@ -234,9 +242,8 @@ namespace sat {
         TRACE("scc_detail", m_solver.display(tout););
         CASSERT("scc_bug", m_solver.check_invariant());
 
-        if (m_scc_tr) {
+        if (m_scc_tr) 
             reduce_tr();
-        }
         TRACE("scc_detail", m_solver.display(tout););
         return to_elim.size();
     }
diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h
index 0554e09d4..af239c53d 100644
--- a/src/sat/sat_scc.h
+++ b/src/sat/sat_scc.h
@@ -41,9 +41,13 @@ namespace sat {
         void reduce_tr();
         unsigned reduce_tr(bool learned);
 
+
     public:
 
         scc(solver & s, params_ref const & p);
+
+        bool extract_roots(literal_vector& roots, bool_var_vector& lits);
+
         unsigned operator()();
 
         void updt_params(params_ref const & p);