Generalize more uses of string-specific functions (#4145)

Towards theory of sequences.

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index eebad2274..e931c5c1a 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -20,6 +20,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -370,12 +371,13 @@ Node InferenceManager::getSymbolicDefinition(Node n,
 
 void InferenceManager::registerLength(Node n)
 {
+  Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
   // register length information:
   //  for variables, split on empty vs positive length
   //  for concat/const/replace, introduce proxy var and state length relation
   Node lsum;
-  if (n.getKind() != STRING_CONCAT && n.getKind() != CONST_STRING)
+  if (n.getKind() != STRING_CONCAT && !n.isConst())
   {
     Node lsumb = nm->mkNode(STRING_LENGTH, n);
     lsum = Rewriter::rewrite(lsumb);
@@ -422,9 +424,9 @@ void InferenceManager::registerLength(Node n)
     lsum = nm->mkNode(PLUS, nodeVec);
     lsum = Rewriter::rewrite(lsum);
   }
-  else if (n.getKind() == CONST_STRING)
+  else if (n.isConst())
   {
-    lsum = nm->mkConst(Rational(n.getConst<String>().size()));
+    lsum = nm->mkConst(Rational(Word::getLength(n)));
   }
   Assert(!lsum.isNull());
   d_proxyVarToLength[sk] = lsum;