From 7357de6df17449837e8da7defc9c8a52522c50de Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 10 Jan 2018 08:52:01 -0800 Subject: [PATCH] Removing throw specifiers from type enumerators. (#1502) --- src/theory/arith/type_enumerator.h | 42 +++++------- src/theory/arrays/type_enumerator.h | 53 ++++++++------- src/theory/booleans/type_enumerator.h | 17 ++--- src/theory/builtin/type_enumerator.cpp | 4 +- src/theory/builtin/type_enumerator.h | 22 +++--- src/theory/datatypes/type_enumerator.h | 38 ++++++----- src/theory/sets/theory_sets_type_enumerator.h | 53 ++++++++------- src/theory/strings/type_enumerator.h | 68 +++++++++---------- src/theory/type_enumerator.h | 35 ++++++---- src/theory/type_enumerator_template.cpp | 4 +- 10 files changed, 175 insertions(+), 161 deletions(-) diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 4cb34ed4a..dad4ad4eb 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -32,20 +32,17 @@ namespace arith { class RationalEnumerator : public TypeEnumeratorBase { Rational d_rat; -public: - - RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase(type), - d_rat(0) { + public: + RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), d_rat(0) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == REAL_TYPE); } - Node operator*() throw() { - return NodeManager::currentNM()->mkConst(d_rat); - } - - RationalEnumerator& operator++() throw() { + Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); } + RationalEnumerator& operator++() override + { // sequence is 0, then diagonal with negatives interleaved // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3, // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...) @@ -70,29 +67,27 @@ public: return *this; } - bool isFinished() throw() { - return false; - } - + bool isFinished() override { return false; } };/* class RationalEnumerator */ class IntegerEnumerator : public TypeEnumeratorBase { Integer d_int; -public: - - IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase(type), - d_int(0) { + public: + IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), d_int(0) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == INTEGER_TYPE); } - Node operator*() throw() { + Node operator*() override + { return NodeManager::currentNM()->mkConst(Rational(d_int)); } - IntegerEnumerator& operator++() throw() { + IntegerEnumerator& operator++() override + { // sequence is 0, 1, -1, 2, -2, 3, -3, ... if(d_int <= 0) { d_int = -d_int + 1; @@ -102,10 +97,7 @@ public: return *this; } - bool isFinished() throw() { - return false; - } - + bool isFinished() override { return false; } };/* class IntegerEnumerator */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 4314fad83..2202c69bc 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -39,18 +39,17 @@ class ArrayEnumerator : public TypeEnumeratorBase { bool d_finished; Node d_arrayConst; -public: - - ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : - 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() + 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)); @@ -61,16 +60,17 @@ public: // 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) throw() : - 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) + 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(); @@ -87,7 +87,8 @@ public: } } - Node operator*() { + Node operator*() override + { if (d_finished) { throw NoMoreValuesException(getType()); } @@ -101,7 +102,8 @@ public: return n; } - ArrayEnumerator& operator++() { + ArrayEnumerator& operator++() override + { Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl; if (d_finished) { @@ -144,7 +146,8 @@ public: return *this; } - bool isFinished() throw() { + bool isFinished() override + { Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl; return d_finished; } diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index b0759cbb2..32c6bae42 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -30,11 +30,10 @@ namespace booleans { class BooleanEnumerator : public TypeEnumeratorBase { enum { FALSE, TRUE, DONE } d_value; -public: - - BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : - TypeEnumeratorBase(type), - d_value(FALSE) { + public: + BooleanEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), d_value(FALSE) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == BOOLEAN_TYPE); } @@ -50,7 +49,8 @@ public: } } - BooleanEnumerator& operator++() throw() { + BooleanEnumerator& operator++() override + { // sequence is FALSE, TRUE if(d_value == FALSE) { d_value = TRUE; @@ -60,10 +60,7 @@ public: return *this; } - bool isFinished() throw() { - return d_value == DONE; - } - + bool isFinished() override { return d_value == DONE; } };/* class BooleanEnumerator */ }/* CVC4::theory::booleans namespace */ 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(type), - d_count(0) { + public: + UninterpretedSortEnumerator(TypeNode type, + TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(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 /** 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; diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 8cf4ab3d9..462d6306e 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -79,21 +79,25 @@ class DatatypesEnumerator : public TypeEnumeratorBase { Node getCurrentTerm( unsigned index ); void init(); -public: - DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : - TypeEnumeratorBase(type), - d_tep(tep), - d_datatype(DatatypeType(type.toType()).getDatatype()), - d_type(type) { + public: + DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), + d_tep(tep), + d_datatype(DatatypeType(type.toType()).getDatatype()), + d_type(type) + { d_child_enum = false; init(); } - DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) : - TypeEnumeratorBase(type), - d_tep(tep), - d_datatype(DatatypeType(type.toType()).getDatatype()), - d_type(type) { + DatatypesEnumerator(TypeNode type, + bool childEnum, + TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), + d_tep(tep), + d_datatype(DatatypeType(type.toType()).getDatatype()), + d_type(type) + { d_child_enum = childEnum; init(); } @@ -127,10 +131,8 @@ public: d_child_enum = de.d_child_enum; } - virtual ~DatatypesEnumerator() throw() { - } - - Node operator*() { + Node operator*() override + { Debug("dt-enum-debug") << ": get term " << this << std::endl; if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) { return getCurrentTerm( d_ctor ); @@ -139,7 +141,8 @@ public: } } - DatatypesEnumerator& operator++() { + DatatypesEnumerator& operator++() override + { Debug("dt-enum-debug") << ": increment " << this << std::endl; unsigned prevSize = d_size_limit; while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) { @@ -171,7 +174,8 @@ public: return *this; } - bool isFinished() throw() { + bool isFinished() override + { return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors(); } diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index f261ac3fa..87a0485ae 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -42,18 +42,17 @@ class SetEnumerator : public TypeEnumeratorBase { bool d_finished; Node d_setConst; -public: - - SetEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase(type), - d_tep(tep), - d_index(0), - d_constituentType(type.getSetElementType()), - d_nm(NodeManager::currentNM()), - d_indexVec(), - d_constituentVec(), - d_finished(false), - d_setConst() + public: + SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type), + d_tep(tep), + d_index(0), + d_constituentType(type.getSetElementType()), + d_nm(NodeManager::currentNM()), + d_indexVec(), + d_constituentVec(), + d_finished(false), + d_setConst() { // d_indexVec.push_back(false); // d_constituentVec.push_back(new TypeEnumerator(d_constituentType)); @@ -63,16 +62,17 @@ public: // An set 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. - SetEnumerator(const SetEnumerator& ae) throw() : - TypeEnumeratorBase(ae.d_nm->mkSetType(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_setConst(ae.d_setConst) + SetEnumerator(const SetEnumerator& ae) + : TypeEnumeratorBase( + ae.d_nm->mkSetType(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_setConst(ae.d_setConst) { for(std::vector::const_iterator i = ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end(); @@ -89,7 +89,8 @@ public: } } - Node operator*() throw(NoMoreValuesException) { + Node operator*() override + { if (d_finished) { throw NoMoreValuesException(getType()); } @@ -108,7 +109,8 @@ public: return n; } - SetEnumerator& operator++() throw() { + SetEnumerator& operator++() override + { Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl; if (d_finished) { @@ -169,7 +171,8 @@ public: return *this; } - bool isFinished() throw() { + bool isFinished() override + { Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl; return d_finished; } diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index c7a36f2f5..b1904f53f 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -38,48 +38,52 @@ class StringEnumerator : public TypeEnumeratorBase { //make constant from d_data d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) ); } -public: - StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase(type) { + public: + StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(type) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == STRING_TYPE); d_cardinality = 256; mkCurr(); } - Node operator*() throw() { - return d_curr; - } - StringEnumerator& operator++() { - bool changed = false; - do{ - for(unsigned i=0; i d_data; Node d_curr; @@ -87,7 +91,8 @@ private: //make constant from d_data d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) ); } -public: + + public: StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) { for( unsigned i=0; iisFinished(); } - Node operator*() throw(NoMoreValuesException) { + Node operator*() + { // On Mac clang, there appears to be a code generation bug in an exception // block above (and perhaps here, too). For now, there doesn't appear a // good workaround; just disable assertions on that setup. @@ -163,11 +164,19 @@ public: return **d_te; #endif /* CVC4_ASSERTIONS && !(APPLE || clang) */ } - TypeEnumerator& operator++() throw() { ++*d_te; return *this; } - TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; } - - TypeNode getType() const throw() { return d_te->getType(); } + TypeEnumerator& operator++() + { + ++*d_te; + return *this; + } + TypeEnumerator operator++(int) + { + TypeEnumerator te = *this; + ++*d_te; + return te; + } + TypeNode getType() const { return d_te->getType(); } };/* class TypeEnumerator */ }/* CVC4::theory namespace */ diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index a2bc8ab86..91ae3e1d6 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -29,7 +29,9 @@ using namespace std; namespace CVC4 { namespace theory { -TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep) throw(AssertionException) { +TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator( + TypeNode type, TypeEnumeratorProperties* tep) +{ switch(type.getKind()) { case kind::TYPE_CONSTANT: switch(type.getConst()) { -- 2.30.2