Improved tracing for equivalence classes of EE (#6169)

Helps debugging model issues.

2 files changed, 56 insertions, 38 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 2a5d043f5..b92cdaf5b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -203,8 +203,13 @@ void TheoryStrings::presolve() {
 bool TheoryStrings::collectModelValues(TheoryModel* m,
                                        const std::set<Node>& termSet)
 {
-  Trace("strings-model") << "TheoryStrings : Collect model values" << std::endl;
-
+  if (Trace.isOn("strings-model"))
+  {
+    Trace("strings-model") << "TheoryStrings : Collect model values"
+                           << std::endl;
+    Trace("strings-model") << "Equivalence classes are:" << std::endl;
+    Trace("strings-model") << debugPrintStringsEqc() << std::endl;
+  }
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
   // Generate model
   // get the relevant string equivalence classes
@@ -629,42 +634,7 @@ void TheoryStrings::postCheck(Effort e)
         << "Theory of strings " << e << " effort check " << std::endl;
     if (Trace.isOn("strings-eqc"))
     {
-      for (unsigned t = 0; t < 2; t++)
-      {
-        eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
-        Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
-        while( !eqcs2_i.isFinished() ){
-          Node eqc = (*eqcs2_i);
-          bool print = (t == 0 && eqc.getType().isStringLike())
-                       || (t == 1 && !eqc.getType().isStringLike());
-          if (print) {
-            eq::EqClassIterator eqc2_i =
-                eq::EqClassIterator(eqc, d_equalityEngine);
-            Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
-            while( !eqc2_i.isFinished() ) {
-              if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){
-                Trace("strings-eqc") << (*eqc2_i) << " ";
-              }
-              ++eqc2_i;
-            }
-            Trace("strings-eqc") << " } " << std::endl;
-            EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
-            if( ei ){
-              Trace("strings-eqc-debug")
-                  << "* Length term : " << ei->d_lengthTerm.get() << std::endl;
-              Trace("strings-eqc-debug")
-                  << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get()
-                  << std::endl;
-              Trace("strings-eqc-debug")
-                  << "* Normalization length lemma : "
-                  << ei->d_normalizedLength.get() << std::endl;
-            }
-          }
-          ++eqcs2_i;
-        }
-        Trace("strings-eqc") << std::endl;
-      }
-      Trace("strings-eqc") << std::endl;
+      Trace("strings-eqc") << debugPrintStringsEqc() << std::endl;
     }
     ++(d_statistics.d_checkRuns);
     bool sentLemma = false;
@@ -1074,6 +1044,52 @@ void TheoryStrings::runStrategy(Theory::Effort e)
   Trace("strings-process") << "----finished round---" << std::endl;
 }
 
+std::string TheoryStrings::debugPrintStringsEqc()
+{
+  std::stringstream ss;
+  for (unsigned t = 0; t < 2; t++)
+  {
+    eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
+    ss << (t == 0 ? "STRINGS:" : "OTHER:") << std::endl;
+    while (!eqcs2_i.isFinished())
+    {
+      Node eqc = (*eqcs2_i);
+      bool print = (t == 0 && eqc.getType().isStringLike())
+                   || (t == 1 && !eqc.getType().isStringLike());
+      if (print)
+      {
+        eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
+        ss << "Eqc( " << eqc << " ) : { ";
+        while (!eqc2_i.isFinished())
+        {
+          if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL)
+          {
+            ss << (*eqc2_i) << " ";
+          }
+          ++eqc2_i;
+        }
+        ss << " } " << std::endl;
+        EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
+        if (ei)
+        {
+          Trace("strings-eqc-debug")
+              << "* Length term : " << ei->d_lengthTerm.get() << std::endl;
+          Trace("strings-eqc-debug")
+              << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get()
+              << std::endl;
+          Trace("strings-eqc-debug")
+              << "* Normalization length lemma : "
+              << ei->d_normalizedLength.get() << std::endl;
+        }
+      }
+      ++eqcs2_i;
+    }
+    ss << std::endl;
+  }
+  ss << std::endl;
+  return ss.str();
+}
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 12f644fb4..f35c67da6 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -241,6 +241,8 @@ class TheoryStrings : public Theory {
   void runInferStep(InferStep s, int effort);
   /** run strategy for effort e */
   void runStrategy(Theory::Effort e);
+  /** print strings equivalence classes for debugging */
+  std::string debugPrintStringsEqc();
   /** Commonly used constants */
   Node d_true;
   Node d_false;