Convert more uses of strings to words (#4527)

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index df5263c45e6169f592533250e7145f51bca5b880..16c83de78019e3d302d8fe01fba877d13bffa957 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -33,7 +33,6 @@ BaseSolver::BaseSolver(context::Context* c,
                        InferenceManager& im)
     : d_state(s), d_im(im), d_congruent(c)
 {
-  d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
   d_false = NodeManager::currentNM()->mkConst(false);
   d_cardSize = utils::getAlphabetCardinality();
 }
@@ -50,7 +49,6 @@ void BaseSolver::checkInit()
   std::map<Kind, uint32_t> ncongruent;
   std::map<Kind, uint32_t> congruent;
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
-  Assert(d_state.getRepresentative(d_emptyString) == d_emptyString);
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
   while (!eqcs_i.isFinished())
   {
@@ -58,9 +56,11 @@ void BaseSolver::checkInit()
     TypeNode tn = eqc.getType();
     if (!tn.isRegExp())
     {
+      Node emps;
       if (tn.isString())
       {
         d_stringsEqc.push_back(eqc);
+        emps = Word::mkEmptyWord(tn);
       }
       Node var;
       eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
@@ -85,7 +85,7 @@ void BaseSolver::checkInit()
             if (d_congruent.find(n) == d_congruent.end())
             {
               std::vector<Node> c;
-              Node nc = d_termIndex[k].add(n, 0, d_state, d_emptyString, c);
+              Node nc = d_termIndex[k].add(n, 0, d_state, emps, c);
               if (nc != n)
               {
                 // check if we have inferred a new equality by removal of empty
@@ -101,14 +101,13 @@ void BaseSolver::checkInit()
                     for (unsigned t = 0; t < 2; t++)
                     {
                       Node nn = t == 0 ? nc : n;
-                      while (
-                          count[t] < nn.getNumChildren()
-                          && (nn[count[t]] == d_emptyString
-                              || d_state.areEqual(nn[count[t]], d_emptyString)))
+                      while (count[t] < nn.getNumChildren()
+                             && (nn[count[t]] == emps
+                                 || d_state.areEqual(nn[count[t]], emps)))
                       {
-                        if (nn[count[t]] != d_emptyString)
+                        if (nn[count[t]] != emps)
                         {
-                          exp.push_back(nn[count[t]].eqNode(d_emptyString));
+                          exp.push_back(nn[count[t]].eqNode(emps));
                         }
                         count[t]++;
                       }
@@ -160,11 +159,11 @@ void BaseSolver::checkInit()
                   bool foundNEmpty = false;
                   for (const Node& nnc : n)
                   {
-                    if (d_state.areEqual(nnc, d_emptyString))
+                    if (d_state.areEqual(nnc, emps))
                     {
-                      if (nnc != d_emptyString)
+                      if (nnc != emps)
                       {
-                        exp.push_back(nnc.eqNode(d_emptyString));
+                        exp.push_back(nnc.eqNode(emps));
                       }
                     }
                     else
@@ -293,10 +292,11 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
       while (count < n.getNumChildren())
       {
         // Add explanations for the empty children
+        Node emps;
         while (count < n.getNumChildren()
-               && d_state.areEqual(n[count], d_emptyString))
+               && d_state.isEqualEmptyWord(n[count], emps))
         {
-          d_im.addToExplanation(n[count], d_emptyString, exp);
+          d_im.addToExplanation(n[count], emps, exp);
           count++;
         }
         if (count < n.getNumChildren())

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index aa85d1056769b6c90ef1ce3b2e50628ee5cd0a1d..2d2ec0af0cab30f87af1f3511023e2556acd26e8 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -3044,10 +3044,9 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
     {
       res = nm->mkConst(String(std::string(u, 'A')));
     }
-    else
-    {
-      Unimplemented() << "canonicalStrForSymbolicLength for non-string";
-    }
+    // we could do this for sequences, but we need to be careful: some
+    // sorts do not permit values that the solver can handle (e.g. uninterpreted
+    // sorts and arrays).
   }
   else if (len.getKind() == PLUS)
   {
@@ -3075,6 +3074,10 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
     Integer intReps = ratReps.getNumerator();
 
     Node nRep = canonicalStrForSymbolicLength(len[1], stype);
+    if (nRep.isNull())
+    {
+      return Node::null();
+    }
     std::vector<Node> nRepChildren;
     utils::getConcat(nRep, nRepChildren);
     NodeBuilder<> concatBuilder(STRING_CONCAT);

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 1766a4b24c43a8b11f66fc8aa0bc05160aee50f9..622e919f790efb6911a880c960721ad687fcad61 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -264,6 +264,20 @@ Node SolverState::explainNonEmpty(Node s)
   return Node::null();
 }
 
+bool SolverState::isEqualEmptyWord(Node s, Node& emps)
+{
+  Node sr = getRepresentative(s);
+  if (sr.isConst())
+  {
+    if (Word::getLength(sr) == 0)
+    {
+      emps = sr;
+      return true;
+    }
+  }
+  return false;
+}
+
 void SolverState::setConflict() { d_conflict = true; }
 bool SolverState::isInConflict() const { return d_conflict; }
 

diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index bd5bb2926caf527f45d02e2714f1a7377766bbb7..d43c600f47365a713588c975585bb352b7c9f358 100644 (file)
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -135,6 +135,13 @@ class SolverState
    * in the equality engine.
    */
   Node explainNonEmpty(Node s);
+  /**
+   * Is equal empty word? Returns true if s is equal to the empty word (of
+   * its type). If this method returns true, it updates emps to be that word.
+   * This is an optimization so that the relevant empty word does not need to
+   * be constructed to check if s is equal to the empty word.
+   */
+  bool isEqualEmptyWord(Node s, Node& emps);
   /**
    * Get the above information for equivalence class eqc. If doMake is true,
    * we construct a new information class if one does not exist. The term eqc

diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 097964672c97bf9ba1bf778e6e020a5f1a2707cb..311eda5542167787b5f0159b02d8911675b91ce3 100644 (file)
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -905,7 +905,7 @@ Node StringsEntail::getStringOrEmpty(Node n)
 Node StringsEntail::inferEqsFromContains(Node x, Node y)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node emp = nm->mkConst(String(""));
+  Node emp = Word::mkEmptyWord(x.getType());
   Assert(x.getType() == y.getType());
   TypeNode stype = x.getType();