Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).

3 files changed, 0 insertions, 92 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 0884083c0..34ae30f4c 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -51,19 +51,6 @@ sort INTEGER_TYPE \
         "expr/node_manager.h" \
     "integer type"
 
-constant SUBRANGE_TYPE \
-    ::CVC4::SubrangeBounds \
-    ::CVC4::SubrangeBoundsHashFunction \
-    "util/subrange_bound.h" \
-    "the type of an integer subrange"
-cardinality SUBRANGE_TYPE \
-    "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
-    "theory/arith/theory_arith_type_rules.h"
-well-founded SUBRANGE_TYPE \
-    true \
-    "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
-    "theory/arith/theory_arith_type_rules.h"
-
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashFunction \
@@ -76,9 +63,6 @@ enumerator REAL_TYPE \
 enumerator INTEGER_TYPE \
     "::CVC4::theory::arith::IntegerEnumerator" \
     "theory/arith/type_enumerator.h"
-enumerator SUBRANGE_TYPE \
-    "::CVC4::theory::arith::SubrangeEnumerator" \
-    "theory/arith/type_enumerator.h"
 
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 59c2aaa8f..db3ae65f2 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -171,33 +171,6 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
-
-class SubrangeProperties {
-public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
-    if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
-      return Cardinality::INTEGERS;
-    }
-    return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
-    if(bounds.lower.hasBound()) {
-      return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
-    }
-    if(bounds.upper.hasBound()) {
-      return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
-    }
-    return NodeManager::currentNM()->mkConst(Rational(0));
-  }
-};/* class SubrangeProperties */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 5d6b936a7..4cb34ed4a 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -108,55 +108,6 @@ public:
 
 };/* class IntegerEnumerator */
 
-class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
-  Integer d_int;
-  SubrangeBounds d_bounds;
-  bool d_direction;// true == +, false == -
-
-public:
-
-  SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<SubrangeEnumerator>(type),
-    d_int(0),
-    d_bounds(type.getConst<SubrangeBounds>()),
-    d_direction(d_bounds.lower.hasBound()) {
-
-    d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
-
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    // if we're counting down, there's no lower bound
-    Assert(d_direction || !d_bounds.lower.hasBound());
-  }
-
-  Node operator*() throw(NoMoreValuesException) {
-    if(isFinished()) {
-      throw NoMoreValuesException(getType());
-    }
-    return NodeManager::currentNM()->mkConst(Rational(d_int));
-  }
-
-  SubrangeEnumerator& operator++() throw() {
-    if(d_direction) {
-      if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
-        d_int += 1;
-      }
-    } else {
-      // if we're counting down, there's no lower bound
-      d_int -= 1;
-    }
-    return *this;
-  }
-
-  bool isFinished() throw() {
-    // if we're counting down, there's no lower bound
-    return d_direction &&
-      d_bounds.upper.hasBound() &&
-      d_int > d_bounds.upper.getBound();
-  }
-
-};/* class SubrangeEnumerator */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */