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

1 files changed, 6 insertions, 4 deletions

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.