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

1 files changed, 0 insertions, 25 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1d1150842..44c116558 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -875,31 +875,6 @@ public:
   TypeNode mkSortConstructor(const std::string& name, size_t arity);
 
   /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingExceptionPrivate can be thrown if
-   * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
-   * proving that the resulting predicate subtype is inhabited.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingExceptionPrivate can be thrown if lambda
-   * is not a LAMBDA, or is ill-typed, or if the witness is not a
-   * witness or ill-typed.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make an integer subrange type as defined by the argument.
-   */
-  TypeNode mkSubrangeType(const SubrangeBounds& bounds)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
    * Get the type for the given node and optionally do type checking.
    *
    * Initial type computation will be near-constant time if