src/theory/strings/word.h

   1 /*********************                                                        */
   2 /*! \file word.h
   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-2020 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 Utility functions for words.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__STRINGS__WORD_H
  18 #define CVC4__THEORY__STRINGS__WORD_H
  19
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23 #include "expr/type_node.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace strings {
  28
  29 // ------------------------------ for words (string or sequence constants)
  30 class Word
  31 {
  32  public:
  33   /** make empty constant of type tn */
  34   static Node mkEmptyWord(TypeNode tn);
  35
  36   /** make word from constants in (non-empty) vector vec */
  37   static Node mkWordFlatten(const std::vector<Node>& xs);
  38
  39   /** Return the length of word x */
  40   static size_t getLength(TNode x);
  41
  42   /** Get characters
  43    *
  44    * Given word x, this returns the vector of words of length one whose
  45    * concatenation is equivalent to x.
  46    */
  47   static std::vector<Node> getChars(TNode x);
  48
  49   /** Return true if x is empty */
  50   static bool isEmpty(TNode x);
  51
  52   /** string compare
  53    *
  54    * Returns true if x is equal to y for their first n characters.
  55    * If n is larger than the length of x or y, this method returns
  56    * true if and only if x is equal to y.
  57    */
  58   static bool strncmp(TNode x, TNode y, std::size_t n);
  59
  60   /** reverse string compare
  61    *
  62    * Returns true if x is equal to y for their last n characters.
  63    * If n is larger than the length of tx or y, this method returns
  64    * true if and only if x is equal to y.
  65    */
  66   static bool rstrncmp(TNode x, TNode y, std::size_t n);
  67
  68   /** Return the first position y occurs in x, or std::string::npos otherwise */
  69   static std::size_t find(TNode x, TNode y, std::size_t start = 0);
  70
  71   /**
  72    * Return the first position y occurs in x searching from the end of x, or
  73    * std::string::npos otherwise
  74    */
  75   static std::size_t rfind(TNode x, TNode y, std::size_t start = 0);
  76
  77   /** Returns true if y is a prefix of x */
  78   static bool hasPrefix(TNode x, TNode y);
  79
  80   /** Returns true if y is a suffix of x */
  81   static bool hasSuffix(TNode x, TNode y);
  82
  83   /** Replace the character at index n in x with t */
  84   static Node update(TNode x, std::size_t n, TNode t);
  85
  86   /** Replace the first occurrence of y in x with t */
  87   static Node replace(TNode x, TNode y, TNode t);
  88
  89   /** Return the substring/subsequence of x starting at index i */
  90   static Node substr(TNode x, std::size_t i);
  91
  92   /** Return the substring/subsequence of x starting at index i with size at
  93    * most
  94    * j */
  95   static Node substr(TNode x, std::size_t i, std::size_t j);
  96
  97   /** Return the prefix of x of size at most i */
  98   static Node prefix(TNode x, std::size_t i);
  99
 100   /** Return the suffix of x of size at most i */
 101   static Node suffix(TNode x, std::size_t i);
 102
 103   /**
 104    * Checks if there is any overlap between word x and another word y. This
 105    * corresponds to checking whether one string contains the other and whether a
 106    * substring/subsequence of one is a prefix of the other and vice-versa.
 107    *
 108    * @param x The first string
 109    * @param y The second string
 110    * @return True if there is an overlap, false otherwise
 111    */
 112   static bool noOverlapWith(TNode x, TNode y);
 113
 114   /** overlap
 115    *
 116    * if overlap returns m>0,
 117    * then the maximal suffix of this string that is a prefix of y is of length
 118    * m.
 119    *
 120    * For example, if x is "abcdef", then:
 121    * x.overlap("defg") = 3
 122    * x.overlap("ab") = 0
 123    * x.overlap("d") = 0
 124    * x.overlap("bcdefdef") = 5
 125    */
 126   static std::size_t overlap(TNode x, TNode y);
 127
 128   /** reverse overlap
 129    *
 130    * if roverlap returns m>0,
 131    * then the maximal prefix of this word that is a suffix of y is of length m.
 132    *
 133    * For example, if x is "abcdef", then:
 134    * x.roverlap("aaabc") = 3
 135    * x.roverlap("def") = 0
 136    * x.roverlap("d") = 0
 137    * x.roverlap("defabcde") = 5
 138    *
 139    * Notice that x.overlap(y) = y.roverlap(x)
 140    */
 141   static std::size_t roverlap(TNode x, TNode y);
 142   /** Return true if word x is a repetition of the same character */
 143   static bool isRepeated(TNode x);
 144   /** Split constant
 145    *
 146    * This returns the suffix remainder (resp. prefix remainder when isRev is
 147    * true) of words a and b, call it r, such that:
 148    * (1) a = b ++ r , or
 149    * (2) a ++ r = b
 150    * when isRev = false.  The argument index is set to 1 if we are in the second
 151    * case, and 0 otherwise.
 152    *
 153    * If a and b do not share a common prefix (resp. suffix), then this method
 154    * returns the null node.
 155    */
 156   static Node splitConstant(TNode x, TNode y, size_t& index, bool isRev);
 157   /** reverse
 158    *
 159    * Return the result of reversing x.
 160    */
 161   static Node reverse(TNode x);
 162 };
 163
 164 // ------------------------------ end for words (string or sequence constants)
 165
 166 }  // namespace strings
 167 }  // namespace theory
 168 }  // namespace CVC4
 169
 170 #endif