From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 18 Nov 2012 21:53:36 +0000 (+0000)
Subject: Disable predicate subtyping:
X-Git-Tag: cvc5-1.0.0~7576
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f9f549059060402e00cbc8e7725eb1ed758bfdc;p=cvc5.git

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 1dc8d37bd..02d76d351 100644
--- 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 738529d92..cacfa9215 100644
--- 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 f38acd153..561d99392 100644
--- 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 e64c202b4..cb1e829c4 100644
--- 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 f8a5f48fe..e5590aa59 100644
--- 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 a5f04aeb0..18dfcd473 100644
--- 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 */