From 33ca2a3f2359493a9154a229a30ad3aa3a21f2aa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 17 Aug 2017 08:51:51 -0700 Subject: Remove unused SubrangeBound(s) classes (#221) As discussed in pull request #220, commit 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s). There were still a few mentions of it left in the code, most of them commented out. The occurrences in expr.i and expr_manager.i, however, created issues with the Python wrapper. This commit removes the SubrangeBound(s) implementation and other leftovers. --- src/compat/cvc3_compat.cpp | 10 -- src/cvc4.i | 1 - src/expr/expr.i | 1 - src/expr/expr_manager.i | 1 - src/expr/expr_manager_template.h | 9 +- src/expr/node_manager.h | 1 - src/expr/type.h | 16 -- src/parser/cvc/Cvc.g | 30 +--- src/theory/arith/theory_arith_type_rules.h | 2 - src/util/Makefile.am | 3 - src/util/subrange_bound.cpp | 61 -------- src/util/subrange_bound.h | 234 ----------------------------- src/util/subrange_bound.i | 24 --- test/unit/theory/type_enumerator_white.h | 34 ----- 14 files changed, 6 insertions(+), 421 deletions(-) delete mode 100644 src/util/subrange_bound.cpp delete mode 100644 src/util/subrange_bound.h delete mode 100644 src/util/subrange_bound.i diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index ffb299394..169b49faa 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -33,7 +33,6 @@ #include "smt/command.h" #include "util/bitvector.h" #include "util/sexpr.h" -#include "util/subrange_bound.h" using namespace std; @@ -1255,15 +1254,6 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { -/* - bool noLowerBound = l.getType().isString() && l.getConst() == "_NEGINF"; - bool noUpperBound = r.getType().isString() && r.getConst() == "_POSINF"; - CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst().isIntegral()), l); - CompatCheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst().isIntegral()), r); - CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst().getNumerator()); - CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst().getNumerator()); - return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); - */ Unimplemented("Subrange types not supported by CVC4 (sorry!)"); } diff --git a/src/cvc4.i b/src/cvc4.i index 4768e2344..f07f9fba3 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -326,7 +326,6 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "util/result.i" %include "util/sexpr.i" %include "util/statistics.i" -%include "util/subrange_bound.i" %include "util/tuple.i" %include "util/unsafe_interrupt_exception.i" diff --git a/src/expr/expr.i b/src/expr/expr.i index 93a0cbe99..d77981cc4 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -141,7 +141,6 @@ namespace CVC4 { %template(getConstBitVectorSize) CVC4::Expr::getConst; %template(getConstAscriptionType) CVC4::Expr::getConst; %template(getConstBitVectorBitOf) CVC4::Expr::getConst; -%template(getConstSubrangeBounds) CVC4::Expr::getConst; %template(getConstBitVectorRepeat) CVC4::Expr::getConst; %template(getConstBitVectorExtract) CVC4::Expr::getConst; %template(getConstBitVectorRotateLeft) CVC4::Expr::getConst; diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index b8f8d5da9..136e75f98 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -44,7 +44,6 @@ %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; -%template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 8719d8ef4..a12c68791 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -25,7 +25,6 @@ #include "expr/kind.h" #include "expr/type.h" #include "util/statistics.h" -#include "util/subrange_bound.h" ${includes} @@ -33,7 +32,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 37 "${template}" +#line 36 "${template}" namespace CVC4 { @@ -458,12 +457,6 @@ public: //Type mkPredicateSubtype(Expr lambda, Expr witness) // throw(TypeCheckingException); - /** - * Make an integer subrange type as defined by the argument. - */ - //Type mkSubrangeType(const SubrangeBounds& bounds) - // throw(TypeCheckingException); - /** Get the type of an expression */ Type getType(Expr e, bool check = false) throw(TypeCheckingException); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f112381d8..fab5d4688 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -36,7 +36,6 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" -#include "util/subrange_bound.h" #include "options/options.h" namespace CVC4 { diff --git a/src/expr/type.h b/src/expr/type.h index 25f0c5436..dfab42dad 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -25,7 +25,6 @@ #include #include "util/cardinality.h" -#include "util/subrange_bound.h" namespace CVC4 { @@ -584,21 +583,6 @@ public: Type getParentType() const; };/* class PredicateSubtype */ - -/** - * Class encapsulating an integer subrange type. - */ -class CVC4_PUBLIC SubrangeType : public Type { - -public: - - /** Construct from the base type */ - SubrangeType(const Type& type = Type()) throw(IllegalArgumentException); - - /** Get the bounds defining this integer subrange */ - SubrangeBounds getSubrangeBounds() const; - -};/* class SubrangeType */ #endif /* 0 */ /** diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a137cece3..efdd328a4 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -539,7 +539,6 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { #include "parser/antlr_tracing.h" #include "parser/parser.h" #include "smt/command.h" -#include "util/subrange_bound.h" namespace CVC4 { class Expr; @@ -559,18 +558,6 @@ namespace CVC4 { myString() : std::string() {} };/* class myString */ - /** - * Just exists to give us the void* construction that - * ANTLR requires. - */ - class mySubrangeBound : public CVC4::SubrangeBound { - public: - mySubrangeBound() : CVC4::SubrangeBound() {} - mySubrangeBound(void*) : CVC4::SubrangeBound() {} - mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {} - mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {} - };/* class mySubrangeBound */ - /** * Just exists to give us the void* construction that * ANTLR requires. @@ -1284,16 +1271,9 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } /* subrange types */ - | LBRACKET k1=bound DOTDOT k2=bound RBRACKET - { if(k1.hasBound() && k2.hasBound() && - k1.getBound() > k2.getBound()) { - std::stringstream ss; - ss << "Subrange [" << k1.getBound() << ".." << k2.getBound() - << "] inappropriate: range must be nonempty!"; - PARSER_STATE->parseError(ss.str()); - } + | LBRACKET bound DOTDOT bound RBRACKET + { PARSER_STATE->unimplementedFeature("subrange typing not supported in this release"); - //t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2)); } /* tuple types / old-style function types */ @@ -1348,9 +1328,9 @@ parameterization[CVC4::parser::DeclarationCheck check, ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET ; -bound returns [CVC4::parser::cvc::mySubrangeBound bound] - : UNDERSCORE { $bound = SubrangeBound(); } - | k=integer { $bound = SubrangeBound(k.getNumerator()); } +bound + : UNDERSCORE + | integer ; typeLetDecl[CVC4::parser::DeclarationCheck check] diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index db3ae65f2..e19573039 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -19,8 +19,6 @@ #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H #define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H -#include "util/subrange_bound.h" - namespace CVC4 { namespace theory { namespace arith { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 877525de7..027abce64 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -55,8 +55,6 @@ libutil_la_SOURCES = \ statistics.h \ statistics_registry.cpp \ statistics_registry.h \ - subrange_bound.cpp \ - subrange_bound.h \ tuple.h \ unsafe_interrupt_exception.h \ utility.h @@ -102,7 +100,6 @@ EXTRA_DIST = \ result.i \ sexpr.i \ statistics.i \ - subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp deleted file mode 100644 index b49a3ef27..000000000 --- a/src/util/subrange_bound.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file subrange_bound.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 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.\endverbatim - ** - ** \brief Representation of subrange bounds - ** - ** Simple class to represent a subrange bound, either infinite - ** (no bound) or finite (an arbitrary precision integer). - **/ - -#include "util/subrange_bound.h" - -#include - -#include "base/cvc4_assert.h" -#include "base/exception.h" -#include "util/integer.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) { - out << bounds.lower << ".." << bounds.upper; - - return out; -} - -/** Get the finite SubrangeBound, failing an assertion if infinite. */ -const Integer& SubrangeBound::getBound() const { - PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite"); - return d_bound; -} - -SubrangeBounds::SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) - : lower(l), upper(u) { - PrettyCheckArgument( - !l.hasBound() || !u.hasBound() || l.getBound() <= u.getBound(), l, - "Bad subrange bounds specified"); -} - -bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, - const SubrangeBounds& b) { - return (a.lower.hasBound() && b.lower.hasBound()) || - (a.upper.hasBound() && b.upper.hasBound()); -} - -SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, - const SubrangeBounds& b) { - DebugCheckArgument(joinIsBounded(a, b), a); - SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); - SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); - return SubrangeBounds(newLower, newUpper); -} - -} /* namespace CVC4 */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h deleted file mode 100644 index 1f1cb84d7..000000000 --- a/src/util/subrange_bound.h +++ /dev/null @@ -1,234 +0,0 @@ -/********************* */ -/*! \file subrange_bound.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 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.\endverbatim - ** - ** \brief Representation of subrange bounds - ** - ** Simple class to represent a subrange bound, either infinite - ** (no bound) or finite (an arbitrary precision integer). - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SUBRANGE_BOUND_H -#define __CVC4__SUBRANGE_BOUND_H - -#include - -#include "base/exception.h" -#include "util/integer.h" - -namespace CVC4 { - -/** - * Representation of a subrange bound. A bound can either exist and be - * a finite arbitrary-precision integer, or not exist (and thus be - * an infinite bound). For example, the CVC language subrange [-5.._] - * has a lower bound of -5 and an infinite upper bound. - */ -class CVC4_PUBLIC SubrangeBound { - public: - /** Construct an infinite SubrangeBound. */ - SubrangeBound() : d_nobound(true), d_bound() {} - - /** Construct a finite SubrangeBound. */ - SubrangeBound(const Integer& i) : d_nobound(false), d_bound(i) {} - - ~SubrangeBound() {} - - /** - * Get the finite SubrangeBound, failing an assertion if infinite. - * - * @throws IllegalArgumentException if the bound is infinite. - */ - const Integer& getBound() const; - - /** Returns true iff this is a finite SubrangeBound. */ - bool hasBound() const { return !d_nobound; } - - /** Test two SubrangeBounds for equality. */ - bool operator==(const SubrangeBound& b) const { - return hasBound() == b.hasBound() && - (!hasBound() || getBound() == b.getBound()); - } - - /** Test two SubrangeBounds for disequality. */ - bool operator!=(const SubrangeBound& b) const { return !(*this == b); } - - /** - * Is this SubrangeBound "less than" another? For two - * SubrangeBounds that "have bounds," this is defined as expected. - * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a - * bound, b1 < b2 (but note also that b1 > b2). This strange - * behavior is due to the fact that a SubrangeBound without a bound - * is the representation for both +infinity and -infinity. - */ - bool operator<(const SubrangeBound& b) const { - return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - (hasBound() && b.hasBound() && getBound() < b.getBound()); - } - - /** - * Is this SubrangeBound "less than or equal to" another? For two - * SubrangeBounds that "have bounds," this is defined as expected. - * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a - * bound, b1 < b2 (but note also that b1 > b2). This strange - * behavior is due to the fact that a SubrangeBound without a bound - * is the representation for both +infinity and -infinity. - */ - bool operator<=(const SubrangeBound& b) const { - return !hasBound() || !b.hasBound() || - (hasBound() && b.hasBound() && getBound() <= b.getBound()); - } - - /** - * Is this SubrangeBound "greater than" another? For two - * SubrangeBounds that "have bounds," this is defined as expected. - * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a - * bound, b1 > b2 (but note also that b1 < b2). This strange - * behavior is due to the fact that a SubrangeBound without a bound - * is the representation for both +infinity and -infinity. - */ - bool operator>(const SubrangeBound& b) const { - return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - (hasBound() && b.hasBound() && getBound() < b.getBound()); - } - - /** - * Is this SubrangeBound "greater than or equal to" another? For - * two SubrangeBounds that "have bounds," this is defined as - * expected. For a finite SubrangeBound b1 and a SubrangeBounds b2 - * without a bound, b1 > b2 (but note also that b1 < b2). This - * strange behavior is due to the fact that a SubrangeBound without - * a bound is the representation for both +infinity and -infinity. - */ - bool operator>=(const SubrangeBound& b) const { - return !hasBound() || !b.hasBound() || - (hasBound() && b.hasBound() && getBound() <= b.getBound()); - } - - static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b) { - if (a.hasBound() && b.hasBound()) { - return SubrangeBound(Integer::min(a.getBound(), b.getBound())); - } else { - return SubrangeBound(); - } - } - - static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b) { - if (a.hasBound() && b.hasBound()) { - return SubrangeBound(Integer::max(a.getBound(), b.getBound())); - } else { - return SubrangeBound(); - } - } - - private: - bool d_nobound; - Integer d_bound; -}; /* class SubrangeBound */ - -class CVC4_PUBLIC SubrangeBounds { - public: - SubrangeBound lower; - SubrangeBound upper; - - SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u); - - bool operator==(const SubrangeBounds& bounds) const { - return lower == bounds.lower && upper == bounds.upper; - } - - bool operator!=(const SubrangeBounds& bounds) const { - return !(*this == bounds); - } - - /** - * Is this pair of SubrangeBounds "less than" (contained inside) the - * given pair of SubrangeBounds? Think of this as a subtype - * relation, e.g., [0,2] < [0,3] - */ - bool operator<(const SubrangeBounds& bounds) const { - return (lower > bounds.lower && upper <= bounds.upper) || - (lower >= bounds.lower && upper < bounds.upper); - } - - /** - * Is this pair of SubrangeBounds "less than or equal" (contained - * inside) the given pair of SubrangeBounds? Think of this as a - * subtype relation, e.g., [0,2] < [0,3] - */ - bool operator<=(const SubrangeBounds& bounds) const { - return lower >= bounds.lower && upper <= bounds.upper; - } - - /** - * Is this pair of SubrangeBounds "greater than" (does it contain) - * the given pair of SubrangeBounds? Think of this as a supertype - * relation, e.g., [0,3] > [0,2] - */ - bool operator>(const SubrangeBounds& bounds) const { - return (lower < bounds.lower && upper >= bounds.upper) || - (lower <= bounds.lower && upper > bounds.upper); - } - - /** - * Is this pair of SubrangeBounds "greater than" (does it contain) - * the given pair of SubrangeBounds? Think of this as a supertype - * relation, e.g., [0,3] > [0,2] - */ - bool operator>=(const SubrangeBounds& bounds) const { - return lower <= bounds.lower && upper >= bounds.upper; - } - - /** - * Returns true if the join of two subranges is not (- infinity, + infinity). - */ - static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b); - - /** - * Returns the join of two subranges, a and b. - * precondition: joinIsBounded(a,b) is true - */ - static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b); - -}; /* class SubrangeBounds */ - -struct CVC4_PUBLIC SubrangeBoundsHashFunction { - inline size_t operator()(const SubrangeBounds& bounds) const { - // We use Integer::hash() rather than Integer::getUnsignedLong() - // because the latter might overflow and throw an exception - size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() - : std::numeric_limits::max(); - size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() - : std::numeric_limits::max(); - return l + 0x9e3779b9 + (u << 6) + (u >> 2); - } -}; /* struct SubrangeBoundsHashFunction */ - -inline std::ostream& operator<<(std::ostream& out, - const SubrangeBound& bound) CVC4_PUBLIC; - -inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) { - if (bound.hasBound()) { - out << bound.getBound(); - } else { - out << '_'; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, - const SubrangeBounds& bounds) CVC4_PUBLIC; - -} /* CVC4 namespace */ - -#endif /* __CVC4__SUBRANGE_BOUND_H */ diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i deleted file mode 100644 index c12bd11e4..000000000 --- a/src/util/subrange_bound.i +++ /dev/null @@ -1,24 +0,0 @@ -%{ -#include "util/subrange_bound.h" -%} - -%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const; -%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const; -%rename(less) CVC4::SubrangeBound::operator<(const SubrangeBound&) const; -%rename(lessEqual) CVC4::SubrangeBound::operator<=(const SubrangeBound&) const; -%rename(greater) CVC4::SubrangeBound::operator>(const SubrangeBound&) const; -%rename(greaterEqual) CVC4::SubrangeBound::operator>=(const SubrangeBound&) const; - -%rename(equals) CVC4::SubrangeBounds::operator==(const SubrangeBounds&) const; -%ignore CVC4::SubrangeBounds::operator!=(const SubrangeBounds&) const; -%rename(less) CVC4::SubrangeBounds::operator<(const SubrangeBounds&) const; -%rename(lessEqual) CVC4::SubrangeBounds::operator<=(const SubrangeBounds&) const; -%rename(greater) CVC4::SubrangeBounds::operator>(const SubrangeBounds&) const; -%rename(greaterEqual) CVC4::SubrangeBounds::operator>=(const SubrangeBounds&) const; - -%rename(apply) CVC4::SubrangeBoundsHashFunction::operator()(const SubrangeBounds&) const; - -%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&); -%ignore CVC4::operator<<(std::ostream&, const SubrangeBounds&); - -%include "util/subrange_bound.h" diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index af1d9ab48..76aa3d8af 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -142,40 +142,6 @@ public: TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7))); TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7))); TS_ASSERT( ! te.isFinished() ); -/* - // subrange bounded only below - te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(0)), SubrangeBound()))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0))); - for(int i = 1; i <= 100; ++i) { - TS_ASSERT( ! (++te).isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i))); - } - TS_ASSERT( ! te.isFinished() ); - - // subrange bounded only above - te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(), SubrangeBound(Integer(-5))))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5))); - for(int i = 1; i <= 100; ++i) { - TS_ASSERT( ! (++te).isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5 - i))); - } - TS_ASSERT( ! te.isFinished() ); - - // finite subrange - te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(-10)), SubrangeBound(Integer(15))))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-10))); - for(int i = -9; i <= 15; ++i) { - TS_ASSERT( ! (++te).isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i))); - } - TS_ASSERT( (++te).isFinished() ); - TS_ASSERT_THROWS(*te, NoMoreValuesException); -std::cout<<"here\n"; - TS_ASSERT_THROWS(*++te, NoMoreValuesException); - */ } void testDatatypesFinite() { -- cgit v1.2.3