diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-18 23:48:38 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-18 23:48:38 +0000 |
commit | ea8139dc7b727bf48bd7b7c6b169d763618a1f2a (patch) | |
tree | 95701608122c2a6e232ee22979e9da757bf4e2dd /src/expr | |
parent | 3b93d45dab9513195d5604a069423ed13e173f49 (diff) |
This commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.h | 3 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 136 | ||||
-rw-r--r-- | src/expr/type_node.h | 27 |
3 files changed, 159 insertions, 7 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2bcf5e18c..00fe6baa8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -573,9 +573,6 @@ public: /** Get the (singleton) type for reals. */ inline TypeNode realType(); - /** Get the (singleton) type for pseudobooleans. */ - inline TypeNode pseudobooleanType(); - /** Get the (singleton) type for strings. */ inline TypeNode stringType(); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 3f5c3a032..7b093d11a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -181,4 +181,140 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1]; } +TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + + Assert(!t0.isNull()); + Assert(!t1.isNull()); + + if(EXPECT_TRUE(t0 == t1)){ + return t0; + }else{ // t0 != t1 + if(t0.getKind()== kind::TYPE_CONSTANT){ + switch(t0.getConst<TypeConstant>()) { + case INTEGER_TYPE: + if(t1.isInteger()){ + // t0 == IntegerType && t1.isInteger() + return t0; //IntegerType + }else if(t1.isReal()){ + // t0 == IntegerType && t1.isReal() && !t1.isInteger() + return NodeManager::currentNM()->realType(); // RealType + }else{ + return TypeNode(); //null type + } + case REAL_TYPE: + if(t1.isReal()){ + return t0; // RealType + }else{ + return TypeNode(); // null type + } + default: + if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + return t0; // t0 is a constant type + }else{ + return TypeNode(); // null type + } + } + }else if(t1.getKind() == kind::TYPE_CONSTANT){ + return leastCommonTypeNode(t1, t0); //decrease the number of special cases + }else{ + // t0 != t1 && + // t0.getKind() == kind::TYPE_CONSTANT && + // t1.getKind() == kind::TYPE_CONSTANT + switch(t0.getKind()){ + case kind::ARRAY_TYPE: + case kind::BITVECTOR_TYPE: + case kind::SORT_TYPE: + case kind::PARAMETRIC_DATATYPE: + case kind::CONSTRUCTOR_TYPE: + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + return t0; + }else{ + return TypeNode(); + } + case kind::FUNCTION_TYPE: + return TypeNode(); // Not sure if this is right + case kind::TUPLE_TYPE: + Unimplemented(); + return TypeNode(); // Not sure if this is right + 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 leastCommonTypeNode(t1, t0); //decrease the number of special cases + } + 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(); + } + default: + Unimplemented(); + return TypeNode(); + } + } + } +} + +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().getSubtypeBaseType()); + } + std::vector<TypeNode> t1stack; + t1stack.push_back(t1); + while(t1stack.back().isPredicateSubtype()){ + t1stack.push_back(t1stack.back().getSubtypeBaseType()); + } + + 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()); + } +} + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 25b5e4bb3..482da2814 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -159,9 +159,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { - return - d_nv == typeNode.d_nv || - (typeNode.isReal() && this->isReal()); + return d_nv == typeNode.d_nv; } /** @@ -595,9 +593,25 @@ public: /** Is this a kind type (i.e., the type of a type)? */ bool isKind() 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, + * a TypeNode such that isNull() is true is returned. + * + * For more information see: http://church.cims.nyu.edu/wiki/Cvc4_Type_Lattice + */ + static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); + private: /** + * 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. * * @param out the stream to indent @@ -940,7 +954,12 @@ inline unsigned TypeNode::getBitVectorSize() const { inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { Assert(isSubrange()); - return getConst<SubrangeBounds>(); + if(getKind() == kind::SUBRANGE_TYPE){ + return getConst<SubrangeBounds>(); + }else{ + Assert(isPredicateSubtype()); + return getSubtypeBaseType().getSubrangeBounds(); + } } #ifdef CVC4_DEBUG |