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.

14 files changed, 6 insertions, 421 deletions

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<CVC4::String>() == "_NEGINF";
-  bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF";
-  CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
-  CompatCheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
-  CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
-  CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().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<JavaInputStreamAdapter*> 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<CVC4::BitVectorSize>;
 %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
 %template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>;
-%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>;
 %template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>;
 %template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>;
 %template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>;
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<CVC4::BitVectorSize>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::SubrangeBounds>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
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 <stdint.h>
 
 #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;
@@ -563,18 +562,6 @@ namespace CVC4 {
        * 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.
-       */
       struct myExpr : public CVC4::Expr {
         myExpr() : CVC4::Expr() {}
         myExpr(void*) : CVC4::Expr() {}
@@ -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 <limits>
-
-#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 <limits>
-
-#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<size_t>::max();
-    size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash()
-                                       : std::numeric_limits<size_t>::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() {