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/expr | |
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/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 10 | ||||
-rw-r--r-- | src/expr/type.cpp | 8 | ||||
-rw-r--r-- | src/expr/type.h | 12 |
4 files changed, 27 insertions, 7 deletions
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. |