GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/sequences_rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sequences_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Yoni Zohar
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 Rewriter for the theory of strings and sequences
13
 **
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H
19
#define CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H
20
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "theory/strings/rewrites.h"
25
#include "theory/strings/sequences_stats.h"
26
#include "theory/strings/strings_entail.h"
27
#include "theory/theory_rewriter.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace strings {
32
33
9274
class SequencesRewriter : public TheoryRewriter
34
{
35
 public:
36
  SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics);
37
38
 protected:
39
  /** rewrite regular expression concatenation
40
   *
41
   * This is the entry point for post-rewriting applications of re.++.
42
   * Returns the rewritten form of node.
43
   */
44
  Node rewriteConcatRegExp(TNode node);
45
  /** rewrite regular expression star
46
   *
47
   * This is the entry point for post-rewriting applications of re.*.
48
   * Returns the rewritten form of node.
49
   */
50
  Node rewriteStarRegExp(TNode node);
51
  /** rewrite regular expression intersection/union
52
   *
53
   * This is the entry point for post-rewriting applications of re.inter and
54
   * re.union. Returns the rewritten form of node.
55
   */
56
  Node rewriteAndOrRegExp(TNode node);
57
  /** rewrite regular expression loop
58
   *
59
   * This is the entry point for post-rewriting applications of re.loop.
60
   * Returns the rewritten form of node.
61
   */
62
  Node rewriteLoopRegExp(TNode node);
63
  /** rewrite regular expression repeat
64
   *
65
   * This is the entry point for post-rewriting applications of re.repeat.
66
   * Returns the rewritten form of node.
67
   */
68
  Node rewriteRepeatRegExp(TNode node);
69
  /** rewrite regular expression option
70
   *
71
   * This is the entry point for post-rewriting applications of re.opt.
72
   * Returns the rewritten form of node.
73
   */
74
  Node rewriteOptionRegExp(TNode node);
75
  /** rewrite regular expression plus
76
   *
77
   * This is the entry point for post-rewriting applications of re.+.
78
   * Returns the rewritten form of node.
79
   */
80
  Node rewritePlusRegExp(TNode node);
81
  /** rewrite regular expression difference
82
   *
83
   * This is the entry point for post-rewriting applications of re.diff.
84
   * Returns the rewritten form of node.
85
   */
86
  Node rewriteDifferenceRegExp(TNode node);
87
  /** rewrite regular expression range
88
   *
89
   * This is the entry point for post-rewriting applications of re.range.
90
   * Returns the rewritten form of node.
91
   */
92
  Node rewriteRangeRegExp(TNode node);
93
94
  /** rewrite regular expression membership
95
   *
96
   * This is the entry point for post-rewriting applications of str.in.re
97
   * Returns the rewritten form of node.
98
   */
99
  Node rewriteMembership(TNode node);
100
101
  /** rewrite string equality extended
102
   *
103
   * This method returns a formula that is equivalent to the equality between
104
   * two strings s = t, given by node. It is called by rewriteEqualityExt.
105
   */
106
  Node rewriteStrEqualityExt(Node node);
107
  /** rewrite arithmetic equality extended
108
   *
109
   * This method returns a formula that is equivalent to the equality between
110
   * two arithmetic string terms s = t, given by node. t is called by
111
   * rewriteEqualityExt.
112
   */
113
  Node rewriteArithEqualityExt(Node node);
114
  /**
115
   * Called when node rewrites to ret.
116
   *
117
   * The rewrite r indicates the justification for the rewrite, which is printed
118
   * by this function for debugging.
119
   *
120
   * If node is not an equality and ret is an equality, this method applies
121
   * an additional rewrite step (rewriteEqualityExt) that performs
122
   * additional rewrites on ret, after which we return the result of this call.
123
   * Otherwise, this method simply returns ret.
124
   */
125
  Node returnRewrite(Node node, Node ret, Rewrite r);
126
127
 public:
128
  RewriteResponse postRewrite(TNode node) override;
129
  RewriteResponse preRewrite(TNode node) override;
130
131
  /** rewrite equality
132
   *
133
   * This method returns a formula that is equivalent to the equality between
134
   * two strings s = t, given by node. The result of rewrite is one of
135
   * { s = t, t = s, true, false }.
136
   */
137
  Node rewriteEquality(Node node);
138
  /** rewrite equality extended
139
   *
140
   * This method returns a formula that is equivalent to the equality between
141
   * two terms s = t, given by node, where s and t are terms in the signature
142
   * of the theory of strings. Notice that s and t may be of string type or
143
   * of Int type.
144
   *
145
   * Specifically, this function performs rewrites whose conclusion is not
146
   * necessarily one of { s = t, t = s, true, false }.
147
   */
148
  Node rewriteEqualityExt(Node node) override;
149
  /** rewrite string length
150
   * This is the entry point for post-rewriting terms node of the form
151
   *   str.len( t )
152
   * Returns the rewritten form of node.
153
   */
154
  Node rewriteLength(Node node);
155
  /** rewrite concat
156
   * This is the entry point for post-rewriting terms node of the form
157
   *   str.++( t1, .., tn )
158
   * Returns the rewritten form of node.
159
   */
160
  Node rewriteConcat(Node node);
