diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/expr/node_manager.h | |
parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) |
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).
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 25 |
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 |