GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/sequence.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sequence.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-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 The sequence data type.
13
 **/
14
15
#include "cvc4_public.h"
16
17
#ifndef CVC4__EXPR__SEQUENCE_H
18
#define CVC4__EXPR__SEQUENCE_H
19
20
#include <memory>
21
#include <vector>
22
23
namespace CVC4 {
24
25
template <bool ref_count>
26
class NodeTemplate;
27
typedef NodeTemplate<true> Node;
28
class TypeNode;
29
30
/** The CVC4 sequence class
31
 *
32
 * This data structure is the domain of values for the sequence type.
33
 */
34
class Sequence
35
{
36
 public:
37
  /** constructors for Sequence
38
   *
39
   * Internally, a CVC4::Sequence is represented by a vector of Nodes (d_seq),
40
   * where each Node in this vector must be a constant.
41
   */
42
  Sequence() = default;
43
  explicit Sequence(const TypeNode& t, const std::vector<Node>& s);
44
  Sequence(const Sequence& seq);
45
46
  ~Sequence();
47
48
  Sequence& operator=(const Sequence& y);
49
50
  Sequence concat(const Sequence& other) const;
51
52
20908
  bool operator==(const Sequence& y) const { return cmp(y) == 0; }
53
  bool operator!=(const Sequence& y) const { return cmp(y) != 0; }
54
  bool operator<(const Sequence& y) const { return cmp(y) < 0; }
55
  bool operator>(const Sequence& y) const { return cmp(y) > 0; }
56
  bool operator<=(const Sequence& y) const { return cmp(y) <= 0; }
57
  bool operator>=(const Sequence& y) const { return cmp(y) >= 0; }
58
59
  bool strncmp(const Sequence& y, size_t n) const;
60
  bool rstrncmp(const Sequence& y, size_t n) const;
61
62
  /** is this the empty sequence? */
63
  bool empty() const;
64
  /** is less than or equal to sequence y */
65
  bool isLeq(const Sequence& y) const;
66
  /** Return the length of the sequence */
67
  size_t size() const;
68
69
  /** Return true if this sequence is a repetition of the same element */
70
  bool isRepeated() const;
71
72
  /**
73
   * Return the first position y occurs in this sequence, or std::string::npos
74
   * otherwise.
75
   */
76
  size_t find(const Sequence& y, size_t start = 0) const;
77
  /**
78
   * Return the first position y occurs in this sequence searching from the end,
79
   * or std::string::npos otherwise.
80
   */
81
  size_t rfind(const Sequence& y, size_t start = 0) const;
82
  /** Returns true if y is a prefix of this */
83
  bool hasPrefix(const Sequence& y) const;
84
  /** Returns true if y is a suffix of this */
85
  bool hasSuffix(const Sequence& y) const;
86
  /** Replace the character at index i in this sequence with t */
87
  Sequence update(size_t i, const Sequence& t) const;
88
  /** Replace the first occurrence of s in this sequence with t */
89
  Sequence replace(const Sequence& s, const Sequence& t) const;
90
  /** Return the subsequence of this sequence starting at index i */
91
  Sequence substr(size_t i) const;
92
  /**
93
   * Return the subsequence of this sequence starting at index i with size at
94
   * most j.
95
   */
96
  Sequence substr(size_t i, size_t j) const;
97
  /** Return the prefix of this sequence of size at most i */
98
42
  Sequence prefix(size_t i) const { return substr(0, i); }
99
  /** Return the suffix of this sequence of size at most i */
100
57
  Sequence suffix(size_t i) const { return substr(size() - i, i); }
101
102
  /**
103
   * Checks if there is any overlap between this sequence and another sequence.
104
   * This corresponds to checking whether one sequence contains the other and
105
   * whether a subsequence of one is a prefix of the other and vice-versa.
106
   *
107
   * @param y The other sequence
108
   * @return True if there is an overlap, false otherwise
109
   */
110
  bool noOverlapWith(const Sequence& y) const;
111
112
  /** sequence overlap
113
   *
114
   * if overlap returns m>0,
115
   * then the maximal suffix of this sequence that is a prefix of y is of length
116
   * m.
117
   *
118
   * For example, if x is "abcdef", then:
119
   * x.overlap("defg") = 3
120
   * x.overlap("ab") = 0
121
   * x.overlap("d") = 0
122
   * x.overlap("bcdefdef") = 5
123
   */
124
  size_t overlap(const Sequence& y) const;
125
  /** sequence reverse overlap
126
   *
127
   * if roverlap returns m>0,
128
   * then the maximal prefix of this sequence that is a suffix of y is of length
129
   * m.
130
   *
131
   * For example, if x is "abcdef", then:
132
   * x.roverlap("aaabc") = 3
133
   * x.roverlap("def") = 0
134
   * x.roverlap("d") = 0
135
   * x.roverlap("defabcde") = 5
136
   *
137
   * Notice that x.overlap(y) = y.roverlap(x)
138
   */
139
  size_t roverlap(const Sequence& y) const;
140
141
  /** get the element type of the sequence */
142
  const TypeNode& getType() const;
143
  /** get the internal Node representation of this sequence */
144
  const std::vector<Node>& getVec() const;
145
  /** get the internal node value of the first element in this sequence */
146
  const Node& front() const;
147
  /** get the internal node value of the last element in this sequence */
148
  const Node& back() const;
149
  /** @return The element at the i-th position */
150
  const Node& nth(size_t i) const;
151
  /**
152
   * Returns the maximum sequence length representable by this class.
153
   * Corresponds to the maximum size of d_seq.
154
   */
155
  static size_t maxSize();
156
157
 private:
158
  /**
159
   * Returns a negative number if *this < y, 0 if *this and y are equal and a
160
   * positive number if *this > y.
161
   */
162
  int cmp(const Sequence& y) const;
163
  /** The element type of the sequence */
164
  std::unique_ptr<TypeNode> d_type;
165
  /** The data of the sequence */
166
  std::vector<Node> d_seq;
167
};
168
169
struct SequenceHashFunction
170
{
171
  size_t operator()(const Sequence& s) const;
172
};
173
174
std::ostream& operator<<(std::ostream& os, const Sequence& s);
175
176
}  // namespace CVC4
177
178
#endif /* CVC4__EXPR__SEQUENCE_H */