GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/expr/sequence.h Lines: 3 3 100.0 % Date: 2021-03-23 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 21 #include 22 23 namespace CVC4 { 24 25 template 26 class NodeTemplate; 27 typedef NodeTemplate 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& 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 20912 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& 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 d_type; 165 /** The data of the sequence */ 166 std::vector 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 */

 Generated by: GCOVR (Version 3.2)