Debug output

lib/up_scc_binary.cpp

@@ -6,9 +6,10 @@
  * Encoding based on SCCs of the graph of the implication system with levels
  * encoded in binary.
  */
+#include <iomanip>
 
-#include "up_scc_binary.h"
 #include "up_levels.h"
+#include "up_scc_binary.h"
 
 void
 SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
@@ -24,6 +25,36 @@ SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
       max_level = max_level_bound;
    }
 
+   if (logs.CheckLevel(3))
+   {
+      logs.TLog(3) << "[UPSCCUnary::Encode] Using implication system:"
+                   << std::endl;
+
+      for (unsigned i = 0; i < mImplSystem.Size(); ++i)
+      {
+         logs.Log(3) << std::setw(2) << i << " | " << mImplSystem[i]
+                     << std::endl;
+      }
+      std::vector<std::vector<Literal>> scc_literals(mSCCGraph.SCCCount());
+      logs.TLog(3) << "SCCs:";
+      for (unsigned i = 0; i < mCnf.MaxVariable() * 2; ++i)
+      {
+         Literal lit(i);
+         logs.Log(3) << " " << lit << " (" << mSCCGraph.SCC(lit) << ")";
+         scc_literals[mSCCGraph.SCC(lit)].push_back(lit);
+      }
+      logs.Log(3) << std::endl;
+      for (unsigned i = 0; i < scc_literals.size(); ++i)
+      {
+         logs.Log(3) << "SCC " << i << ":";
+         for (const auto &lit : scc_literals[i])
+         {
+            logs.Log(3) << " " << lit;
+         }
+         logs.Log(3) << std::endl;
+      }
+   }
+
    Context ctx{max_level, VarInfoList(2 * mCnf.MaxVariable()),
        mVarStore.VarArray(mCnf.MaxVariable(), true, ":in(", ")"),
        mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"), {}, {}};