diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-10 08:52:01 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-10 08:52:01 -0800 |
commit | 7357de6df17449837e8da7defc9c8a52522c50de (patch) | |
tree | 9c50d698ad428299ce056818d0af65b0c4d310a7 /src/theory/builtin | |
parent | 2e5cc613d280fab1be89d8360250cbc3a1635ac9 (diff) |
Removing throw specifiers from type enumerators. (#1502)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/type_enumerator.cpp | 4 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 22 |
2 files changed, 15 insertions, 11 deletions
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 6435d3b4b..6884d41d9 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -39,7 +39,7 @@ Node FunctionEnumerator::operator*() return TheoryBuiltinRewriter::getLambdaForArrayRepresentation(a, d_bvl); } -FunctionEnumerator& FunctionEnumerator::operator++() throw() +FunctionEnumerator& FunctionEnumerator::operator++() { ++d_arrayEnum; return *this; @@ -47,4 +47,4 @@ FunctionEnumerator& FunctionEnumerator::operator++() throw() } /* CVC4::theory::builtin namespace */ } /* CVC4::theory namespace */ -} /* CVC4 namespace */
\ No newline at end of file +} /* CVC4 namespace */ diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index e75443140..e7258d27a 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -34,11 +34,12 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE Integer d_count; bool d_has_fixed_bound; Integer d_fixed_bound; -public: - UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : - TypeEnumeratorBase<UninterpretedSortEnumerator>(type), - d_count(0) { + public: + UninterpretedSortEnumerator(TypeNode type, + TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0) + { Assert(type.getKind() == kind::SORT_TYPE); d_has_fixed_bound = false; Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl; @@ -54,19 +55,22 @@ public: } } - Node operator*() { + Node operator*() override + { if(isFinished()) { throw NoMoreValuesException(getType()); } return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count)); } - UninterpretedSortEnumerator& operator++() throw() { + UninterpretedSortEnumerator& operator++() override + { d_count += 1; return *this; } - bool isFinished() throw() { + bool isFinished() override + { if( d_has_fixed_bound ){ return d_count>=d_fixed_bound; }else{ @@ -87,9 +91,9 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator> /** Get the current term of the enumerator. */ Node operator*() override; /** Increment the enumerator. */ - FunctionEnumerator& operator++() throw() override; + FunctionEnumerator& operator++() override; /** is the enumerator finished? */ - bool isFinished() throw() override { return d_arrayEnum.isFinished(); } + bool isFinished() override { return d_arrayEnum.isFinished(); } private: /** Enumerates arrays, which we convert to functions. */ TypeEnumerator d_arrayEnum; |