src/theory/strings/word.cpp

   1 /*********************                                                        */
   2 /*! \file word.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of utility functions for words.
  13  **/
  14
  15 #include "theory/strings/word.h"
  16
  17 #include "expr/sequence.h"
  18 #include "util/string.h"
  19
  20 using namespace cvc5::kind;
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace strings {
  25
  26 Node Word::mkEmptyWord(TypeNode tn)
  27 {
  28   if (tn.isString())
  29   {
  30     std::vector<unsigned> vec;
  31     return NodeManager::currentNM()->mkConst(String(vec));
  32   }
  33   else if (tn.isSequence())
  34   {
  35     std::vector<Node> seq;
  36     return NodeManager::currentNM()->mkConst(
  37         Sequence(tn.getSequenceElementType(), seq));
  38   }
  39   Unimplemented();
  40   return Node::null();
  41 }
  42
  43 Node Word::mkWordFlatten(const std::vector<Node>& xs)
  44 {
  45   Assert(!xs.empty());
  46   NodeManager* nm = NodeManager::currentNM();
  47   Kind k = xs[0].getKind();
  48   if (k == CONST_STRING)
  49   {
  50     std::vector<unsigned> vec;
  51     for (TNode x : xs)
  52     {
  53       Assert(x.getKind() == CONST_STRING);
  54       String sx = x.getConst<String>();
  55       const std::vector<unsigned>& vecc = sx.getVec();
  56       vec.insert(vec.end(), vecc.begin(), vecc.end());
  57     }
  58     return nm->mkConst(String(vec));
  59   }
  60   else if (k == CONST_SEQUENCE)
  61   {
  62     std::vector<Node> seq;
  63     TypeNode tn = xs[0].getType();
  64     for (TNode x : xs)
  65     {
  66       Assert(x.getType() == tn);
  67       const Sequence& sx = x.getConst<Sequence>();
  68       const std::vector<Node>& vecc = sx.getVec();
  69       seq.insert(seq.end(), vecc.begin(), vecc.end());
  70     }
  71     return NodeManager::currentNM()->mkConst(
  72         Sequence(tn.getSequenceElementType(), seq));
  73   }
  74   Unimplemented();
  75   return Node::null();
  76 }
  77
  78 size_t Word::getLength(TNode x)
  79 {
  80   Kind k = x.getKind();
  81   if (k == CONST_STRING)
  82   {
  83     return x.getConst<String>().size();
  84   }
  85   else if (k == CONST_SEQUENCE)
  86   {
  87     return x.getConst<Sequence>().size();
  88   }
  89   Unimplemented() << "Word::getLength on " << x;
  90   return 0;
  91 }
  92
  93 std::vector<Node> Word::getChars(TNode x)
  94 {
  95   Kind k = x.getKind();
  96   std::vector<Node> ret;
  97   NodeManager* nm = NodeManager::currentNM();
  98   if (k == CONST_STRING)
  99   {
 100     std::vector<unsigned> ccVec;
 101     const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
 102     for (unsigned chVal : cvec)
 103     {
 104       ccVec.clear();
 105       ccVec.push_back(chVal);
 106       Node ch = nm->mkConst(String(ccVec));
 107       ret.push_back(ch);
 108     }
 109     return ret;
 110   }
 111   else if (k == CONST_SEQUENCE)
 112   {
 113     TypeNode t = x.getConst<Sequence>().getType();
 114     const Sequence& sx = x.getConst<Sequence>();
 115     const std::vector<Node>& vec = sx.getVec();
 116     for (const Node& v : vec)
 117     {
 118       ret.push_back(nm->mkConst(Sequence(t, {v})));
 119     }
 120     return ret;
 121   }
 122   Unimplemented();
 123   return ret;
 124 }
 125
 126 bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
 127
 128 bool Word::strncmp(TNode x, TNode y, std::size_t n)
 129 {
 130   Kind k = x.getKind();
 131   if (k == CONST_STRING)
 132   {
 133     Assert(y.getKind() == CONST_STRING);
 134     String sx = x.getConst<String>();
 135     String sy = y.getConst<String>();
 136     return sx.strncmp(sy, n);
 137   }
 138   else if (k == CONST_SEQUENCE)
 139   {
 140     Assert(y.getKind() == CONST_SEQUENCE);
 141     const Sequence& sx = x.getConst<Sequence>();
 142     const Sequence& sy = y.getConst<Sequence>();
 143     return sx.strncmp(sy, n);
 144   }
 145   Unimplemented();
 146   return false;
 147 }
 148
 149 bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
 150 {
 151   Kind k = x.getKind();
 152   if (k == CONST_STRING)
 153   {
 154     Assert(y.getKind() == CONST_STRING);
 155     String sx = x.getConst<String>();
 156     String sy = y.getConst<String>();
 157     return sx.rstrncmp(sy, n);
 158   }
 159   else if (k == CONST_SEQUENCE)
 160   {
 161     Assert(y.getKind() == CONST_SEQUENCE);
 162     const Sequence& sx = x.getConst<Sequence>();
 163     const Sequence& sy = y.getConst<Sequence>();
 164     return sx.rstrncmp(sy, n);
 165   }
 166   Unimplemented();
 167   return false;
 168 }
 169
 170 std::size_t Word::find(TNode x, TNode y, std::size_t start)
 171 {
 172   Kind k = x.getKind();
 173   if (k == CONST_STRING)
 174   {
 175     Assert(y.getKind() == CONST_STRING);
 176     String sx = x.getConst<String>();
 177     String sy = y.getConst<String>();
 178     return sx.find(sy, start);
 179   }
 180   else if (k == CONST_SEQUENCE)
 181   {
 182     Assert(y.getKind() == CONST_SEQUENCE);
 183     const Sequence& sx = x.getConst<Sequence>();
 184     const Sequence& sy = y.getConst<Sequence>();
 185     return sx.find(sy, start);
 186   }
 187   Unimplemented();
 188   return 0;
 189 }
 190
 191 std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
 192 {
 193   Kind k = x.getKind();
 194   if (k == CONST_STRING)
 195   {
 196     Assert(y.getKind() == CONST_STRING);
 197     String sx = x.getConst<String>();
 198     String sy = y.getConst<String>();
 199     return sx.rfind(sy, start);
 200   }
 201   else if (k == CONST_SEQUENCE)
 202   {
 203     Assert(y.getKind() == CONST_SEQUENCE);
 204     const Sequence& sx = x.getConst<Sequence>();
 205     const Sequence& sy = y.getConst<Sequence>();
 206     return sx.rfind(sy, start);
 207   }
 208   Unimplemented();
 209   return 0;
 210 }
 211
 212 bool Word::hasPrefix(TNode x, TNode y)
 213 {
 214   Kind k = x.getKind();
 215   if (k == CONST_STRING)
 216   {
 217     Assert(y.getKind() == CONST_STRING);
 218     String sx = x.getConst<String>();
 219     String sy = y.getConst<String>();
 220     return sx.hasPrefix(sy);
 221   }
 222   else if (k == CONST_SEQUENCE)
 223   {
 224     Assert(y.getKind() == CONST_SEQUENCE);
 225     const Sequence& sx = x.getConst<Sequence>();
 226     const Sequence& sy = y.getConst<Sequence>();
 227     return sx.hasPrefix(sy);
 228   }
 229   Unimplemented();
 230   return false;
 231 }
 232
 233 bool Word::hasSuffix(TNode x, TNode y)
 234 {
 235   Kind k = x.getKind();
 236   if (k == CONST_STRING)
 237   {
 238     Assert(y.getKind() == CONST_STRING);
 239     String sx = x.getConst<String>();
 240     String sy = y.getConst<String>();
 241     return sx.hasSuffix(sy);
 242   }
 243   else if (k == CONST_SEQUENCE)
 244   {
 245     Assert(y.getKind() == CONST_SEQUENCE);
 246     const Sequence& sx = x.getConst<Sequence>();
 247     const Sequence& sy = y.getConst<Sequence>();
 248     return sx.hasSuffix(sy);
 249   }
 250   Unimplemented();
 251   return false;
 252 }
 253
 254 Node Word::update(TNode x, std::size_t i, TNode t)
 255 {
 256   NodeManager* nm = NodeManager::currentNM();
 257   Kind k = x.getKind();
 258   if (k == CONST_STRING)
 259   {
 260     Assert(t.getKind() == CONST_STRING);
 261     String sx = x.getConst<String>();
 262     String st = t.getConst<String>();
 263     return nm->mkConst(String(sx.update(i, st)));
 264   }
 265   else if (k == CONST_SEQUENCE)
 266   {
 267     Assert(t.getKind() == CONST_SEQUENCE);
 268     const Sequence& sx = x.getConst<Sequence>();
 269     const Sequence& st = t.getConst<Sequence>();
 270     Sequence res = sx.update(i, st);
 271     return nm->mkConst(res);
 272   }
 273   Unimplemented();
 274   return Node::null();
 275 }
 276 Node Word::replace(TNode x, TNode y, TNode t)
 277 {
 278   NodeManager* nm = NodeManager::currentNM();
 279   Kind k = x.getKind();
 280   if (k == CONST_STRING)
 281   {
 282     Assert(y.getKind() == CONST_STRING);
 283     Assert(t.getKind() == CONST_STRING);
 284     String sx = x.getConst<String>();
 285     String sy = y.getConst<String>();
 286     String st = t.getConst<String>();
 287     return nm->mkConst(String(sx.replace(sy, st)));
 288   }
 289   else if (k == CONST_SEQUENCE)
 290   {
 291     Assert(y.getKind() == CONST_SEQUENCE);
 292     Assert(t.getKind() == CONST_SEQUENCE);
 293     const Sequence& sx = x.getConst<Sequence>();
 294     const Sequence& sy = y.getConst<Sequence>();
 295     const Sequence& st = t.getConst<Sequence>();
 296     Sequence res = sx.replace(sy, st);
 297     return nm->mkConst(res);
 298   }
 299   Unimplemented();
 300   return Node::null();
 301 }
 302 Node Word::substr(TNode x, std::size_t i)
 303 {
 304   NodeManager* nm = NodeManager::currentNM();
 305   Kind k = x.getKind();
 306   if (k == CONST_STRING)
 307   {
 308     String sx = x.getConst<String>();
 309     return nm->mkConst(String(sx.substr(i)));
 310   }
 311   else if (k == CONST_SEQUENCE)
 312   {
 313     const Sequence& sx = x.getConst<Sequence>();
 314     Sequence res = sx.substr(i);
 315     return nm->mkConst(res);
 316   }
 317   Unimplemented();
 318   return Node::null();
 319 }
 320 Node Word::substr(TNode x, std::size_t i, std::size_t j)
 321 {
 322   NodeManager* nm = NodeManager::currentNM();
 323   Kind k = x.getKind();
 324   if (k == CONST_STRING)
 325   {
 326     String sx = x.getConst<String>();
 327     return nm->mkConst(String(sx.substr(i, j)));
 328   }
 329   else if (k == CONST_SEQUENCE)
 330   {
 331     const Sequence& sx = x.getConst<Sequence>();
 332     Sequence res = sx.substr(i, j);
 333     return nm->mkConst(res);
 334   }
 335   Unimplemented();
 336   return Node::null();
 337 }
 338
 339 Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
 340
 341 Node Word::suffix(TNode x, std::size_t i)
 342 {
 343   NodeManager* nm = NodeManager::currentNM();
 344   Kind k = x.getKind();
 345   if (k == CONST_STRING)
 346   {
 347     String sx = x.getConst<String>();
 348     return nm->mkConst(String(sx.suffix(i)));
 349   }
 350   else if (k == CONST_SEQUENCE)
 351   {
 352     const Sequence& sx = x.getConst<Sequence>();
 353     Sequence res = sx.suffix(i);
 354     return nm->mkConst(res);
 355   }
 356   Unimplemented();
 357   return Node::null();
 358 }
 359
 360 bool Word::noOverlapWith(TNode x, TNode y)
 361 {
 362   Kind k = x.getKind();
 363   if (k == CONST_STRING)
 364   {
 365     Assert(y.getKind() == CONST_STRING);
 366     String sx = x.getConst<String>();
 367     String sy = y.getConst<String>();
 368     return sx.noOverlapWith(sy);
 369   }
 370   else if (k == CONST_SEQUENCE)
 371   {
 372     Assert(y.getKind() == CONST_SEQUENCE);
 373     const Sequence& sx = x.getConst<Sequence>();
 374     const Sequence& sy = y.getConst<Sequence>();
 375     return sx.noOverlapWith(sy);
 376   }
 377   Unimplemented();
 378   return false;
 379 }
 380
 381 std::size_t Word::overlap(TNode x, TNode y)
 382 {
 383   Kind k = x.getKind();
 384   if (k == CONST_STRING)
 385   {
 386     Assert(y.getKind() == CONST_STRING);
 387     String sx = x.getConst<String>();
 388     String sy = y.getConst<String>();
 389     return sx.overlap(sy);
 390   }
 391   else if (k == CONST_SEQUENCE)
 392   {
 393     Assert(y.getKind() == CONST_SEQUENCE);
 394     const Sequence& sx = x.getConst<Sequence>();
 395     const Sequence& sy = y.getConst<Sequence>();
 396     return sx.overlap(sy);
 397   }
 398   Unimplemented();
 399   return 0;
 400 }
 401
 402 std::size_t Word::roverlap(TNode x, TNode y)
 403 {
 404   Kind k = x.getKind();
 405   if (k == CONST_STRING)
 406   {
 407     Assert(y.getKind() == CONST_STRING);
 408     String sx = x.getConst<String>();
 409     String sy = y.getConst<String>();
 410     return sx.roverlap(sy);
 411   }
 412   else if (k == CONST_SEQUENCE)
 413   {
 414     Assert(y.getKind() == CONST_SEQUENCE);
 415     const Sequence& sx = x.getConst<Sequence>();
 416     const Sequence& sy = y.getConst<Sequence>();
 417     return sx.roverlap(sy);
 418   }
 419   Unimplemented();
 420   return 0;
 421 }
 422
 423 bool Word::isRepeated(TNode x)
 424 {
 425   Kind k = x.getKind();
 426   if (k == CONST_STRING)
 427   {
 428     return x.getConst<String>().isRepeated();
 429   }
 430   else if (k == CONST_SEQUENCE)
 431   {
 432     return x.getConst<Sequence>().isRepeated();
 433   }
 434   Unimplemented();
 435   return false;
 436 }
 437
 438 Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
 439 {
 440   Assert(x.isConst() && y.isConst());
 441   size_t lenA = getLength(x);
 442   size_t lenB = getLength(y);
 443   index = lenA <= lenB ? 1 : 0;
 444   size_t lenShort = index == 1 ? lenA : lenB;
 445   bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
 446   if (cmp)
 447   {
 448     Node l = index == 0 ? x : y;
 449     if (isRev)
 450     {
 451       size_t new_len = getLength(l) - lenShort;
 452       return substr(l, 0, new_len);
 453     }
 454     else
 455     {
 456       return substr(l, lenShort);
 457     }
 458   }
 459   // not the same prefix/suffix
 460   return Node::null();
 461 }
 462
 463 Node Word::reverse(TNode x)
 464 {
 465   NodeManager* nm = NodeManager::currentNM();
 466   Kind k = x.getKind();
 467   if (k == CONST_STRING)
 468   {
 469     String sx = x.getConst<String>();
 470     std::vector<unsigned> nvec = sx.getVec();
 471     std::reverse(nvec.begin(), nvec.end());
 472     return nm->mkConst(String(nvec));
 473   }
 474   else if (k == CONST_SEQUENCE)
 475   {
 476     const Sequence& sx = x.getConst<Sequence>();
 477     const std::vector<Node>& vecc = sx.getVec();
 478     std::vector<Node> vecr(vecc.begin(), vecc.end());
 479     std::reverse(vecr.begin(), vecr.end());
 480     Sequence res(sx.getType(), vecr);
 481     return nm->mkConst(res);
 482   }
 483   Unimplemented();
 484   return Node::null();
 485 }
 486
 487 }  // namespace strings
 488 }  // namespace theory
 489 }  // namespace cvc5