From 8f9f549059060402e00cbc8e7725eb1ed758bfdc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 18 Nov 2012 21:53:36 +0000 Subject: [PATCH] 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.) --- src/compat/cvc3_compat.cpp | 20 +++++--------------- src/expr/expr_manager_template.cpp | 4 ++++ src/expr/expr_manager_template.h | 10 ++++++---- src/expr/type.cpp | 8 ++++++++ src/expr/type.h | 12 +++++++++--- src/parser/cvc/Cvc.g | 4 +++- 6 files changed, 35 insertions(+), 23 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) { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 738529d92..cacfa9215 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -730,6 +730,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } +/* - not in release 1.0 Type ExprManager::mkPredicateSubtype(Expr lambda) throw(TypeCheckingException) { NodeManagerScope nms(d_nodeManager); @@ -740,7 +741,9 @@ Type ExprManager::mkPredicateSubtype(Expr lambda) throw TypeCheckingException(this, &e); } } +*/ +/* - not in release 1.0 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) throw(TypeCheckingException) { NodeManagerScope nms(d_nodeManager); @@ -751,6 +754,7 @@ Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) throw TypeCheckingException(this, &e); } } +*/ Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds) throw(TypeCheckingException) { 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. diff --git a/src/expr/type.cpp b/src/expr/type.cpp index e64c202b4..cb1e829c4 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -402,17 +402,21 @@ Type::operator SortConstructorType() const throw(IllegalArgumentException) { } /** Is this a predicate subtype */ +/* - not in release 1.0 bool Type::isPredicateSubtype() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isPredicateSubtype(); } +*/ /** Cast to a predicate subtype */ +/* - not in release 1.0 Type::operator PredicateSubtype() const throw(IllegalArgumentException) { NodeManagerScope nms(d_nodeManager); CheckArgument(isNull() || isPredicateSubtype(), this); return PredicateSubtype(*this); } +*/ /** Is this an integer subrange */ bool Type::isSubrange() const { @@ -582,11 +586,13 @@ SortConstructorType::SortConstructorType(const Type& t) CheckArgument(isNull() || isSortConstructor(), this); } +/* - not in release 1.0 PredicateSubtype::PredicateSubtype(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isPredicateSubtype(), this); } +*/ SubrangeType::SubrangeType(const Type& t) throw(IllegalArgumentException) : @@ -699,6 +705,7 @@ BooleanType TesterType::getRangeType() const { return BooleanType(makeType(d_nodeManager->booleanType())); } +/* - not in release 1.0 Expr PredicateSubtype::getPredicate() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getSubtypePredicate().toExpr(); @@ -708,6 +715,7 @@ Type PredicateSubtype::getParentType() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getSubtypeParentType().toType(); } +*/ SubrangeBounds SubrangeType::getSubrangeBounds() const { NodeManagerScope nms(d_nodeManager); diff --git a/src/expr/type.h b/src/expr/type.h index f8a5f48fe..e5590aa59 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -57,7 +57,8 @@ class TupleType; class SExprType; class SortType; class SortConstructorType; -class PredicateSubtype; +// not in release 1.0 +//class PredicateSubtype; class SubrangeType; class Type; @@ -421,13 +422,15 @@ public: * Is this a predicate subtype? * @return true if this is a predicate subtype */ - bool isPredicateSubtype() const; + // not in release 1.0 + //bool isPredicateSubtype() const; /** * Cast this type to a predicate subtype * @return the predicate subtype */ - operator PredicateSubtype() const throw(IllegalArgumentException); + // not in release 1.0 + //operator PredicateSubtype() const throw(IllegalArgumentException); /** * Is this an integer subrange type? @@ -601,6 +604,8 @@ public: };/* class SortConstructorType */ +// not in release 1.0 +#if 0 /** * Class encapsulating a predicate subtype. */ @@ -621,6 +626,7 @@ public: Type getParentType() const; };/* class PredicateSubtype */ +#endif /* 0 */ /** * Class encapsulating an integer subrange type. 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 */ -- 2.30.2