diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-18 21:53:36 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-18 21:53:36 +0000 |
| commit | 8f9f549059060402e00cbc8e7725eb1ed758bfdc (patch) | |
| tree | 58783604e659fd45dce3d0a1928f6bab9dda0af1 /src/parser/cvc | |
| parent | a441252481616ff4851f208caffce826a026ae30 (diff) | |
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.)
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
1 files changed, 3 insertions, 1 deletions
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 */ |