Minor updates to string utilities (#3675)

6 files changed, 58 insertions, 16 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index c9a2bcd70..2b5338a6a 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/kind.h"
 #include "options/strings_options.h"
+#include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_rewriter.h"
@@ -625,6 +626,17 @@ void InferenceManager::explain(TNode literal,
     }
   }
 }
+void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
+void InferenceManager::markCongruent(Node a, Node b)
+{
+  Assert(a.getKind() == b.getKind());
+  ExtTheory* eth = d_parent.getExtTheory();
+  if (eth->hasFunctionKind(a.getKind()))
+  {
+    eth->markCongruent(a, b);
+  }
+}
 
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index e052889f6..819e4b98f 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -61,7 +61,8 @@ class TheoryStrings;
  * to doPendingLemmas.
  *
  * It also manages other kinds of interaction with the output channel of the
- * theory of strings, e.g. sendPhaseRequirement.
+ * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
+ * with the extended theory object e.g. markCongruent.
  */
 class InferenceManager
 {
@@ -249,6 +250,19 @@ class InferenceManager
    * the node corresponding to their conjunction.
    */
   void explain(TNode literal, std::vector<TNode>& assumptions) const;
+  /**
+   * Set that we are incomplete for the current set of assertions (in other
+   * words, we must answer "unknown" instead of "sat"); this calls the output
+   * channel's setIncomplete method.
+   */
+  void setIncomplete();
+  /**
+   * Mark that terms a and b are congruent in the current context.
+   * This makes a call to markCongruent in the extended theory object of
+   * the parent theory if the kind of a (and b) is owned by the extended
+   * theory.
+   */
+  void markCongruent(Node a, Node b);
 
  private:
   /**
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1bc104096..01f9fc99a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2806,7 +2806,7 @@ void TheoryStrings::getNormalForms(Node eqc,
                 if (Trace.isOn("strings-error"))
                 {
                   Trace("strings-error") << "Cycle for normal form ";
-                  printConcat(currv, "strings-error");
+                  utils::printConcatTrace(currv, "strings-error");
                   Trace("strings-error") << "..." << currv[i] << std::endl;
                 }
                 Assert(!d_state.areEqual(currv[i], n));
@@ -4163,7 +4163,8 @@ void TheoryStrings::checkNormalFormsDeq()
         {
           Trace("strings-solve") << "- Verify disequalities are processed for "
                                  << cols[i][0] << ", normal form : ";
-          printConcat(getNormalForm(cols[i][0]).d_nf, "strings-solve");
+          utils::printConcatTrace(getNormalForm(cols[i][0]).d_nf,
+                                  "strings-solve");
           Trace("strings-solve")
               << "... #eql = " << cols[i].size() << std::endl;
         }
@@ -4184,9 +4185,11 @@ void TheoryStrings::checkNormalFormsDeq()
                 if (Trace.isOn("strings-solve"))
                 {
                   Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
-                  printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
+                  utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf,
+                                          "strings-solve");
                   Trace("strings-solve") << " against " << cols[i][k] << " ";
-                  printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
+                  utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf,
+                                          "strings-solve");
                   Trace("strings-solve") << "..." << std::endl;
                 }
                 processDeq(cols[i][j], cols[i][k]);
@@ -4359,13 +4362,6 @@ void TheoryStrings::checkCardinality() {
   Trace("strings-card") << "...end check cardinality" << std::endl;
 }
 
-void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
-  for( unsigned i=0; i<n.size(); i++ ){
-    if( i>0 ) Trace(c) << " ++ ";
-    Trace(c) << n[i];
-  }
-}
-
 
 //// Finite Model Finding
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8e2af8434..b9e994fb5 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -615,10 +615,6 @@ private:
    */
   void registerTerm(Node n, int effort);
 
- protected:
-
-  void printConcat(std::vector<Node>& n, const char* c);
-
   // Symbolic Regular Expression
  private:
   /** regular expression solver module */
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 03c2419c4..a564c82e1 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -225,6 +225,25 @@ void getRegexpComponents(Node r, std::vector<Node>& result)
   }
 }
 
+void printConcat(std::ostream& out, std::vector<Node>& n)
+{
+  for (unsigned i = 0, nsize = n.size(); i < nsize; i++)
+  {
+    if (i > 0)
+    {
+      out << " ++ ";
+    }
+    out << n[i];
+  }
+}
+
+void printConcatTrace(std::vector<Node>& n, const char* c)
+{
+  std::stringstream ss;
+  printConcat(ss, n);
+  Trace(c) << ss.str();
+}
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 2c84bd516..ccdac8edf 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -131,6 +131,11 @@ bool isSimpleRegExp(Node r);
  */
 void getRegexpComponents(Node r, std::vector<Node>& result);
 
+/** Print the vector n as a concatentation term on output stream out */
+void printConcat(std::ostream& out, std::vector<Node>& n);
+/** Print the vector n as a concatentation term on trace given by c */
+void printConcatTrace(std::vector<Node>& n, const char* c);
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory