Disable predicate subtyping:

* remove from public interface (ExprManager, Type)
* CVC parser reports an unimplemented feature error if used

I didn't want to tear it out completely (from NodeManager, TypeNode,
type-checking, pre-processing, etc.) because that's a lot of hassle
and we'll add it back in after the release anyway.  It *does* mean
that CVC4::Predicate is in the public interface, but that it can't be
used for anything (by users).

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 1dc8d37bdf342410f042537225b8084444c5e4b6..02d76d351b902a84aecf2d81213c521f5e9fffa3 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -197,7 +197,7 @@ bool Type::isBool() const {
 }
 
 bool Type::isSubtype() const {
-  return isPredicateSubtype();
+  return false;
 }
 
 Cardinality Type::card() const {
@@ -1075,11 +1075,14 @@ Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
 }
 
 Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
+  /*
   if(witness.isNull()) {
     return d_em->mkPredicateSubtype(pred);
   } else {
     return d_em->mkPredicateSubtype(pred, witness);
   }
+  */
 }
 
 Type ValidityChecker::tupleType(const Type& type0, const Type& type1) {
@@ -1276,20 +1279,7 @@ Type ValidityChecker::getBaseType(const Expr& e) {
 }
 
 Type ValidityChecker::getBaseType(const Type& t) {
-  Type type = t;
-  while(type.isPredicateSubtype()) {
-    type = CVC4::PredicateSubtype(type).getBaseType();
-  }
-  // We might still be a (primitive) subtype.  Check the types that can
-  // form the base of such a type.
-  if(type.isReal()) {
-    return d_em->realType();
-  }
-  assert(!type.isInteger());// should be handled by Real
-  if(type.isBoolean()) {
-    return d_em->booleanType();
-  }
-  return type;
+  return t.getBaseType();
 }
 
 Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) {

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 738529d92c50441ea1094fe2670626779d042f7d..cacfa92153f7b5c52b974f0266ffb4cdc25fec19 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -730,6 +730,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
+/* - not in release 1.0
 Type ExprManager::mkPredicateSubtype(Expr lambda)
   throw(TypeCheckingException) {
   NodeManagerScope nms(d_nodeManager);
@@ -740,7 +741,9 @@ Type ExprManager::mkPredicateSubtype(Expr lambda)
     throw TypeCheckingException(this, &e);
   }
 }
+*/
 
+/* - not in release 1.0
 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
   throw(TypeCheckingException) {
   NodeManagerScope nms(d_nodeManager);
@@ -751,6 +754,7 @@ Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
     throw TypeCheckingException(this, &e);
   }
 }
+*/
 
 Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
   throw(TypeCheckingException) {

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f38acd1530aa91a5d13cfeece692fab225e7da5d..561d99392880f80b1167de56896dafdc8ab38643 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -438,8 +438,9 @@ public:
    * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
    * the resulting predicate subtype is inhabited.
    */
-  Type mkPredicateSubtype(Expr lambda)
-    throw(TypeCheckingException);
+  // not in release 1.0
+  //Type mkPredicateSubtype(Expr lambda)
+  //  throw(TypeCheckingException);
 
   /**
    * Make a predicate subtype type defined by the given LAMBDA
@@ -448,8 +449,9 @@ public:
    * a LAMBDA, or is ill-typed, or if the witness is not a witness or
    * ill-typed.
    */
-  Type mkPredicateSubtype(Expr lambda, Expr witness)
-    throw(TypeCheckingException);
+  // not in release 1.0
+  //Type mkPredicateSubtype(Expr lambda, Expr witness)
+  //  throw(TypeCheckingException);
 
   /**
    * Make an integer subrange type as defined by the argument.

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index e64c202b41d65d77bc4d0f845dbecf26b5ca1dab..cb1e829c41f3ee91288cf9710b990b29f49d861b 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -402,17 +402,21 @@ Type::operator SortConstructorType() const throw(IllegalArgumentException) {
 }
 
 /** Is this a predicate subtype */
+/* - not in release 1.0
 bool Type::isPredicateSubtype() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isPredicateSubtype();
 }
+*/
 
 /** Cast to a predicate subtype */
+/* - not in release 1.0
 Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
   CheckArgument(isNull() || isPredicateSubtype(), this);
   return PredicateSubtype(*this);
 }
+*/
 
 /** Is this an integer subrange */
 bool Type::isSubrange() const {
@@ -582,11 +586,13 @@ SortConstructorType::SortConstructorType(const Type& t)
   CheckArgument(isNull() || isSortConstructor(), this);
 }
 
+/* - not in release 1.0
 PredicateSubtype::PredicateSubtype(const Type& t)
   throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isPredicateSubtype(), this);
 }
+*/
 
 SubrangeType::SubrangeType(const Type& t)
   throw(IllegalArgumentException) :
@@ -699,6 +705,7 @@ BooleanType TesterType::getRangeType() const {
   return BooleanType(makeType(d_nodeManager->booleanType()));
 }
 
+/* - not in release 1.0
 Expr PredicateSubtype::getPredicate() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getSubtypePredicate().toExpr();
@@ -708,6 +715,7 @@ Type PredicateSubtype::getParentType() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getSubtypeParentType().toType();
 }
+*/
 
 SubrangeBounds SubrangeType::getSubrangeBounds() const {
   NodeManagerScope nms(d_nodeManager);

diff --git a/src/expr/type.h b/src/expr/type.h
index f8a5f48fe8f32241b6c66a1c5c296810dbcb98e3..e5590aa5951595e15bf04ce4157011451d2ef0e2 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -57,7 +57,8 @@ class TupleType;
 class SExprType;
 class SortType;
 class SortConstructorType;
-class PredicateSubtype;
+// not in release 1.0
+//class PredicateSubtype;
 class SubrangeType;
 class Type;
 
@@ -421,13 +422,15 @@ public:
    * Is this a predicate subtype?
    * @return true if this is a predicate subtype
    */
-  bool isPredicateSubtype() const;
+  // not in release 1.0
+  //bool isPredicateSubtype() const;
 
   /**
    * Cast this type to a predicate subtype
    * @return the predicate subtype
    */
-  operator PredicateSubtype() const throw(IllegalArgumentException);
+  // not in release 1.0
+  //operator PredicateSubtype() const throw(IllegalArgumentException);
 
   /**
    * Is this an integer subrange type?
@@ -601,6 +604,8 @@ public:
 
 };/* class SortConstructorType */
 
+// not in release 1.0
+#if 0
 /**
  * Class encapsulating a predicate subtype.
  */
@@ -621,6 +626,7 @@ public:
   Type getParentType() const;
 
 };/* class PredicateSubtype */
+#endif /* 0 */
 
 /**
  * Class encapsulating an integer subrange type.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index a5f04aeb024f76434282413d4b2adcbc3796905c..18dfcd473e71efc850d9270672bdc55171e9038d 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1145,9 +1145,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
       PARSER_STATE->useDeclarationsFrom(symtab);
       delete old;*/
-      t = f2.isNull() ?
+      PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
+      /*t = f2.isNull() ?
         EXPR_MANAGER->mkPredicateSubtype(f) :
         EXPR_MANAGER->mkPredicateSubtype(f, f2);
+      */
     }
 
     /* subrange types */