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
--- /dev/null
+/******************************************************************************
+ * 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<ArrayEnumerator>(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<ArrayEnumerator>(
+ 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<TypeEnumerator*>::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
namespace theory {
namespace arrays {
-class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
- /** type properties */
- TypeEnumeratorProperties * d_tep;
+class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator>
+{
+ 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;
std::vector<TypeEnumerator*> d_constituentVec;
bool d_finished;
Node d_arrayConst;
-
- public:
- ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
- : TypeEnumeratorBase<ArrayEnumerator>(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<ArrayEnumerator>(
- 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<TypeEnumerator*>::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
projects / cvc5.git / commitdiff