1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
/********************* */
/*! \file word.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Utility functions for words.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__WORD_H
#define CVC4__THEORY__STRINGS__WORD_H
#include <vector>
#include "expr/node.h"
#include "expr/type_node.h"
namespace CVC4 {
namespace theory {
namespace strings {
// ------------------------------ for words (string or sequence constants)
class Word
{
public:
/** make empty constant of type tn */
static Node mkEmptyWord(TypeNode tn);
/** make empty constant of kind k */
static Node mkEmptyWord(Kind k);
/** make word from constants in (non-empty) vector vec */
static Node mkWord(const std::vector<Node>& xs);
/** Return the length of word x */
static size_t getLength(TNode x);
/** Return true if x is empty */
static bool isEmpty(TNode x);
/** string compare
*
* Returns true if x is equal to y for their first n characters.
* If n is larger than the length of x or y, this method returns
* true if and only if x is equal to y.
*/
static bool strncmp(TNode x, TNode y, std::size_t n);
/** reverse string compare
*
* Returns true if x is equal to y for their last n characters.
* If n is larger than the length of tx or y, this method returns
* true if and only if x is equal to y.
*/
static bool rstrncmp(TNode x, TNode y, std::size_t n);
/** Return the first position y occurs in x, or std::string::npos otherwise */
static std::size_t find(TNode x, TNode y, std::size_t start = 0);
/**
* Return the first position y occurs in x searching from the end of x, or
* std::string::npos otherwise
*/
static std::size_t rfind(TNode x, TNode y, std::size_t start = 0);
/** Returns true if y is a prefix of x */
static bool hasPrefix(TNode x, TNode y);
/** Returns true if y is a suffix of x */
static bool hasSuffix(TNode x, TNode y);
/** Replace the first occurrence of y in x with t */
static Node replace(TNode x, TNode y, TNode t);
/** Return the substring/subsequence of x starting at index i */
static Node substr(TNode x, std::size_t i);
/** Return the substring/subsequence of x starting at index i with size at
* most
* j */
static Node substr(TNode x, std::size_t i, std::size_t j);
/** Return the prefix of x of size at most i */
static Node prefix(TNode x, std::size_t i);
/** Return the suffix of x of size at most i */
static Node suffix(TNode x, std::size_t i);
/**
* Checks if there is any overlap between word x and another word y. This
* corresponds to checking whether one string contains the other and whether a
* substring/subsequence of one is a prefix of the other and vice-versa.
*
* @param x The first string
* @param y The second string
* @return True if there is an overlap, false otherwise
*/
static bool noOverlapWith(TNode x, TNode y);
/** overlap
*
* if overlap returns m>0,
* then the maximal suffix of this string that is a prefix of y is of length
* m.
*
* For example, if x is "abcdef", then:
* x.overlap("defg") = 3
* x.overlap("ab") = 0
* x.overlap("d") = 0
* x.overlap("bcdefdef") = 5
*/
static std::size_t overlap(TNode x, TNode y);
/** reverse overlap
*
* if roverlap returns m>0,
* then the maximal prefix of this word that is a suffix of y is of length m.
*
* For example, if x is "abcdef", then:
* x.roverlap("aaabc") = 3
* x.roverlap("def") = 0
* x.roverlap("d") = 0
* x.roverlap("defabcde") = 5
*
* Notice that x.overlap(y) = y.roverlap(x)
*/
static std::size_t roverlap(TNode x, TNode y);
};
// ------------------------------ end for words (string or sequence constants)
} // namespace strings
} // namespace theory
} // namespace CVC4
#endif
|
