Generalize more string-specific functions (#4152)

Towards theory of sequences.

Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field.

1 files changed, 7 insertions, 8 deletions

diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index 4e9b0f8cd..3c0dbc2a7 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/eqc_info.h"
 
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -59,10 +60,8 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
       Assert(!t.isConst() || !prev.isConst());
       Trace("strings-eager-pconf-debug")
           << "Check conflict constants " << prevC << ", " << c << std::endl;
-      const String& ps = prevC.getConst<String>();
-      const String& cs = c.getConst<String>();
-      unsigned pvs = ps.size();
-      unsigned cvs = cs.size();
+      size_t pvs = Word::getLength(prevC);
+      size_t cvs = Word::getLength(c);
       if (pvs == cvs || (pvs > cvs && t.isConst())
           || (cvs > pvs && prev.isConst()))
       {
@@ -73,15 +72,15 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
       }
       else
       {
-        const String& larges = pvs > cvs ? ps : cs;
-        const String& smalls = pvs > cvs ? cs : ps;
+        Node larges = pvs > cvs ? prevC : c;
+        Node smalls = pvs > cvs ? c : prevC;
         if (isSuf)
         {
-          conflict = !larges.hasSuffix(smalls);
+          conflict = !Word::hasSuffix(larges, smalls);
         }
         else
         {
-          conflict = !larges.hasPrefix(smalls);
+          conflict = !Word::hasPrefix(larges, smalls);
         }
       }
       if (!conflict && (pvs > cvs || prev.isConst()))