From 2e4e1d2d202ac048a2d808e907d6e6e61d002709 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 5 Apr 2020 01:52:37 -0500
Subject: [PATCH] Type-independent preregistration of empty word (#4205)

Also removes another instance of empty string in TheoryStrings for consistency sake.
---
 src/theory/strings/theory_strings.cpp | 40 ++++++++++++++++++---------
 src/theory/strings/theory_strings.h   | 10 +++++++
 2 files changed, 37 insertions(+), 13 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d74a0e9ca..92116582f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -75,6 +75,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics),
       d_pregistered_terms_cache(u),
       d_registered_terms_cache(u),
+      d_registeredTypesCache(u),
       d_functionsTerms(c),
       d_has_str_code(false),
       d_rewriter(&d_statistics.d_rewrites),
@@ -122,7 +123,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  d_emptyString = Word::mkEmptyWord(CONST_STRING);
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
@@ -654,12 +654,12 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
         nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
     Node k = nm->mkBoundVar(nm->stringType());
     Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
-    node = nm->mkNode(CHOICE,
-                      bvl,
-                      nm->mkNode(ITE,
-                                 cond,
-                                 t.eqNode(nm->mkNode(STRING_TO_CODE, k)),
-                                 k.eqNode(d_emptyString)));
+    Node emp = Word::mkEmptyWord(node.getType());
+    node = nm->mkNode(
+        CHOICE,
+        bvl,
+        nm->mkNode(
+            ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
   }
 
   return node;
@@ -674,12 +674,6 @@ void TheoryStrings::check(Effort e) {
 
   bool polarity;
   TNode atom;
-
-  if (!done() && !d_equalityEngine.hasTerm(d_emptyString))
-  {
-    preRegisterTerm( d_emptyString );
-  }
-
   // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
   Trace("strings-check-debug")
       << "Theory of strings, check : " << e << std::endl;
@@ -1089,6 +1083,8 @@ void TheoryStrings::registerTerm(Node n, int effort)
     return;
   }
   d_registered_terms_cache.insert(n);
+  // ensure the type is registered
+  registerType(tn);
   NodeManager* nm = NodeManager::currentNM();
   Debug("strings-register") << "TheoryStrings::registerTerm() " << n
                             << ", effort = " << effort << std::endl;
@@ -1130,6 +1126,24 @@ void TheoryStrings::registerTerm(Node n, int effort)
   }
 }
 
+void TheoryStrings::registerType(TypeNode tn)
+{
+  if (d_registeredTypesCache.find(tn) != d_registeredTypesCache.end())
+  {
+    return;
+  }
+  d_registeredTypesCache.insert(tn);
+  if (tn.isStringLike())
+  {
+    // preregister the empty word for the type
+    Node emp = Word::mkEmptyWord(tn);
+    if (!d_equalityEngine.hasTerm(emp))
+    {
+      preRegisterTerm(emp);
+    }
+  }
+}
+
 void TheoryStrings::checkRegisterTermsNormalForms()
 {
   const std::vector<Node>& seqc = d_bsolver.getStringEqc();
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5ae0ac7a9..84e0a0a00 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -103,6 +103,7 @@ class TheoryStrings : public Theory {
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
 
  public:
   TheoryStrings(context::Context* c, context::UserContext* u,
@@ -242,6 +243,8 @@ class TheoryStrings : public Theory {
   // preReg cache
   NodeSet d_pregistered_terms_cache;
   NodeSet d_registered_terms_cache;
+  /** The types that we have preregistered */
+  TypeNodeSet d_registeredTypesCache;
   std::vector< Node > d_empty_vec;
 private:
 
@@ -350,6 +353,13 @@ private:
    * effort, the call to this method does nothing.
    */
   void registerTerm(Node n, int effort);
+  /** Register type
+   *
+   * Ensures the theory solver is setup to handle string-like type tn. In
+   * particular, this includes:
+   * - Calling preRegisterTerm on the empty word for tn
+   */
+  void registerType(TypeNode tn);
 
   // Symbolic Regular Expression
  private:
-- 
2.30.2