From fc42f53145e403216b2a5cf91cc437de7456a0f6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 22 Sep 2021 10:08:34 -0700 Subject: arrays: Move type enumerator implementation to .cpp. (#7216) This further cleans up the class declaration in the header to comply with code style guidelines. --- src/CMakeLists.txt | 1 + src/theory/arrays/type_enumerator.cpp | 159 ++++++++++++++++++++++++++++++++++ src/theory/arrays/type_enumerator.h | 143 +++++------------------------- 3 files changed, 184 insertions(+), 119 deletions(-) create mode 100644 src/theory/arrays/type_enumerator.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5dbaa3349..9b2e2e8e2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -543,6 +543,7 @@ libcvc5_add_sources( theory/arrays/theory_arrays_type_rules.cpp theory/arrays/theory_arrays_type_rules.h theory/arrays/type_enumerator.h + theory/arrays/type_enumerator.cpp theory/arrays/union_find.cpp theory/arrays/union_find.h theory/assertion.cpp diff --git a/src/theory/arrays/type_enumerator.cpp b/src/theory/arrays/type_enumerator.cpp new file mode 100644 index 000000000..c1187f0da --- /dev/null +++ b/src/theory/arrays/type_enumerator.cpp @@ -0,0 +1,159 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Clark Barrett, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * An enumerator for arrays. + */ +#include "theory/arrays/type_enumerator.h" + +#include "expr/array_store_all.h" +#include "expr/kind.h" +#include "expr/type_node.h" +#include "theory/rewriter.h" +#include "theory/type_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace arrays { + +ArrayEnumerator::ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase(type), + d_tep(tep), + d_index(type.getArrayIndexType(), tep), + d_constituentType(type.getArrayConstituentType()), + d_nm(NodeManager::currentNM()), + d_indexVec(), + d_constituentVec(), + d_finished(false), + d_arrayConst() +{ + d_indexVec.push_back(*d_index); + d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); + d_arrayConst = + d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back())))); + Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl; +} + +ArrayEnumerator::ArrayEnumerator(const ArrayEnumerator& ae) + : TypeEnumeratorBase( + ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)), + d_tep(ae.d_tep), + d_index(ae.d_index), + d_constituentType(ae.d_constituentType), + d_nm(ae.d_nm), + d_indexVec(ae.d_indexVec), + d_constituentVec(), // copied below + d_finished(ae.d_finished), + d_arrayConst(ae.d_arrayConst) +{ + for (std::vector::const_iterator + i = ae.d_constituentVec.begin(), + i_end = ae.d_constituentVec.end(); + i != i_end; + ++i) + { + d_constituentVec.push_back(new TypeEnumerator(**i)); + } +} + +ArrayEnumerator::~ArrayEnumerator() +{ + while (!d_constituentVec.empty()) + { + delete d_constituentVec.back(); + d_constituentVec.pop_back(); + } +} + +Node ArrayEnumerator::operator*() +{ + if (d_finished) + { + throw NoMoreValuesException(getType()); + } + Node n = d_arrayConst; + for (size_t i = 0, size = d_indexVec.size(); i < size; ++i) + { + n = d_nm->mkNode(kind::STORE, + n, + d_indexVec[d_indexVec.size() - 1 - i], + *(*(d_constituentVec[i]))); + } + Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl; + n = Rewriter::rewrite(n); + Trace("array-type-enum") << "operator * returning: " << n << std::endl; + return n; +} + +ArrayEnumerator& ArrayEnumerator::operator++() +{ + Trace("array-type-enum") << "operator++ called, **this = " << **this + << std::endl; + + if (d_finished) + { + Trace("array-type-enum") << "operator++ finished!" << std::endl; + return *this; + } + while (!d_constituentVec.empty()) + { + ++(*d_constituentVec.back()); + if (d_constituentVec.back()->isFinished()) + { + delete d_constituentVec.back(); + d_constituentVec.pop_back(); + } + else + { + break; + } + } + + if (d_constituentVec.empty()) + { + ++d_index; + if (d_index.isFinished()) + { + Trace("array-type-enum") << "operator++ finished!" << std::endl; + d_finished = true; + return *this; + } + d_indexVec.push_back(*d_index); + d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); + ++(*d_constituentVec.back()); + if (d_constituentVec.back()->isFinished()) + { + Trace("array-type-enum") << "operator++ finished!" << std::endl; + d_finished = true; + return *this; + } + } + + while (d_constituentVec.size() < d_indexVec.size()) + { + d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); + } + + Trace("array-type-enum") << "operator++ returning, **this = " << **this + << std::endl; + return *this; +} + +bool ArrayEnumerator::isFinished() +{ + Trace("array-type-enum") << "isFinished returning: " << d_finished + << std::endl; + return d_finished; +} + +} // namespace arrays +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 6fc026b19..097b16184 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -28,9 +28,29 @@ namespace cvc5 { namespace theory { namespace arrays { -class ArrayEnumerator : public TypeEnumeratorBase { - /** type properties */ - TypeEnumeratorProperties * d_tep; +class ArrayEnumerator : public TypeEnumeratorBase +{ + public: + /** Constructor. */ + ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + + /** + * Copy Constructor. + * An array enumerator could be large, and generally you don't want to + * go around copying these things; but a copy ctor is presently required + * by the TypeEnumerator framework. + */ + ArrayEnumerator(const ArrayEnumerator& ae); + + /** Destructor. */ + ~ArrayEnumerator(); + + Node operator*() override; + ArrayEnumerator& operator++() override; + bool isFinished() override; + + private: + TypeEnumeratorProperties* d_tep; TypeEnumerator d_index; TypeNode d_constituentType; NodeManager* d_nm; @@ -38,122 +58,7 @@ class ArrayEnumerator : public TypeEnumeratorBase { std::vector d_constituentVec; bool d_finished; Node d_arrayConst; - - public: - ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) - : TypeEnumeratorBase(type), - d_tep(tep), - d_index(type.getArrayIndexType(), tep), - d_constituentType(type.getArrayConstituentType()), - d_nm(NodeManager::currentNM()), - d_indexVec(), - d_constituentVec(), - d_finished(false), - d_arrayConst() - { - d_indexVec.push_back(*d_index); - d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); - d_arrayConst = - d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back())))); - Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl; - } - - // An array enumerator could be large, and generally you don't want to - // go around copying these things; but a copy ctor is presently required - // by the TypeEnumerator framework. - ArrayEnumerator(const ArrayEnumerator& ae) - : TypeEnumeratorBase( - ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)), - d_tep(ae.d_tep), - d_index(ae.d_index), - d_constituentType(ae.d_constituentType), - d_nm(ae.d_nm), - d_indexVec(ae.d_indexVec), - d_constituentVec(), // copied below - d_finished(ae.d_finished), - d_arrayConst(ae.d_arrayConst) - { - for(std::vector::const_iterator i = - ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end(); - i != i_end; - ++i) { - d_constituentVec.push_back(new TypeEnumerator(**i)); - } - } - - ~ArrayEnumerator() { - while (!d_constituentVec.empty()) { - delete d_constituentVec.back(); - d_constituentVec.pop_back(); - } - } - - Node operator*() override - { - if (d_finished) { - throw NoMoreValuesException(getType()); - } - Node n = d_arrayConst; - for (unsigned i = 0; i < d_indexVec.size(); ++i) { - n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i]))); - } - Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl; - n = Rewriter::rewrite(n); - Trace("array-type-enum") << "operator * returning: " << n << std::endl; - return n; - } - - ArrayEnumerator& operator++() override - { - Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl; - - if (d_finished) { - Trace("array-type-enum") << "operator++ finished!" << std::endl; - return *this; - } - while (!d_constituentVec.empty()) { - ++(*d_constituentVec.back()); - if (d_constituentVec.back()->isFinished()) { - delete d_constituentVec.back(); - d_constituentVec.pop_back(); - } - else { - break; - } - } - - if (d_constituentVec.empty()) { - ++d_index; - if (d_index.isFinished()) { - Trace("array-type-enum") << "operator++ finished!" << std::endl; - d_finished = true; - return *this; - } - d_indexVec.push_back(*d_index); - d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); - ++(*d_constituentVec.back()); - if (d_constituentVec.back()->isFinished()) { - Trace("array-type-enum") << "operator++ finished!" << std::endl; - d_finished = true; - return *this; - } - } - - while (d_constituentVec.size() < d_indexVec.size()) { - d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); - } - - Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl; - return *this; - } - - bool isFinished() override - { - Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl; - return d_finished; - } - -};/* class ArrayEnumerator */ +}; /* class ArrayEnumerator */ } // namespace arrays } // namespace theory -- cgit v1.2.3