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).

10 files changed, 23 insertions, 138 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 */
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 4d3112129..2dbc5affd 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -36,8 +36,7 @@ struct ArraySelectTypeRule {
         throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
       }
       TypeNode indexType = n[1].getType(check);
-      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
-      //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
+      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ 
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
       }
     }
@@ -56,12 +55,10 @@ struct ArrayStoreTypeRule {
         }
         TypeNode indexType = n[1].getType(check);
         TypeNode valueType = n[2].getType(check);
-        if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
-        //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
+        if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
           throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
         }
-        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){  
-        //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){  //FIXME:typing
+        if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
           Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
           Debug("array-types") << "value types: " << valueType << std::endl;
           throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 0ebebf1dd..12e897189 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -336,17 +336,4 @@ typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
-constant SUBTYPE_TYPE \
-    ::CVC4::Predicate \
-    ::CVC4::PredicateHashFunction \
-    "expr/predicate.h" \
-    "predicate subtype; payload is an instance of the CVC4::Predicate class"
-cardinality SUBTYPE_TYPE \
-    "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-well-founded SUBTYPE_TYPE \
-    "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-
 endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 7f86c7d0d..d8893d441 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -77,6 +77,9 @@ class EqualityTypeRule {
       TypeNode lhsType = n[0].getType(check);
       TypeNode rhsType = n[1].getType(check);
 
+      // TODO : we may want to limit cases where we have equalities between terms of different types 
+      //   equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets
+      //   one possibility is to only allow this for Int/Real
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
         ss << "Subexpressions must have a common base type:" << std::endl;
@@ -299,26 +302,6 @@ public:
   }
 };/* class SExprProperties */
 
-class SubtypeProperties {
-public:
-
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Computing the cardinality for predicate subtype not yet supported.");
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Computing the well-foundedness for predicate subtype not yet supported.");
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Constructing a ground term for predicate subtype not yet supported.");
-  }
-
-};/* class SubtypeProperties */
-
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 82d7274fa..e787ebc49 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -79,8 +79,7 @@ struct DatatypeConstructorTypeRule {
           Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
                                  << (*tchild_it) << std::endl;
           TypeNode argumentType = *tchild_it;
-          if (!childType.isComparableTo(argumentType)) {
-          //if (!childType.isSubtypeOf(argumentType)) {   //FIXME:typing
+          if (!childType.isSubtypeOf(argumentType)) { 
             std::stringstream ss;
             ss << "bad type for constructor argument:\n"
                << "child type:  " << childType << "\n"
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 1fd5f08be..23b185230 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -115,6 +115,21 @@ struct MemberTypeRule {
         throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
       }
       TypeNode elementType = n[0].getType(check);
+      // TODO : still need to be flexible here due to situations like:
+      //
+      // T : (Set Int)
+      // S : (Set Real)
+      // (= (as T (Set Real)) S)
+      // (member 0.5 S)
+      // ...where (member 0.5 T) is inferred
+      //
+      // or
+      //
+      // S : (Set Real)
+      // (not (member 0.5 s))
+      // (member 0.0 s)
+      // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0)))
+      //      
       if(!elementType.isComparableTo(setType.getSetElementType())) {
       //if(!elementType.isSubtypeOf(setType.getSetElementType())) {     //FIXME:typing
         std::stringstream ss;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3ddb18754..82607a165 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -243,9 +243,6 @@ public:
   static inline TheoryId theoryOf(TypeNode typeNode) {
     Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
-    while (typeNode.isPredicateSubtype()) {
-      typeNode = typeNode.getSubtypeParentType();
-    }
     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
     } else {
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index a3c775a2a..c31de403c 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -45,8 +45,7 @@ class UfTypeRule {
            ++argument_it, ++argument_type_it) {
         TypeNode currentArgument = (*argument_it).getType();
         TypeNode currentArgumentType = *argument_type_it;
-        if (!currentArgument.isComparableTo(currentArgumentType)) {
-        //if (!currentArgument.isSubtypeOf(currentArgumentType)) {   //FIXME:typing
+        if (!currentArgument.isSubtypeOf(currentArgumentType)) { 
           std::stringstream ss;
           ss << "argument type is not a subtype of the function's argument "
              << "type:\n"