From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 25 Mar 2020 13:48:14 +0000 (-0500)
Subject:  Generalize more uses of string-specific functions (#4145)
X-Git-Tag: cvc5-1.0.0~3448
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b71f00097394c5f292abb002e31f49a07aff0b58;p=cvc5.git

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

Towards theory of sequences.
---

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 231c81bbf..10c5741fe 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1009,7 +1009,7 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
     {
       slv = getVarElimLitBv(lit, args, var);
     }
-    else if (tt.isString())
+    else if (tt.isStringLike())
     {
       slv = getVarElimLitString(lit, args, var);
     }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d33c72ede..f15b6780c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/strings/word.h"
 
 using namespace CVC4::kind;
 
@@ -405,11 +406,15 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
     ops.push_back(nm->mkConst(true));
     ops.push_back(nm->mkConst(false));
   }
-  else if (type.isString())
+  else if (type.isStringLike())
   {
-    ops.push_back(nm->mkConst(String("")));
-    // dummy character "A"
-    ops.push_back(nm->mkConst(String("A")));
+    ops.push_back(strings::Word::mkEmptyWord(type));
+    if (type.isString())
+    {
+      // Dummy character "A". This is not necessary for sequences which
+      // have the generic constructor seq.unit.
+      ops.push_back(nm->mkConst(String("A")));
+    }
   }
   else if (type.isArray() || type.isSet())
   {
@@ -449,7 +454,7 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
       {
         collectSygusGrammarTypesFor(range.getSetElementType(), types);
       }
-      else if (range.isString() )
+      else if (range.isStringLike())
       {
         // theory of strings shares the integer type
         TypeNode intType = NodeManager::currentNM()->integerType();
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 7f94130f3..cc920f1d7 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/strings/word.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -464,11 +465,11 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val)
       n = NodeManager::currentNM()->mkConst(false);
     }
   }
