Improved tracing for equivalence classes of EE (#6169)

Helps debugging model issues.

8 files changed, 124 insertions, 65 deletions

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index b9057604e..d77a88d67 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -99,6 +99,16 @@ bool ModelManager::buildModel()
 
   // now, finish building the model
   d_modelBuiltSuccess = finishBuildModel();
+
+  if (Trace.isOn("model-builder"))
+  {
+    Trace("model-builder") << "Final model:" << std::endl;
+    Trace("model-builder") << d_model->debugPrintModelEqc() << std::endl;
+  }
+
+  Trace("model-builder") << "ModelManager: model built success is "
+                         << d_modelBuiltSuccess << std::endl;
+
   return d_modelBuiltSuccess;
 }
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 7fe86d86d..47eac5359 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -656,25 +656,7 @@ void TheorySep::postCheck(Effort level)
   }
   if (Trace.isOn("sep-eqc"))
   {
-    eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
-    Trace("sep-eqc") << "EQC:" << std::endl;
-    while (!eqcs2_i.isFinished())
-    {
-      Node eqc = (*eqcs2_i);
-      eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
-      Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
-      while (!eqc2_i.isFinished())
-      {
-        if ((*eqc2_i) != eqc)
-        {
-          Trace("sep-eqc") << (*eqc2_i) << " ";
-        }
-        ++eqc2_i;
-      }
-      Trace("sep-eqc") << " } " << std::endl;
-      ++eqcs2_i;
-    }
-    Trace("sep-eqc") << std::endl;
+    Trace("sep-eqc") << d_equalityEngine->debugPrintEqc();
   }
 
   bool addedLemma = false;
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;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0c1ea7a7a..a5f8afec4 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -451,25 +451,30 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
     bool first = true;
     Node rep;
     for (; !eqc_i.isFinished(); ++eqc_i) {
-      if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
-        Trace("model-builder-debug") << "...skip node " << (*eqc_i) << " in eqc " << eqc << std::endl;
+      Node n = *eqc_i;
+      // notice that constants are always relevant
+      if (termSet != nullptr && termSet->find(n) == termSet->end()
+          && !n.isConst())
+      {
+        Trace("model-builder-debug")
+            << "...skip node " << n << " in eqc " << eqc << std::endl;
         continue;
       }
       if (predicate) {
         if (predTrue || predFalse)
         {
-          if (!assertPredicate(*eqc_i, predTrue))
+          if (!assertPredicate(n, predTrue))
           {
             return false;
           }
         }
         else {
           if (first) {
-            rep = (*eqc_i);
+            rep = n;
             first = false;
           }
           else {
-            Node eq = (*eqc_i).eqNode(rep);
+            Node eq = (n).eqNode(rep);
             Trace("model-builder-assertions")
                 << "(assert " << eq << ");" << std::endl;
             d_equalityEngine->assertEquality(eq, true, Node::null());
@@ -481,7 +486,7 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
         }
       } else {
         if (first) {
-          rep = (*eqc_i);
+          rep = n;
           //add the term (this is specifically for the case of singleton equivalence classes)
           if (rep.getType().isFirstClass())
           {
@@ -491,7 +496,7 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
           first = false;
         }
         else {
-          if (!assertEquality(*eqc_i, rep, true))
+          if (!assertEquality(n, rep, true))
           {
             return false;
           }
@@ -745,5 +750,19 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
 
 const std::string& TheoryModel::getName() const { return d_name; }
 
+std::string TheoryModel::debugPrintModelEqc() const
+{
+  std::stringstream ss;
+  ss << "--- Equivalence classes:" << std::endl;
+  ss << d_equalityEngine->debugPrintEqc() << std::endl;
+  ss << "--- Representative map: " << std::endl;
+  for (const std::pair<const Node, Node>& r : d_reps)
+  {
+    ss << r.first << " -> " << r.second << std::endl;
+  }
+  ss << "---" << std::endl;
+  return ss.str();
+}
+
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 2f895ab83..0c7f092bc 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -347,6 +347,11 @@ public:
   //---------------------------- end function values
   /** Get the name of this model */
   const std::string& getName() const;
+  /**
+   * For debugging, print the equivalence classes of the underlying equality
+   * engine.
+   */
+  std::string debugPrintModelEqc() const;
 
  protected:
   /** Unique name of this model */
@@ -405,7 +410,6 @@ public:
    * a model builder constructs this model.
    */
   virtual void addTermInternal(TNode n);
-
  private:
   /** cache for getModelValue */
   mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 8b44cc4d9..2d34bd547 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2075,6 +2075,29 @@ void EqualityEngine::debugPrintGraph() const {
   Debug("equality::graph") << std::endl;
 }
 
+std::string EqualityEngine::debugPrintEqc() const
+{
+  std::stringstream ss;
+  eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(this);
+  while (!eqcs2_i.isFinished())
+  {
+    Node eqc = (*eqcs2_i);
+    eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, this);
+    ss << "Eqc( " << eqc << " ) : { ";
+    while (!eqc2_i.isFinished())
+    {
+      if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL)
+      {
+        ss << (*eqc2_i) << " ";
+      }
+      ++eqc2_i;
+    }
+    ss << " } " << std::endl;
+    ++eqcs2_i;
+  }
+  return ss.str();
+}
+
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
   Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index b81a17dcf..d1c0ece95 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -93,6 +93,9 @@ class EqualityEngine : public context::ContextNotifyObj {
    */
   void setMasterEqualityEngine(EqualityEngine* master);
 
+  /** Print the equivalence classes for debugging */
+  std::string debugPrintEqc() const;
+
   /** Statistics about the equality engine instance */
   struct Statistics
   {