161
  /** rewrite character at
162
   * This is the entry point for post-rewriting terms node of the form
163
   *   str.charat( s, i1 )
164
   * Returns the rewritten form of node.
165
   */
166
  Node rewriteCharAt(Node node);
167
  /** rewrite substr
168
   * This is the entry point for post-rewriting terms node of the form
169
   *   str.substr( s, i1, i2 )
170
   * Returns the rewritten form of node.
171
   */
172
  Node rewriteSubstr(Node node);
173
  /** rewrite update
174
   * This is the entry point for post-rewriting terms node of the form
175
   *   str.update( s, i1, i2 )
176
   * Returns the rewritten form of node.
177
   */
178
  Node rewriteUpdate(Node node);
179
  /** rewrite contains
180
   * This is the entry point for post-rewriting terms node of the form
181
   *   str.contains( t, s )
182
   * Returns the rewritten form of node.
183
   *
184
   * For details on some of the basic rewrites done in this function, see Figure
185
   * 7 of Reynolds et al "Scaling Up DPLL(T) String Solvers Using
186
   * Context-Dependent Rewriting", CAV 2017.
187
   */
188
  Node rewriteContains(Node node);
189
  /** rewrite indexof
190
   * This is the entry point for post-rewriting terms n of the form
191
   *   str.indexof( s, t, n )
192
   * Returns the rewritten form of node.
193
   */
194
  Node rewriteIndexof(Node node);
195
  /** rewrite replace
196
   * This is the entry point for post-rewriting terms n of the form
197
   *   str.replace( s, t, r )
198
   * Returns the rewritten form of node.
199
   */
200
  Node rewriteReplace(Node node);
201
  /** rewrite replace all
202
   * This is the entry point for post-rewriting terms n of the form
203
   *   str.replaceall( s, t, r )
204
   * Returns the rewritten form of node.
205
   */
206
  Node rewriteReplaceAll(Node node);
207
  /** rewrite replace internal
208
   *
209
   * This method implements rewrite rules that apply to both str.replace and
210
   * str.replaceall. If it returns a non-null ret, then node rewrites to ret.
211
   */
212
  Node rewriteReplaceInternal(Node node);
213
  /** rewrite regular expression replace
214
   *
215
   * This method implements rewrite rules that apply to terms of the form
216
   * str.replace_re(s, r, t).
217
   *
218
   * @param node The node to rewrite
219
   * @return The rewritten node
220
   */
221
  Node rewriteReplaceRe(Node node);
222
  /** rewrite regular expression replace
223
   *
224
   * This method implements rewrite rules that apply to terms of the form
225
   * str.replace_re_all(s, r, t).
226
   *
227
   * @param node The node to rewrite
228
   * @return The rewritten node
229
   */
230
  Node rewriteReplaceReAll(Node node);
231
  /**
232
   * Returns the first, shortest sequence in n that matches r.
233
   *
234
   * @param n The constant string or sequence to search in.
235
   * @param r The regular expression to search for.
236
   * @return A pair holding the start position and the end position of the
237
   *         match or a pair of string::npos if r does not appear in n.
238
   */
239
  std::pair<size_t, size_t> firstMatch(Node n, Node r);
240
  /** rewrite string reverse
241
   *
242
   * This is the entry point for post-rewriting terms n of the form
243
   *   str.rev( s )
244
   * Returns the rewritten form of node.
245
   */
246
  Node rewriteStrReverse(Node node);
247
  /** rewrite prefix/suffix
248
   * This is the entry point for post-rewriting terms n of the form
249
   *   str.prefixof( s, t ) / str.suffixof( s, t )
250
   * Returns the rewritten form of node.
251
   */
252
  Node rewritePrefixSuffix(Node node);
253
254
  /** rewrite str.to_code
255
   * This is the entry point for post-rewriting terms n of the form
256
   *   str.to_code( t )
257
   * Returns the rewritten form of node.
258
   */
259
  Node rewriteStringToCode(Node node);
260
  /** rewrite seq.unit
261
   * This is the entry point for post-rewriting terms n of the form
262
   *   seq.unit( t )
263
   * Returns the rewritten form of node.
264
   */
265
  Node rewriteSeqUnit(Node node);
266
267
  /** rewrite seq.nth
268
   * This is the entry point for post-rewriting terms n of the form
269
   *   seq.nth(s, i)
270
   * Returns the rewritten form of node.
271
   */
272
  Node rewriteSeqNth(Node node);
273
274
  /** length preserving rewrite
275
   *
276
   * Given input n, this returns a string n' whose length is equivalent to n.
277
   * We apply certain normalizations to n', such as replacing all constants
278
   * that are not relevant to length by "A".
279
   */
280
  static Node lengthPreserveRewrite(Node n);
281
282
  /**
283
   * Given a symbolic length n, returns the canonical string (of type stype)
284
   * for that length. For example if n is constant, this function returns a
285
   * string consisting of "A" repeated n times. Returns the null node if no such
286
   * string exists.
287
   */
288
  static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
289
290
  /** Reference to the rewriter statistics. */
291
  IntegralHistogramStat<Rewrite>* d_statistics;
292
293
  /** Instance of the entailment checker for strings. */
294
  StringsEntail d_stringsEntail;
295
}; /* class SequencesRewriter */
296
297
}  // namespace strings
298
}  // namespace theory
299
}  // namespace CVC4
300
301
#endif /* CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H */