-  else if (tn.isString())
+  else if (tn.isStringLike())
   {
     if (val == 0)
     {
-      n = NodeManager::currentNM()->mkConst(::CVC4::String(""));
+      n = strings::Word::mkEmptyWord(tn);
     }
   }
   return n;
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 556ae28c3..876984503 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -719,11 +719,11 @@ void CoreSolver::getNormalForms(Node eqc,
   while( !eqc_i.isFinished() ){
     Node n = (*eqc_i);
     if( !d_bsolver.isCongruent(n) ){
-      if (n.getKind() == CONST_STRING || n.getKind() == STRING_CONCAT)
+      if (n.isConst() || n.getKind() == STRING_CONCAT)
       {
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
         NormalForm nf_curr;
-        if (n.getKind() == CONST_STRING)
+        if (n.isConst())
         {
           nf_curr.init(n);
         }
@@ -803,8 +803,7 @@ void CoreSolver::getNormalForms(Node eqc,
         }
         //if not equal to self
         std::vector<Node>& currv = nf_curr.d_nf;
-        if (currv.size() > 1
-            || (currv.size() == 1 && currv[0].getKind() == CONST_STRING))
+        if (currv.size() > 1 || (currv.size() == 1 && currv[0].isConst()))
         {
           // if in a build with assertions, check that normal form is acyclic
           if (Configuration::isAssertionBuild())
@@ -1082,9 +1081,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       d_im.sendInference(lenExp, eq, Inference::N_UNIFY);
       break;
     }
-    else if ((x.getKind() != CONST_STRING && index == nfiv.size() - rproc - 1)
-             || (y.getKind() != CONST_STRING
-                 && index == nfjv.size() - rproc - 1))
+    else if ((!x.isConst() && index == nfiv.size() - rproc - 1)
+             || (!y.isConst() && index == nfjv.size() - rproc - 1))
     {
       // We have reached the last component in one of the normal forms and it
       // is not a constant. Thus, the last component must be equal to the
@@ -1253,7 +1251,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       NormalForm& nfnc = x.isConst() ? nfj : nfi;
       const std::vector<Node>& nfncv = nfnc.d_nf;
       Node nc = nfncv[index];
-      Assert(nc.getKind() != CONST_STRING) << "Other string is not constant.";
+      Assert(!nc.isConst()) << "Other string is not constant.";
       Assert(nc.getKind() != STRING_CONCAT) << "Other string is not CONCAT.";
       if (!ee->areDisequal(nc, d_emptyString, true))
       {
@@ -1391,8 +1389,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     //
     // E.g. x ++ ... = y ++ ... ---> (x = y ++ k) v (y = x ++ k)
     Assert(d_state.areDisequal(xLenTerm, yLenTerm));
-    Assert(x.getKind() != CONST_STRING);
-    Assert(y.getKind() != CONST_STRING);
+    Assert(!x.isConst());
+    Assert(!y.isConst());
 
     int32_t lentTestSuccess = -1;
     Node lentTestExp;
@@ -1404,7 +1402,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       {
         Node t = e == 0 ? x : y;
         // do not infer constants are larger than variables
-        if (t.getKind() != CONST_STRING)
+        if (!t.isConst())
         {
           Node lt1 = e == 0 ? xLenTerm : yLenTerm;
           Node lt2 = e == 0 ? yLenTerm : xLenTerm;
@@ -1745,18 +1743,18 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
         Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
         if (!d_state.areEqual(i, j))
         {
-          Assert(i.getKind() != kind::CONST_STRING
-                 || j.getKind() != kind::CONST_STRING);
+          Assert(!i.isConst() || !j.isConst());
           std::vector< Node > lexp;
           Node li = d_state.getLength(i, lexp);
           Node lj = d_state.getLength(j, lexp);
           if (d_state.areDisequal(li, lj))
           {
-            if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
+            if (i.isConst() || j.isConst())
+            {
               //check if empty
-              Node const_k = i.getKind() == kind::CONST_STRING ? i : j;
-              Node nconst_k = i.getKind() == kind::CONST_STRING ? j : i;
-              Node lnck = i.getKind() == kind::CONST_STRING ? lj : li;
+              Node const_k = i.isConst() ? i : j;
+              Node nconst_k = i.isConst() ? j : i;
+              Node lnck = i.isConst() ? lj : li;
               if( !ee->areDisequal( nconst_k, d_emptyString, true ) ){
                 Node eq = nconst_k.eqNode( d_emptyString );
                 Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
@@ -1941,7 +1939,8 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >&
       Trace("strings-solve-debug")  << "...Processing(QED) " << i << " " << j << std::endl;
       if (!d_state.areEqual(i, j))
       {
-        if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
+        if (i.isConst() && j.isConst())
+        {
           size_t lenI = Word::getLength(i);
           size_t lenJ = Word::getLength(j);
           unsigned int len_short = lenI < lenJ ? lenI : lenJ;
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index ab6d473bd..4e9b0f8cd 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -44,13 +44,13 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
                                        << " post=" << isSuf << std::endl;
     Node prevC = utils::getConstantEndpoint(prev, isSuf);
     Assert(!prevC.isNull());
-    Assert(prevC.getKind() == CONST_STRING);
+    Assert(prevC.isConst());
     if (c.isNull())
     {
       c = utils::getConstantEndpoint(t, isSuf);
       Assert(!c.isNull());
     }
-    Assert(c.getKind() == CONST_STRING);
+    Assert(c.isConst());
     bool conflict = false;
     // if the constant prefixes are different
     if (c != prevC)
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index c586df6dd..6a3209344 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -645,7 +645,7 @@ Node ExtfSolver::getCurrentSubstitutionFor(int effort,
   {
     return c;
   }
-  else if (effort >= 1 && n.getType().isString())
+  else if (effort >= 1 && n.getType().isStringLike())
   {
     Assert(effort < 3);
     // normal forms
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;
diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 7a2323d89..4dd273eff 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -28,7 +28,7 @@ namespace strings {
 
 void NormalForm::init(Node base)
 {
-  Assert(base.getType().isString());
+  Assert(base.getType().isStringLike());
   Assert(base.getKind() != STRING_CONCAT);
   d_base = base;
   d_nf.clear();
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 200d7a734..716634d5f 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -400,7 +400,7 @@ Node SequencesRewriter::rewriteEqualityExt(Node node)
   {
     return rewriteArithEqualityExt(node);
   }
-  if (node[0].getType().isString())
+  if (node[0].getType().isStringLike())
   {
     return rewriteStrEqualityExt(node);
   }
@@ -409,7 +409,7 @@ Node SequencesRewriter::rewriteEqualityExt(Node node)
 
 Node SequencesRewriter::rewriteStrEqualityExt(Node node)
 {
-  Assert(node.getKind() == EQUAL && node[0].getType().isString());
+  Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
   TypeNode stype = node[0].getType();
 
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index a38bf2c50..30acba9fd 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -108,7 +108,7 @@ void SolverState::eqNotifyNewClass(TNode t)
       ei->d_codeTerm = t[0];
     }
   }
-  else if (k == CONST_STRING)
+  else if (t.isConst())
   {
     EqcInfo* ei = getOrMakeEqcInfo(t);
     ei->d_prefixC = t;
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index 8ca6d2de1..02af3949e 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -40,7 +40,7 @@ StringsFmf::~StringsFmf() {}
 
 void StringsFmf::preRegisterTerm(TNode n)
 {
-  if (!n.getType().isString())
+  if (!n.getType().isStringLike())
   {
     return;
   }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1006076d5..83f0159b5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -700,7 +700,8 @@ void TheoryStrings::check(Effort e) {
         Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
         while( !eqcs2_i.isFinished() ){
           Node eqc = (*eqcs2_i);
-          bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
+          bool print = (t == 0 && eqc.getType().isStringLike())
+                       || (t == 1 && !eqc.getType().isStringLike());
           if (print) {
             eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
             Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
@@ -907,7 +908,9 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   if( atom.getKind()==kind::EQUAL ){
     Trace("strings-pending-debug") << "  Register term" << std::endl;
     for( unsigned j=0; j<2; j++ ) {
-      if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
+      if (!d_equalityEngine.hasTerm(atom[j])
+          && atom[j].getType().isStringLike())
+      {
         registerTerm( atom[j], 0 );
       }
     }
@@ -1047,7 +1050,7 @@ void TheoryStrings::registerTerm(Node n, int effort)
 {
   TypeNode tn = n.getType();
   bool do_register = true;
-  if (!tn.isString())
+  if (!tn.isStringLike())
   {
     if (options::stringEagerLen())
     {
@@ -1070,7 +1073,7 @@ void TheoryStrings::registerTerm(Node n, int effort)
   NodeManager* nm = NodeManager::currentNM();
   Debug("strings-register") << "TheoryStrings::registerTerm() " << n
                             << ", effort = " << effort << std::endl;
-  if (tn.isString())
+  if (tn.isStringLike())
   {
     // register length information:
     //  for variables, split on empty vs positive length
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 6abb57504..7ef31a92a 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -291,7 +291,8 @@ public:
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
         }
-        if( (*it).getKind() != kind::CONST_STRING ) {
+        if (!(*it).isConst())
+        {
           throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
         }
         if( (*it).getConst<String>().size() != 1 ) {