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/compat/cvc3_compat.cpp | |
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/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 20 |
1 files changed, 5 insertions, 15 deletions
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) { |