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/arith | |
parent | 2e5cc613d280fab1be89d8360250cbc3a1635ac9 (diff) |
Removing throw specifiers from type enumerators. (#1502)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/type_enumerator.h | 42 |
1 files changed, 17 insertions, 25 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<RationalEnumerator> { Rational d_rat; -public: - - RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase<RationalEnumerator>(type), - d_rat(0) { + public: + RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst<TypeConstant>() == 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<IntegerEnumerator> { Integer d_int; -public: - - IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase<IntegerEnumerator>(type), - d_int(0) { + public: + IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0) + { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst<TypeConstant>() == 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 */ |