diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/expr | |
parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 3 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 39 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 45 | ||||
-rw-r--r-- | src/expr/node_manager.h | 25 | ||||
-rw-r--r-- | src/expr/predicate.cpp | 99 | ||||
-rw-r--r-- | src/expr/predicate.h | 72 | ||||
-rw-r--r-- | src/expr/predicate.i | 12 | ||||
-rw-r--r-- | src/expr/type.cpp | 33 | ||||
-rw-r--r-- | src/expr/type.h | 4 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 124 | ||||
-rw-r--r-- | src/expr/type_node.h | 78 |
12 files changed, 20 insertions, 518 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index e45c765c0..859d5a312 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -61,8 +61,6 @@ libexpr_la_SOURCES = \ variable_type_map.h \ datatype.h \ datatype.cpp \ - predicate.h \ - predicate.cpp \ record.cpp \ record.h \ uninterpreted_constant.cpp \ @@ -103,7 +101,6 @@ EXTRA_DIST = \ kind.i \ expr.i \ record.i \ - predicate.i \ variable_type_map.i \ uninterpreted_constant.i diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 735d531e1..d6249d6fd 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -842,43 +842,6 @@ 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); - try { - return PredicateSubtype(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkPredicateSubtype(lambda)))); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} -*/ - -/* - not in release 1.0 -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. * @@ -1062,8 +1025,6 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr return to->mkTypeConst(n.getConst<TypeConstant>()); } else if(n.getKind() == kind::BITVECTOR_TYPE) { return to->mkBitVectorType(n.getConst<BitVectorSize>()); - } else if(n.getKind() == kind::SUBRANGE_TYPE) { - return to->mkSubrangeType(n.getSubrangeBounds()); } Type from_t = from->toType(n); Type& to_t = vmap.d_typeMap[from_t]; diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 07dc88fd3..8719d8ef4 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -461,8 +461,8 @@ public: /** * Make an integer subrange type as defined by the argument. */ - Type mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingException); + //Type mkSubrangeType(const SubrangeBounds& bounds) + // throw(TypeCheckingException); /** Get the type of an expression */ Type getType(Expr e, bool check = false) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index b746e0de9..f7a1d98d6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -506,51 +506,6 @@ 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) { - stringstream ss; - ss << "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) { - stringstream ss; - ss << "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)); -} - TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { if( index==types.size() ){ if( d_data.isNull() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1d1150842..44c116558 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -875,31 +875,6 @@ public: 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 diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp deleted file mode 100644 index eaf587110..000000000 --- a/src/expr/predicate.cpp +++ /dev/null @@ -1,99 +0,0 @@ -/********************* */ -/*! \file predicate.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Representation of predicates for predicate subtyping - ** - ** Simple class to represent predicates for predicate subtyping. - ** Instances of this class are carried as the payload of - ** the CONSTANT-metakinded SUBTYPE_TYPE types. - **/ -#include "expr/predicate.h" - -#include "base/cvc4_assert.h" -#include "expr/expr.h" - - -using namespace std; - -namespace CVC4 { - -Predicate::Predicate(const Predicate& p) - : d_predicate(new Expr(p.getExpression())) - , d_witness(new Expr(p.getWitness())) -{} - -Predicate::Predicate(const Expr& e) throw(IllegalArgumentException) - : d_predicate(new Expr(e)) - , d_witness(new Expr()) -{ - PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); - PrettyCheckArgument(e.getType().isPredicate(), e, - "Expression given is not predicate"); - PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, - "Expression given is not predicate of a single argument"); -} - -Predicate::Predicate(const Expr& e, const Expr& w) - throw(IllegalArgumentException) - : d_predicate(new Expr(e)) - , d_witness(new Expr(w)) -{ - PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); - PrettyCheckArgument(e.getType().isPredicate(), e, - "Expression given is not predicate"); - PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, - "Expression given is not predicate of a single argument"); -} - -Predicate::~Predicate() { - delete d_predicate; - delete d_witness; -} - -Predicate& Predicate::operator=(const Predicate& p){ - (*d_predicate) = p.getExpression(); - (*d_witness) = p.getWitness(); - return *this; -} - - -// Predicate::operator Expr() const { -// return d_predicate; -// } - -const Expr& Predicate::getExpression() const { - return *d_predicate; -} - -const Expr& Predicate::getWitness() const { - return *d_witness; -} - -bool Predicate::operator==(const Predicate& p) const { - return getExpression() == p.getExpression() && - getWitness() == p.getWitness(); -} - -std::ostream& operator<<(std::ostream& out, const Predicate& p) { - out << p.getExpression(); - const Expr& witness = p.getWitness(); - if(! witness.isNull()) { - out << " : " << witness; - } - return out; -} - -size_t PredicateHashFunction::operator()(const Predicate& p) const { - ExprHashFunction h; - return h(p.getWitness()) * 5039 + h(p.getExpression()); -} - -}/* CVC4 namespace */ diff --git a/src/expr/predicate.h b/src/expr/predicate.h deleted file mode 100644 index 99e589fcd..000000000 --- a/src/expr/predicate.h +++ /dev/null @@ -1,72 +0,0 @@ -/********************* */ -/*! \file predicate.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Representation of predicates for predicate subtyping - ** - ** Simple class to represent predicates for predicate subtyping. - ** Instances of this class are carried as the payload of - ** the CONSTANT-metakinded SUBTYPE_TYPE types. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__PREDICATE_H -#define __CVC4__PREDICATE_H - -#include "base/exception.h" - -namespace CVC4 { - -class Predicate; - -std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC; - -struct CVC4_PUBLIC PredicateHashFunction { - size_t operator()(const Predicate& p) const; -};/* class PredicateHashFunction */ - -}/* CVC4 namespace */ - - -namespace CVC4 { -class CVC4_PUBLIC Expr; -}/* CVC4 namespace */ - - -namespace CVC4 { -class CVC4_PUBLIC Predicate { -public: - - Predicate(const Expr& e) throw(IllegalArgumentException); - Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException); - - Predicate(const Predicate& p); - ~Predicate(); - Predicate& operator=(const Predicate& p); - - //operator Expr() const; - - const Expr& getExpression() const; - const Expr& getWitness() const; - - bool operator==(const Predicate& p) const; - - friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p); - friend size_t PredicateHashFunction::operator()(const Predicate& p) const; - -private: - Expr* d_predicate; - Expr* d_witness; -};/* class Predicate */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__PREDICATE_H */ diff --git a/src/expr/predicate.i b/src/expr/predicate.i deleted file mode 100644 index aa80a98b5..000000000 --- a/src/expr/predicate.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "expr/predicate.h" -%} - -%rename(equals) CVC4::Predicate::operator==(const Predicate&) const; -%rename(toExpr) CVC4::Predicate::operator Expr() const; - -%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const; - -%ignore CVC4::operator<<(std::ostream&, const Predicate&); - -%include "expr/predicate.h" diff --git a/src/expr/type.cpp b/src/expr/type.cpp index bb3ce0f58..8bcb0f8d5 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -329,20 +329,6 @@ bool Type::isSortConstructor() const { return d_typeNode->isSortConstructor(); } -/** Is this a predicate subtype */ -/* - not in release 1.0 -bool Type::isPredicateSubtype() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isPredicateSubtype(); -} -*/ - -/** Is this an integer subrange */ -bool Type::isSubrange() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSubrange(); -} - size_t FunctionType::getArity() const { return d_typeNode->getNumChildren() - 1; } @@ -505,20 +491,6 @@ SortConstructorType::SortConstructorType(const Type& t) PrettyCheckArgument(isNull() || isSortConstructor(), this); } -/* - not in release 1.0 -PredicateSubtype::PredicateSubtype(const Type& t) - throw(IllegalArgumentException) : - Type(t) { - PrettyCheckArgument(isNull() || isPredicateSubtype(), this); -} -*/ - -SubrangeType::SubrangeType(const Type& t) - throw(IllegalArgumentException) : - Type(t) { - PrettyCheckArgument(isNull() || isSubrange(), this); -} - unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } @@ -666,11 +638,6 @@ Type PredicateSubtype::getParentType() const { } */ -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 04b2907ff..25f0c5436 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -372,7 +372,7 @@ public: * Is this an integer subrange type? * @return true if this is an integer subrange type */ - bool isSubrange() const; + //bool isSubrange() const; /** * Outputs a string representation of this type to the stream. @@ -584,7 +584,6 @@ public: Type getParentType() const; };/* class PredicateSubtype */ -#endif /* 0 */ /** * Class encapsulating an integer subrange type. @@ -600,6 +599,7 @@ public: SubrangeBounds getSubrangeBounds() const; };/* class SubrangeType */ +#endif /* 0 */ /** * Class encapsulating the bit-vector type. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 6e16ee9fa..383a31dd0 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -106,15 +106,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { 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(isTuple() && t.isTuple()) { const Datatype& dt1 = getDatatype(); const Datatype& dt2 = t.getDatatype(); @@ -151,9 +142,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } return true; } - if(isPredicateSubtype()) { - return getSubtypeParentType().isSubtypeOf(t); - } if(isSet() && t.isSet()) { return getSetElementType().isSubtypeOf(t.getSetElementType()); } @@ -205,28 +193,13 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isArray() && t.isArray()) { return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType()); } - //if(isPredicateSubtype()) { - // return t.isComparableTo(getSubtypeParentType()); - //} return false; } -Node TypeNode::getSubtypePredicate() const { - Assert(isPredicateSubtype()); - return Node::fromExpr(getConst<Predicate>().getExpression()); -} - -TypeNode TypeNode::getSubtypeParentType() const { - Assert(isPredicateSubtype()); - return getSubtypePredicate().getType().getArgTypes()[0]; -} - TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; - } else if (isPredicateSubtype()) { - return getSubtypeParentType().getBaseType(); } else if (isParametricDatatype()) { vector<Type> v; for(size_t i = 1; i < getNumChildren(); ++i) { @@ -264,14 +237,12 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { /** Is this a tuple type? */ bool TypeNode::isTuple() const { - return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) || - ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ); } /** Is this a record type? */ bool TypeNode::isRecord() const { - return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) || - ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ); } size_t TypeNode::getTupleLength() const { @@ -375,11 +346,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { return TypeNode(); // null type } default: - //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - // return t0; // t0 is a constant type - //} else { - return TypeNode(); // null type - //} + return TypeNode(); // null type } } else if(t1.getKind() == kind::TYPE_CONSTANT) { return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases @@ -394,11 +361,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - // return t0; - //} else { - return TypeNode(); - //} + return TypeNode(); case kind::FUNCTION_TYPE: return TypeNode(); // Not sure if this is right case kind::SET_TYPE: { @@ -423,47 +386,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::SEXPR_TYPE: Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); return TypeNode(); - case kind::SUBTYPE_TYPE: - //if(t1.isPredicateSubtype()){ - // // This is the case where both t0 and t1 are predicate subtypes. - // return leastCommonPredicateSubtype(t0, t1); - //}else{ // t0 is a predicate subtype and t1 is not - // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases - //} - return TypeNode(); - case kind::SUBRANGE_TYPE: - /* - if(t1.isSubrange()) { - const SubrangeBounds& t0SR = t0.getSubrangeBounds(); - const SubrangeBounds& t1SR = t1.getSubrangeBounds(); - if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) { - SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR); - return NodeManager::currentNM()->mkSubrangeType(j); - } else { - return NodeManager::currentNM()->integerType(); - } - } else if(t1.isPredicateSubtype()) { - // t0 is a subrange - // t1 is not a subrange - // t1 is a predicate subtype - if(t1.isInteger()) { - return NodeManager::currentNM()->integerType(); - } else if(t1.isReal()) { - return NodeManager::currentNM()->realType(); - } else { - return TypeNode(); - } - } else { - // t0 is a subrange - // t1 is not a subrange - // t1 is not a type constant && is not a predicate subtype - // t1 cannot be real subtype or integer. - Assert(t1.isReal()); - Assert(t1.isInteger()); - return TypeNode(); - } -*/ - return TypeNode(); case kind::DATATYPE_TYPE: if( t0.isTuple() && t1.isTuple() ){ const Datatype& dt1 = t0.getDatatype(); @@ -490,9 +412,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { if(!t1.isParametricDatatype()) { return TypeNode(); } - while(t1.getKind() != kind::PARAMETRIC_DATATYPE) { - t1 = t1.getSubtypeParentType(); - } if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { return TypeNode(); } @@ -508,38 +427,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { } } -TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ - Assert(t0.isPredicateSubtype()); - Assert(t1.isPredicateSubtype()); - - std::vector<TypeNode> t0stack; - t0stack.push_back(t0); - while(t0stack.back().isPredicateSubtype()){ - t0stack.push_back(t0stack.back().getSubtypeParentType()); - } - std::vector<TypeNode> t1stack; - t1stack.push_back(t1); - while(t1stack.back().isPredicateSubtype()){ - t1stack.push_back(t1stack.back().getSubtypeParentType()); - } - - Assert(!t0stack.empty()); - Assert(!t1stack.empty()); - - if(t0stack.back() == t1stack.back()){ - TypeNode mostGeneral = t1stack.back(); - t0stack.pop_back(); t1stack.pop_back(); - while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){ - mostGeneral = t0stack.back(); - t0stack.pop_back(); t1stack.pop_back(); - } - return mostGeneral; - }else{ - return leastCommonTypeNode(t0stack.back(), t1stack.back()); - } -} - - Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); Assert( ntn.isComparableTo( tn ) ); @@ -581,8 +468,7 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { /** Is this a sort kind */ bool TypeNode::isSort() const { - return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || - ( isPredicateSubtype() && getSubtypeParentType().isSort() ); + return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); } /** Is this a sort constructor kind */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1a8bb14ed..8dd80bc37 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -620,27 +620,9 @@ 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 parent type of this subtype; note that it could be - * another subtype. - */ - TypeNode getSubtypeParentType() const; - /** Get the most general base type of the type */ TypeNode getBaseType() const; - /** Is this a subrange */ - bool isSubrange() const; - - /** Get the bounds defining this subrange */ - const SubrangeBounds& getSubrangeBounds() const; - /** * Returns the leastUpperBound in the extended type lattice of the two types. * If this is \top, i.e. there is no inhabited type that contains both, @@ -657,13 +639,7 @@ public: static Node getEnsureTypeCondition( Node n, TypeNode tn ); private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); - - /** - * Returns the leastUpperBound in the extended type lattice of two - * predicate subtypes. - */ - static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1); - + /** * Indents the given stream a given amount of spaces. * @@ -852,22 +828,18 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const { inline bool TypeNode::isBoolean() const { return - ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) || - ( isPredicateSubtype() && getSubtypeParentType().isBoolean() ); + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ); } inline bool TypeNode::isInteger() const { return - ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) || - isSubrange() || - ( isPredicateSubtype() && getSubtypeParentType().isInteger() ); + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ); } inline bool TypeNode::isReal() const { return ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) || - isInteger() || - ( isPredicateSubtype() && getSubtypeParentType().isReal() ); + isInteger(); } inline bool TypeNode::isString() const { @@ -944,43 +916,27 @@ inline TypeNode TypeNode::getRangeType() const { /** Is this a symbolic expression type? */ inline bool TypeNode::isSExpr() const { - return getKind() == kind::SEXPR_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isSExpr() ); -} - -/** 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() && getSubtypeParentType().isSubrange() ); + return getKind() == kind::SEXPR_TYPE; } /** Is this a floating-point type */ inline bool TypeNode::isFloatingPoint() const { - return getKind() == kind::FLOATINGPOINT_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() ); + return getKind() == kind::FLOATINGPOINT_TYPE; } /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { - return getKind() == kind::BITVECTOR_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isBitVector() ); + return getKind() == kind::BITVECTOR_TYPE; } /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { - return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE || - ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); + return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE; } /** Is this a parametric datatype type */ inline bool TypeNode::isParametricDatatype() const { - return getKind() == kind::PARAMETRIC_DATATYPE || - ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() ); + return getKind() == kind::PARAMETRIC_DATATYPE; } /** Is this a codatatype type */ @@ -1013,15 +969,13 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { return ( getKind() == kind::FLOATINGPOINT_TYPE && getConst<FloatingPointSize>().exponent() == exp && - getConst<FloatingPointSize>().significand() == sig ) || - ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) ); + getConst<FloatingPointSize>().significand() == sig ); } /** 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() && getSubtypeParentType().isBitVector(size) ); + ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ); } /** Get the datatype specification from a datatype type */ @@ -1054,16 +1008,6 @@ inline unsigned TypeNode::getBitVectorSize() const { return getConst<BitVectorSize>(); } -inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { - Assert(isSubrange()); - if(getKind() == kind::SUBRANGE_TYPE){ - return getConst<SubrangeBounds>(); - }else{ - Assert(isPredicateSubtype()); - return getSubtypeParentType().getSubrangeBounds(); - } -} - #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used |