diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 10 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 70 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 33 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 3 | ||||
-rw-r--r-- | src/expr/node.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 65 | ||||
-rw-r--r-- | src/expr/node_manager.h | 37 | ||||
-rw-r--r-- | src/expr/type.cpp | 61 | ||||
-rw-r--r-- | src/expr/type.h | 60 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 164 | ||||
-rw-r--r-- | src/expr/type_node.h | 194 |
11 files changed, 536 insertions, 163 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8d089901b..3dac28e11 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -494,10 +494,14 @@ Expr DefineFunctionCommand::getFormula() const throw() { void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { //Dump("declarations") << *this << endl; -- done by SmtEngine - if(!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); + try { + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } - d_commandStatus = CommandSuccess::instance(); } Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 46a7bb82c..533a4dd7f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -97,24 +97,33 @@ ExprManager::ExprManager(const Options& options) : #endif } -ExprManager::~ExprManager() { -#ifdef CVC4_STATISTICS_ON +ExprManager::~ExprManager() throw() { NodeManagerScope nms(d_nodeManager); - for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { - if (d_exprStatistics[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatistics[i]); - delete d_exprStatistics[i]; + + try { + +#ifdef CVC4_STATISTICS_ON + for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { + if (d_exprStatistics[i] != NULL) { + StatisticsRegistry::unregisterStat(d_exprStatistics[i]); + delete d_exprStatistics[i]; + } } - } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { - if (d_exprStatisticsVars[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]); - delete d_exprStatisticsVars[i]; + for (unsigned i = 0; i <= LAST_TYPE; ++ i) { + if (d_exprStatisticsVars[i] != NULL) { + StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]); + delete d_exprStatisticsVars[i]; + } } - } #endif - delete d_nodeManager; - delete d_ctxt; + + delete d_nodeManager; + delete d_ctxt; + + } catch(Exception& e) { + Warning() << "CVC4 threw an exception during cleanup." << std::endl + << e << std::endl; + } } const Options* ExprManager::getOptions() const { @@ -697,6 +706,39 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } +Type ExprManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return SubrangeType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSubrangeType(bounds)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + /** * Get the type for the given Expr and optionally do type checking. * diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2abd05821..bf9bfbb38 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -26,6 +26,7 @@ #include "expr/kind.h" #include "expr/type.h" #include "expr/expr.h" +#include "util/subrange_bound.h" ${includes} @@ -33,7 +34,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 37 "${template}" +#line 38 "${template}" namespace CVC4 { @@ -119,7 +120,7 @@ public: * any expression references that used to be managed by this expression * manager and are left-over are bad. */ - ~ExprManager(); + ~ExprManager() throw(); /** Get this node manager's options */ const Options* getOptions() const; @@ -403,9 +404,34 @@ public: SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingException 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. + */ + Type mkPredicateSubtype(Expr lambda) + throw(TypeCheckingException); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingException can be thrown if lambda is not + * 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); + + /** + * Make an integer subrange type as defined by the argument. + */ + Type mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException); + /** Get the type of an expression */ Type getType(Expr e, bool check = false) - throw (TypeCheckingException); + throw(TypeCheckingException); // variables are special, because duplicates are permitted Expr mkVar(const std::string& name, Type type); @@ -421,6 +447,7 @@ public: /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + };/* class ExprManager */ ${mkConst_instantiations} diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index c510ce381..d0f5fde9e 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -76,7 +76,8 @@ TypeCheckingException::~TypeCheckingException() throw() { } void TypeCheckingException::toStream(std::ostream& os) const throw() { - os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; + os << "Error during type checking: " << d_msg << endl + << "The ill-typed expression: " << *d_expr; } Expr TypeCheckingException::getExpression() const throw() { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 695e572ab..e303a9e58 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -36,7 +36,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { } void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { - os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node; + os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node; } NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c647e128c..a2fddadfc 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -29,6 +29,7 @@ #include <algorithm> #include <stack> +#include <utility> #include <ext/hash_set> using namespace std; @@ -235,14 +236,15 @@ void NodeManager::reclaimZombies() { }/* NodeManager::reclaimZombies() */ TypeNode NodeManager::getType(TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - // Many theories' type checkers call Node::getType() directly. - // This is incorrect, since "this" might not be the caller's - // curent node manager. Rather than force the individual typecheckers - // not to do this (by policy, which would be imperfect and lead - // to hard-to-find bugs, which it has in the past), we just - // set this node manager to be current for the duration of this - // check. + throw(TypeCheckingExceptionPrivate, AssertionException) { + + // Many theories' type checkers call Node::getType() directly. This + // is incorrect, since "this" might not be the caller's curent node + // manager. Rather than force the individual typecheckers not to do + // this (by policy, which would be imperfect and lead to + // hard-to-find bugs, which it has in the past), we just set this + // node manager to be current for the duration of this check. + // NodeManagerScope nms(this); TypeNode typeNode; @@ -321,4 +323,51 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } +TypeNode NodeManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda))); +} + +TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda, witness))); +} + +TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate) { + return TypeNode(mkTypeConst(bounds)); +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 704e930b5..da999cc82 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -38,6 +38,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" +#include "util/subrange_bound.h" #include "util/configuration_private.h" #include "util/tls.h" #include "util/options.h" @@ -662,6 +663,31 @@ public: inline 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 @@ -687,7 +713,7 @@ public: * (default: false) */ TypeNode getType(TNode n, bool check = false) - throw (TypeCheckingExceptionPrivate, AssertionException); + throw(TypeCheckingExceptionPrivate, AssertionException); /** * Convert a node to an expression. Uses the ExprManager @@ -944,10 +970,15 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { - CheckArgument(!indexType.isFunctionLike(), domain, + CheckArgument(!indexType.isNull(), indexType, + "unexpected NULL index type"); + CheckArgument(!constituentType.isNull(), constituentType, + "unexpected NULL constituent type"); + CheckArgument(!indexType.isFunctionLike(), indexType, "cannot index arrays by a function-like type"); - CheckArgument(!constituentType.isFunctionLike(), domain, + CheckArgument(!constituentType.isFunctionLike(), constituentType, "cannot store function-like types in arrays"); +Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index a901af73a..eaf10ba20 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -103,26 +103,32 @@ Type& Type::operator=(const Type& t) { } bool Type::operator==(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode == *t.d_typeNode; } bool Type::operator!=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode != *t.d_typeNode; } bool Type::operator<(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode < *t.d_typeNode; } bool Type::operator<=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode <= *t.d_typeNode; } bool Type::operator>(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode > *t.d_typeNode; } bool Type::operator>=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode >= *t.d_typeNode; } @@ -375,13 +381,39 @@ bool Type::isSortConstructor() const { return d_typeNode->isSortConstructor(); } -/** Cast to a sort type */ +/** Cast to a sort constructor type */ Type::operator SortConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isNull() || isSortConstructor()); return SortConstructorType(*this); } +/** Is this a predicate subtype */ +bool Type::isPredicateSubtype() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isPredicateSubtype(); +} + +/** Cast to a predicate subtype */ +Type::operator PredicateSubtype() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isPredicateSubtype()); + return PredicateSubtype(*this); +} + +/** Is this an integer subrange */ +bool Type::isSubrange() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSubrange(); +} + +/** Cast to a predicate subtype */ +Type::operator SubrangeType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isSubrange()); + return SubrangeType(*this); +} + /** Is this a kind type (i.e., the type of a type)? */ bool Type::isKind() const { NodeManagerScope nms(d_nodeManager); @@ -543,6 +575,18 @@ SortConstructorType::SortConstructorType(const Type& t) Assert(isNull() || isSortConstructor()); } +PredicateSubtype::PredicateSubtype(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isNull() || isPredicateSubtype()); +} + +SubrangeType::SubrangeType(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isNull() || isSubrange()); +} + unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } @@ -648,6 +692,21 @@ BooleanType TesterType::getRangeType() const { return BooleanType(makeType(d_nodeManager->booleanType())); } +Expr PredicateSubtype::getPredicate() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubtypePredicate().toExpr(); +} + +Type PredicateSubtype::getBaseType() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubtypeBaseType().toType(); +} + +SubrangeBounds SubrangeType::getSubrangeBounds() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubrangeBounds(); +} + size_t TypeHashFunction::operator()(const Type& t) const { return TypeNodeHashFunction()(NodeManager::fromType(t)); } diff --git a/src/expr/type.h b/src/expr/type.h index 34cc925f6..76fccb37b 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -28,6 +28,7 @@ #include "util/Assert.h" #include "util/cardinality.h" +#include "util/subrange_bound.h" namespace CVC4 { @@ -60,6 +61,8 @@ class TupleType; class KindType; class SortType; class SortConstructorType; +class PredicateSubtype; +class SubrangeType; class Type; /** Strategy for hashing Types */ @@ -405,6 +408,30 @@ public: operator SortConstructorType() const throw(AssertionException); /** + * Is this a predicate subtype? + * @return true if this is a predicate subtype + */ + bool isPredicateSubtype() const; + + /** + * Cast this type to a predicate subtype + * @return the predicate subtype + */ + operator PredicateSubtype() const throw(AssertionException); + + /** + * Is this an integer subrange type? + * @return true if this is an integer subrange type + */ + bool isSubrange() const; + + /** + * Cast this type to an integer subrange type + * @return the integer subrange type + */ + operator SubrangeType() const throw(AssertionException); + + /** * Is this a kind type (i.e., the type of a type)? * @return true if this is a kind type */ @@ -574,6 +601,39 @@ public: };/* class SortConstructorType */ /** + * Class encapsulating a predicate subtype. + */ +class CVC4_PUBLIC PredicateSubtype : public Type { + +public: + + /** Construct from the base type */ + PredicateSubtype(const Type& type = Type()) throw(AssertionException); + + /** Get the LAMBDA defining this predicate subtype */ + Expr getPredicate() const; + + /** Get the base type of this predicate subtype */ + Type getBaseType() const; + +};/* class PredicateSubtype */ + +/** + * Class encapsulating an integer subrange type. + */ +class CVC4_PUBLIC SubrangeType : public Type { + +public: + + /** Construct from the base type */ + SubrangeType(const Type& type = Type()) throw(AssertionException); + + /** Get the bounds defining this integer subrange */ + SubrangeBounds getSubrangeBounds() const; + +};/* class SubrangeType */ + +/** * Class encapsulating the kind type (the type of types). */ class CVC4_PUBLIC KindType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 77203bbb5..8cfb6387a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -71,68 +71,45 @@ Node TypeNode::mkGroundTerm() const { return kind::mkGroundTerm(*this); } -bool TypeNode::isBoolean() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst<TypeConstant>() == BOOLEAN_TYPE || - getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isInteger() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst<TypeConstant>() == INTEGER_TYPE || - getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isReal() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst<TypeConstant>() == REAL_TYPE || - getConst<TypeConstant>() == INTEGER_TYPE || - getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isPseudoboolean() const { - return getKind() == kind::TYPE_CONSTANT && - getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE; -} - -bool TypeNode::isString() const { - return getKind() == kind::TYPE_CONSTANT && - getConst<TypeConstant>() == STRING_TYPE; -} - -bool TypeNode::isArray() const { - return getKind() == kind::ARRAY_TYPE; -} - -TypeNode TypeNode::getArrayIndexType() const { - Assert(isArray()); - return (*this)[0]; -} - -TypeNode TypeNode::getArrayConstituentType() const { - Assert(isArray()); - return (*this)[1]; -} - -TypeNode TypeNode::getConstructorRangeType() const { - Assert(isConstructor()); - return (*this)[getNumChildren()-1]; -} - -bool TypeNode::isFunction() const { - return getKind() == kind::FUNCTION_TYPE; +bool TypeNode::isSubtypeOf(TypeNode t) const { + if(*this == t) { + return true; + } + if(getKind() == kind::TYPE_CONSTANT) { + switch(getConst<TypeConstant>()) { + case PSEUDOBOOLEAN_TYPE: + return t.getKind() == kind::TYPE_CONSTANT && + ( t.getConst<TypeConstant>() == BOOLEAN_TYPE || + t.getConst<TypeConstant>() == INTEGER_TYPE ); + case INTEGER_TYPE: + return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE; + default: + return false; + } + } + if(isSubrange()) { + if(t.isSubrange()) { + return t.getSubrangeBounds() <= getSubrangeBounds(); + } else { + return t.getKind() == kind::TYPE_CONSTANT && + ( t.getConst<TypeConstant>() == INTEGER_TYPE || + t.getConst<TypeConstant>() == REAL_TYPE ); + } + } + if(isPredicateSubtype()) { + return getSubtypeBaseType().isSubtypeOf(t); + } + return false; } -bool TypeNode::isFunctionLike() const { - return - getKind() == kind::FUNCTION_TYPE || - getKind() == kind::CONSTRUCTOR_TYPE || - getKind() == kind::SELECTOR_TYPE || - getKind() == kind::TESTER_TYPE; +Node TypeNode::getSubtypePredicate() const { + Assert(isPredicateSubtype()); + return Node::fromExpr(getConst<Predicate>()); } -bool TypeNode::isPredicate() const { - return isFunction() && getRangeType().isBoolean(); +TypeNode TypeNode::getSubtypeBaseType() const { + Assert(isPredicateSubtype()); + return getSubtypePredicate().getType().getArgTypes()[0]; } std::vector<TypeNode> TypeNode::getArgTypes() const { @@ -158,19 +135,6 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { return params; } -TypeNode TypeNode::getRangeType() const { - if(isTester()) { - return NodeManager::currentNM()->booleanType(); - } - Assert(isFunction() || isConstructor() || isSelector()); - return (*this)[getNumChildren()-1]; -} - -/** Is this a tuple type? */ -bool TypeNode::isTuple() const { - return getKind() == kind::TUPLE_TYPE; -} - /** Is this a tuple type? */ vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); @@ -181,37 +145,6 @@ vector<TypeNode> TypeNode::getTupleTypes() const { return types; } -/** Is this a sort kind */ -bool TypeNode::isSort() const { - return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()); -} - -/** Is this a sort constructor kind */ -bool TypeNode::isSortConstructor() const { - return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); -} - -/** Is this a kind type (i.e., the type of a type)? */ -bool TypeNode::isKind() const { - return getKind() == kind::TYPE_CONSTANT && - getConst<TypeConstant>() == KIND_TYPE; -} - -/** Is this a bit-vector type */ -bool TypeNode::isBitVector() const { - return getKind() == kind::BITVECTOR_TYPE; -} - -/** Is this a datatype type */ -bool TypeNode::isDatatype() const { - return getKind() == kind::DATATYPE_TYPE; -} - -/** Is this a parametric datatype type */ -bool TypeNode::isParametricDatatype() const { - return getKind() == kind::PARAMETRIC_DATATYPE; -} - /** Is this an instantiated datatype type */ bool TypeNode::isInstantiatedDatatype() const { if(getKind() == kind::DATATYPE_TYPE) { @@ -239,31 +172,4 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1]; } -/** Is this a constructor type */ -bool TypeNode::isConstructor() const { - return getKind() == kind::CONSTRUCTOR_TYPE; -} - -/** Is this a selector type */ -bool TypeNode::isSelector() const { - return getKind() == kind::SELECTOR_TYPE; -} - -/** Is this a tester type */ -bool TypeNode::isTester() const { - return getKind() == kind::TESTER_TYPE; -} - -/** Is this a bit-vector type of size <code>size</code> */ -bool TypeNode::isBitVector(unsigned size) const { - return getKind() == kind::BITVECTOR_TYPE && - getConst<BitVectorSize>() == size; -} - -/** Get the size of this bit-vector type */ -unsigned TypeNode::getBitVectorSize() const { - Assert(isBitVector()); - return getConst<BitVectorSize>(); -} - }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index c7da5ceb7..f59ce2dfe 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -447,6 +447,9 @@ public: */ Node mkGroundTerm() const; + /** Is this type a subtype of the given type? */ + bool isSubtypeOf(TypeNode t) const; + /** Is this the Boolean type? */ bool isBoolean() const; @@ -519,6 +522,16 @@ public: */ bool isPredicate() const; + /** + * Is this a predicate-LIKE type? Predicate-like things + * (e.g. datatype testers) that aren't actually predicates ARE + * considered predicates, here. + * + * Arrays are explicitly *not* predicate-like for the purposes of + * this test. + */ + bool isPredicateLike() const; + /** Is this a tuple type? */ bool isTuple() const; @@ -561,6 +574,21 @@ public: /** Is this a sort constructor kind */ bool isSortConstructor() const; + /** Is this a subtype predicate */ + bool isPredicateSubtype() const; + + /** Get the predicate defining this subtype */ + Node getSubtypePredicate() const; + + /** Get the base type of this subtype */ + TypeNode getSubtypeBaseType() const; + + /** Is this a subrange */ + bool isSubrange() const; + + /** Get the bounds defining this subrange */ + const SubrangeBounds& getSubrangeBounds() const; + /** Is this a kind type (i.e., the type of a type)? */ bool isKind() const; @@ -755,6 +783,172 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const { d_nv->printAst(out, indent); } +inline bool TypeNode::isBoolean() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) || + isPseudoboolean() || + ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() ); +} + +inline bool TypeNode::isInteger() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) || + isSubrange() || + isPseudoboolean() || + ( isPredicateSubtype() && getSubtypeBaseType().isInteger() ); +} + +inline bool TypeNode::isReal() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) || + isInteger() || + ( isPredicateSubtype() && getSubtypeBaseType().isReal() ); +} + +inline bool TypeNode::isPseudoboolean() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) || + ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() ); +} + +inline bool TypeNode::isString() const { + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == STRING_TYPE; +} + +inline bool TypeNode::isArray() const { + return getKind() == kind::ARRAY_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() ); +} + +inline TypeNode TypeNode::getArrayIndexType() const { + Assert(isArray()); + return (*this)[0]; +} + +inline TypeNode TypeNode::getArrayConstituentType() const { + Assert(isArray()); + return (*this)[1]; +} + +inline TypeNode TypeNode::getConstructorRangeType() const { + Assert(isConstructor()); + return (*this)[getNumChildren()-1]; +} + +inline bool TypeNode::isFunction() const { + return getKind() == kind::FUNCTION_TYPE; +} + +inline bool TypeNode::isFunctionLike() const { + return + getKind() == kind::FUNCTION_TYPE || + getKind() == kind::CONSTRUCTOR_TYPE || + getKind() == kind::SELECTOR_TYPE || + getKind() == kind::TESTER_TYPE; +} + +inline bool TypeNode::isPredicate() const { + return isFunction() && getRangeType().isBoolean(); +} + +inline bool TypeNode::isPredicateLike() const { + return isFunctionLike() && getRangeType().isBoolean(); +} + +inline TypeNode TypeNode::getRangeType() const { + if(isTester()) { + return NodeManager::currentNM()->booleanType(); + } + Assert(isFunction() || isConstructor() || isSelector()); + return (*this)[getNumChildren() - 1]; +} + +/** Is this a tuple type? */ +inline bool TypeNode::isTuple() const { + return getKind() == kind::TUPLE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isTuple() ); +} + +/** Is this a sort kind */ +inline bool TypeNode::isSort() const { + return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || + ( isPredicateSubtype() && getSubtypeBaseType().isSort() ); +} + +/** Is this a sort constructor kind */ +inline bool TypeNode::isSortConstructor() const { + return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); +} + +/** Is this a predicate subtype */ +inline bool TypeNode::isPredicateSubtype() const { + return getKind() == kind::SUBTYPE_TYPE; +} + +/** Is this a subrange type */ +inline bool TypeNode::isSubrange() const { + return getKind() == kind::SUBRANGE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() ); +} + +/** Is this a kind type (i.e., the type of a type)? */ +inline bool TypeNode::isKind() const { + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == KIND_TYPE; +} + +/** Is this a bit-vector type */ +inline bool TypeNode::isBitVector() const { + return getKind() == kind::BITVECTOR_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isBitVector() ); +} + +/** Is this a datatype type */ +inline bool TypeNode::isDatatype() const { + return getKind() == kind::DATATYPE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isDatatype() ); +} + +/** Is this a parametric datatype type */ +inline bool TypeNode::isParametricDatatype() const { + return getKind() == kind::PARAMETRIC_DATATYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isParametricDatatype() ); +} + +/** Is this a constructor type */ +inline bool TypeNode::isConstructor() const { + return getKind() == kind::CONSTRUCTOR_TYPE; +} + +/** Is this a selector type */ +inline bool TypeNode::isSelector() const { + return getKind() == kind::SELECTOR_TYPE; +} + +/** Is this a tester type */ +inline bool TypeNode::isTester() const { + return getKind() == kind::TESTER_TYPE; +} + +/** Is this a bit-vector type of size <code>size</code> */ +inline bool TypeNode::isBitVector(unsigned size) const { + return + ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) || + ( isPredicateSubtype() && getSubtypeBaseType().isBitVector(size) ); +} + +/** Get the size of this bit-vector type */ +inline unsigned TypeNode::getBitVectorSize() const { + Assert(isBitVector()); + return getConst<BitVectorSize>(); +} + +inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { + Assert(isSubrange()); + return getConst<SubrangeBounds>(); +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used |