diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-12 17:37:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-12 19:37:03 -0500 |
commit | 090d8bc3c31404140856e51d2cc5a5aa1335b3b3 (patch) | |
tree | 0edb9c6a4b37ea22ca0729061659ecfc95738393 /src/expr | |
parent | 64a7db86206aa0993f75446a3e7f77f3c0c023c6 (diff) |
Remove ExprSequence (#4724)
Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/expr_sequence.cpp | 98 | ||||
-rw-r--r-- | src/expr/expr_sequence.h | 78 | ||||
-rw-r--r-- | src/expr/sequence.cpp | 105 | ||||
-rw-r--r-- | src/expr/sequence.h | 34 |
5 files changed, 79 insertions, 238 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9222393c4..bad2f1f42 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -12,8 +12,6 @@ libcvc4_add_sources( expr_iomanip.cpp expr_iomanip.h expr_manager_scope.h - expr_sequence.cpp - expr_sequence.h kind_map.h lazy_proof.cpp lazy_proof.h diff --git a/src/expr/expr_sequence.cpp b/src/expr/expr_sequence.cpp deleted file mode 100644 index aa58bba32..000000000 --- a/src/expr/expr_sequence.cpp +++ /dev/null @@ -1,98 +0,0 @@ -/********************* */ -/*! \file expr_sequence.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Implementation of the sequence data type. - **/ - -#include "expr/expr_sequence.h" - -#include "expr/expr.h" -#include "expr/node.h" -#include "expr/sequence.h" -#include "expr/type.h" -#include "expr/type_node.h" - -namespace CVC4 { - -ExprSequence::ExprSequence(const Type& t, const std::vector<Expr>& seq) -{ - d_type.reset(new Type(t)); - std::vector<Node> nseq; - for (const Expr& e : seq) - { - nseq.push_back(Node::fromExpr(e)); - } - d_sequence.reset(new Sequence(TypeNode::fromType(t), nseq)); -} -ExprSequence::~ExprSequence() {} - -ExprSequence::ExprSequence(const ExprSequence& other) - : d_type(new Type(other.getType())), - d_sequence(new Sequence(other.getSequence())) -{ -} - -ExprSequence& ExprSequence::operator=(const ExprSequence& other) -{ - (*d_type) = other.getType(); - (*d_sequence) = other.getSequence(); - return *this; -} - -const Type& ExprSequence::getType() const { return *d_type; } - -const Sequence& ExprSequence::getSequence() const { return *d_sequence; } - -bool ExprSequence::operator==(const ExprSequence& es) const -{ - return getType() == es.getType() && getSequence() == es.getSequence(); -} - -bool ExprSequence::operator!=(const ExprSequence& es) const -{ - return !(*this == es); -} - -bool ExprSequence::operator<(const ExprSequence& es) const -{ - return (getType() < es.getType()) - || (getType() == es.getType() && getSequence() < es.getSequence()); -} - -bool ExprSequence::operator<=(const ExprSequence& es) const -{ - return (getType() < es.getType()) - || (getType() == es.getType() && getSequence() <= es.getSequence()); -} - -bool ExprSequence::operator>(const ExprSequence& es) const -{ - return !(*this <= es); -} - -bool ExprSequence::operator>=(const ExprSequence& es) const -{ - return !(*this < es); -} - -std::ostream& operator<<(std::ostream& os, const ExprSequence& s) -{ - return os << "__expr_sequence__(" << s.getType() << ", " << s.getSequence() - << ")"; -} - -size_t ExprSequenceHashFunction::operator()(const ExprSequence& es) const -{ - uint64_t hash = fnv1a::fnv1a_64(TypeHashFunction()(es.getType())); - return static_cast<size_t>(SequenceHashFunction()(es.getSequence()), hash); -} - -} // namespace CVC4 diff --git a/src/expr/expr_sequence.h b/src/expr/expr_sequence.h deleted file mode 100644 index 8d14f1dcb..000000000 --- a/src/expr/expr_sequence.h +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \file expr_sequence.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 The sequence data type. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__EXPR__EXPR_SEQUENCE_H -#define CVC4__EXPR__EXPR_SEQUENCE_H - -#include <iosfwd> -#include <memory> -#include <vector> - -namespace CVC4 { - -// messy; Expr needs ExprSequence (because it's the payload of a -// CONSTANT-kinded expression), and ExprSequence needs Expr. -class Type; -class Expr; -class Sequence; - -/** The CVC4 sequence class - * - * This data structure is the domain of values for the sequence type. - */ -class CVC4_PUBLIC ExprSequence -{ - public: - /** constructors for ExprSequence - * - * Internally, a CVC4::ExprSequence is represented by a vector of Nodes - * (d_seq), where each Node in this vector must be a constant. - */ - ExprSequence(const Type& type, const std::vector<Expr>& seq); - ~ExprSequence(); - - ExprSequence(const ExprSequence& other); - ExprSequence& operator=(const ExprSequence& other); - - bool operator==(const ExprSequence& es) const; - bool operator!=(const ExprSequence& es) const; - bool operator<(const ExprSequence& es) const; - bool operator<=(const ExprSequence& es) const; - bool operator>(const ExprSequence& es) const; - bool operator>=(const ExprSequence& es) const; - - /** Get the element type of the sequence */ - const Type& getType() const; - /** Get the underlying sequence */ - const Sequence& getSequence() const; - - private: - /** The element type of the sequence */ - std::unique_ptr<Type> d_type; - /** The data of the sequence */ - std::unique_ptr<Sequence> d_sequence; -}; /* class ExprSequence */ - -struct CVC4_PUBLIC ExprSequenceHashFunction -{ - size_t operator()(const ::CVC4::ExprSequence& s) const; -}; /* struct ExprSequenceHashFunction */ - -std::ostream& operator<<(std::ostream& os, const ExprSequence& s) CVC4_PUBLIC; - -} // namespace CVC4 - -#endif /* CVC4__EXPR__SEQUENCE_H */ diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index 0eb8401e6..816b894e0 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -14,38 +14,52 @@ #include "expr/sequence.h" -#include "expr/expr_sequence.h" +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" using namespace std; namespace CVC4 { -Sequence::Sequence(TypeNode t, const std::vector<Node>& s) : d_type(t), d_seq(s) +Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s) + : d_type(new TypeNode(t)), d_seq(s) +{ +} + +Sequence::Sequence(const Sequence& seq) + : d_type(new TypeNode(seq.getType())), d_seq(seq.getVec()) { } +Sequence::~Sequence() {} + Sequence& Sequence::operator=(const Sequence& y) { if (this != &y) { - d_type = y.d_type; - d_seq = y.d_seq; + d_type.reset(new TypeNode(y.getType())); + d_seq = y.getVec(); } return *this; } int Sequence::cmp(const Sequence& y) const { - Assert(d_type == y.d_type); + if (getType() != y.getType()) + { + return getType() < y.getType() ? -1 : 1; + } if (size() != y.size()) { return size() < y.size() ? -1 : 1; } for (size_t i = 0, sz = size(); i < sz; ++i) { - if (d_seq[i] != y.d_seq[i]) + if (nth(i) != y.nth(i)) { - return d_seq[i] < y.d_seq[i] ? -1 : 1; + return nth(i) < y.nth(i) ? -1 : 1; } } return 0; @@ -53,15 +67,15 @@ int Sequence::cmp(const Sequence& y) const Sequence Sequence::concat(const Sequence& other) const { - Assert(d_type == other.d_type); + Assert(getType() == other.getType()); std::vector<Node> ret_vec(d_seq); ret_vec.insert(ret_vec.end(), other.d_seq.begin(), other.d_seq.end()); - return Sequence(d_type, ret_vec); + return Sequence(getType(), ret_vec); } bool Sequence::strncmp(const Sequence& y, size_t n) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); size_t b = (size() >= y.size()) ? size() : y.size(); size_t s = (size() <= y.size()) ? size() : y.size(); if (n > s) @@ -74,7 +88,7 @@ bool Sequence::strncmp(const Sequence& y, size_t n) const } for (size_t i = 0; i < n; ++i) { - if (d_seq[i] != y.d_seq[i]) + if (nth(i) != y.nth(i)) { return false; } @@ -97,7 +111,7 @@ bool Sequence::rstrncmp(const Sequence& y, size_t n) const } for (size_t i = 0; i < n; ++i) { - if (d_seq[size() - i - 1] != y.d_seq[y.size() - i - 1]) + if (nth(size() - i - 1) != y.nth(y.size() - i - 1)) { return false; } @@ -105,21 +119,31 @@ bool Sequence::rstrncmp(const Sequence& y, size_t n) const return true; } -Node Sequence::front() const +bool Sequence::empty() const { return d_seq.empty(); } + +size_t Sequence::size() const { return d_seq.size(); } + +const Node& Sequence::front() const { Assert(!d_seq.empty()); return d_seq.front(); } -Node Sequence::back() const +const Node& Sequence::back() const { Assert(!d_seq.empty()); return d_seq.back(); } +const Node& Sequence::nth(size_t i) const +{ + Assert(i < size()); + return d_seq[i]; +} + size_t Sequence::overlap(const Sequence& y) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); size_t i = size() < y.size() ? size() : y.size(); for (; i > 0; i--) { @@ -135,7 +159,7 @@ size_t Sequence::overlap(const Sequence& y) const size_t Sequence::roverlap(const Sequence& y) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); size_t i = size() < y.size() ? size() : y.size(); for (; i > 0; i--) { @@ -149,14 +173,18 @@ size_t Sequence::roverlap(const Sequence& y) const return i; } +const TypeNode& Sequence::getType() const { return *d_type; } + +const std::vector<Node>& Sequence::getVec() const { return d_seq; } + bool Sequence::isRepeated() const { if (size() > 1) { - Node f = d_seq[0]; + Node f = nth(0); for (unsigned i = 1, sz = size(); i < sz; ++i) { - if (f != d_seq[i]) + if (f != nth(i)) { return false; } @@ -167,7 +195,7 @@ bool Sequence::isRepeated() const size_t Sequence::find(const Sequence& y, size_t start) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); if (size() < y.size() + start) { return std::string::npos; @@ -191,7 +219,7 @@ size_t Sequence::find(const Sequence& y, size_t start) const size_t Sequence::rfind(const Sequence& y, size_t start) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); if (size() < y.size() + start) { return std::string::npos; @@ -215,7 +243,7 @@ size_t Sequence::rfind(const Sequence& y, size_t start) const bool Sequence::hasPrefix(const Sequence& y) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); size_t s = size(); size_t ys = y.size(); if (ys > s) @@ -224,7 +252,7 @@ bool Sequence::hasPrefix(const Sequence& y) const } for (size_t i = 0; i < ys; i++) { - if (d_seq[i] != y.d_seq[i]) + if (nth(i) != y.nth(i)) { return false; } @@ -234,7 +262,7 @@ bool Sequence::hasPrefix(const Sequence& y) const bool Sequence::hasSuffix(const Sequence& y) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); size_t s = size(); size_t ys = y.size(); if (ys > s) @@ -244,7 +272,7 @@ bool Sequence::hasSuffix(const Sequence& y) const size_t idiff = s - ys; for (size_t i = 0; i < ys; i++) { - if (d_seq[i + idiff] != y.d_seq[i]) + if (nth(i + idiff) != y.nth(i)) { return false; } @@ -254,8 +282,8 @@ bool Sequence::hasSuffix(const Sequence& y) const Sequence Sequence::replace(const Sequence& s, const Sequence& t) const { - Assert(d_type == s.d_type); - Assert(d_type == t.d_type); + Assert(getType() == s.getType()); + Assert(getType() == t.getType()); size_t ret = find(s); if (ret != std::string::npos) { @@ -263,7 +291,7 @@ Sequence Sequence::replace(const Sequence& s, const Sequence& t) const vec.insert(vec.begin(), d_seq.begin(), d_seq.begin() + ret); vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end()); vec.insert(vec.end(), d_seq.begin() + ret + s.size(), d_seq.end()); - return Sequence(d_type, vec); + return Sequence(getType(), vec); } return *this; } @@ -272,10 +300,8 @@ Sequence Sequence::substr(size_t i) const { Assert(i >= 0); Assert(i <= size()); - std::vector<Node> ret_vec; - std::vector<Node>::const_iterator itr = d_seq.begin() + i; - ret_vec.insert(ret_vec.end(), itr, d_seq.end()); - return Sequence(d_type, ret_vec); + std::vector<Node> retVec(d_seq.begin() + i, d_seq.end()); + return Sequence(getType(), retVec); } Sequence Sequence::substr(size_t i, size_t j) const @@ -283,15 +309,14 @@ Sequence Sequence::substr(size_t i, size_t j) const Assert(i >= 0); Assert(j >= 0); Assert(i + j <= size()); - std::vector<Node> ret_vec; std::vector<Node>::const_iterator itr = d_seq.begin() + i; - ret_vec.insert(ret_vec.end(), itr, itr + j); - return Sequence(d_type, ret_vec); + std::vector<Node> retVec(itr, itr + j); + return Sequence(getType(), retVec); } bool Sequence::noOverlapWith(const Sequence& y) const { - Assert(d_type == y.d_type); + Assert(getType() == y.getType()); return y.find(*this) == std::string::npos && this->find(y) == std::string::npos && this->overlap(y) == 0 && y.overlap(*this) == 0; @@ -299,16 +324,6 @@ bool Sequence::noOverlapWith(const Sequence& y) const size_t Sequence::maxSize() { return std::numeric_limits<uint32_t>::max(); } -ExprSequence Sequence::toExprSequence() -{ - std::vector<Expr> seq; - for (const Node& n : d_seq) - { - seq.push_back(n.toExpr()); - } - return ExprSequence(d_type.toType(), seq); -} - std::ostream& operator<<(std::ostream& os, const Sequence& s) { const std::vector<Node>& vec = s.getVec(); diff --git a/src/expr/sequence.h b/src/expr/sequence.h index 763534274..c3b710592 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -12,17 +12,20 @@ ** \brief The sequence data type. **/ -#include "cvc4_private.h" +#include "cvc4_public.h" #ifndef CVC4__EXPR__SEQUENCE_H #define CVC4__EXPR__SEQUENCE_H +#include <memory> #include <vector> -#include "expr/node.h" namespace CVC4 { -class ExprSequence; +template <bool ref_count> +class NodeTemplate; +typedef NodeTemplate<true> Node; +class TypeNode; /** The CVC4 sequence class * @@ -37,7 +40,10 @@ class Sequence * where each Node in this vector must be a constant. */ Sequence() = default; - explicit Sequence(TypeNode t, const std::vector<Node>& s); + explicit Sequence(const TypeNode& t, const std::vector<Node>& s); + Sequence(const Sequence& seq); + + ~Sequence(); Sequence& operator=(const Sequence& y); @@ -54,11 +60,11 @@ class Sequence bool rstrncmp(const Sequence& y, size_t n) const; /** is this the empty sequence? */ - bool empty() const { return d_seq.empty(); } + bool empty() const; /** is less than or equal to sequence y */ bool isLeq(const Sequence& y) const; /** Return the length of the sequence */ - size_t size() const { return d_seq.size(); } + size_t size() const; /** Return true if this sequence is a repetition of the same element */ bool isRepeated() const; @@ -131,23 +137,21 @@ class Sequence size_t roverlap(const Sequence& y) const; /** get the element type of the sequence */ - TypeNode getType() const { return d_type; } + const TypeNode& getType() const; /** get the internal Node representation of this sequence */ - const std::vector<Node>& getVec() const { return d_seq; } + const std::vector<Node>& getVec() const; /** get the internal node value of the first element in this sequence */ - Node front() const; + const Node& front() const; /** get the internal node value of the last element in this sequence */ - Node back() const; + const Node& back() const; + /** @return The element at the i-th position */ + const Node& nth(size_t i) const; /** * Returns the maximum sequence length representable by this class. * Corresponds to the maximum size of d_seq. */ static size_t maxSize(); - //!!!!!!!!!!!!!!! temporary - ExprSequence toExprSequence(); - //!!!!!!!!!!!!!!! end temporary - private: /** * Returns a negative number if *this < y, 0 if *this and y are equal and a @@ -155,7 +159,7 @@ class Sequence */ int cmp(const Sequence& y) const; /** The element type of the sequence */ - TypeNode d_type; + std::unique_ptr<TypeNode> d_type; /** The data of the sequence */ std::vector<Node> d_seq; }; |