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

2 files changed, 3 insertions, 33 deletions

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 */