diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
commit | b122cec27ca27d0b48e786191448e0053be78ed0 (patch) | |
tree | 615981d8623e830894f02fc528b173ac7461f934 /src/expr | |
parent | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff) |
Tuples and records merge. Resolves bug 270.
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(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 | 13 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 9 | ||||
-rwxr-xr-x | src/expr/mkexpr | 4 | ||||
-rw-r--r-- | src/expr/node.cpp | 3 | ||||
-rw-r--r-- | src/expr/node.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 36 | ||||
-rw-r--r-- | src/expr/node_manager.h | 64 | ||||
-rw-r--r-- | src/expr/type.cpp | 30 | ||||
-rw-r--r-- | src/expr/type.h | 32 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 170 | ||||
-rw-r--r-- | src/expr/type_node.h | 29 |
11 files changed, 330 insertions, 64 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index cacfa9215..7cb5eb459 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -517,6 +517,11 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } +RecordType ExprManager::mkRecordType(const Record& rec) { + NodeManagerScope nms(d_nodeManager); + return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); +} + SExprType ExprManager::mkSExprType(const std::vector<Type>& types) { NodeManagerScope nms(d_nodeManager); std::vector<TypeNode> typeNodes; @@ -804,20 +809,20 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { return t; } -Expr ExprManager::mkVar(const std::string& name, Type type) { +Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) { Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); NodeManagerScope nms(d_nodeManager); - Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); + Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal); Debug("nm") << "set " << name << " on " << *n << std::endl; INC_STAT_VAR(type, false); return Expr(this, n); } -Expr ExprManager::mkVar(Type type) { +Expr ExprManager::mkVar(Type type, bool isGlobal) { Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type, false); - return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal)); } Expr ExprManager::mkBoundVar(const std::string& name, Type type) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 561d99392..b9cae9431 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -359,6 +359,11 @@ public: TupleType mkTupleType(const std::vector<Type>& types); /** + * Make a record type with types from the rec parameter. + */ + RecordType mkRecordType(const Record& rec); + + /** * Make a symbolic expressiontype with types from * <code>types[0..types.size()-1]</code>. <code>types</code> may * have any number of elements. @@ -464,8 +469,8 @@ public: throw(TypeCheckingException); // variables are special, because duplicates are permitted - Expr mkVar(const std::string& name, Type type); - Expr mkVar(Type type); + Expr mkVar(const std::string& name, Type type, bool isGlobal = false); + Expr mkVar(Type type, bool isGlobal = false); Expr mkBoundVar(const std::string& name, Type type); Expr mkBoundVar(Type type); diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 28a47d84d..ec8d0d12f 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -136,7 +136,9 @@ function typerule { lineno=${BASH_LINENO[0]} check_theory_seen typerules="${typerules} +#line $lineno \"$kf\" case kind::$1: +#line $lineno \"$kf\" typeNode = $2::computeType(nodeManager, n, check); break; " @@ -147,7 +149,9 @@ function construle { lineno=${BASH_LINENO[0]} check_theory_seen construles="${construles} +#line $lineno \"$kf\" case kind::$1: +#line $lineno \"$kf\" return $2::computeIsConst(nodeManager, n); " } diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 11e889ca2..e580b6348 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -27,6 +27,9 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message) throw() : Exception(message), d_node(new Node(node)) { +#ifdef CVC4_DEBUG + s_debugLastException = toString().c_str(); +#endif /* CVC4_DEBUG */ } TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { diff --git a/src/expr/node.h b/src/expr/node.h index d36953054..a3b8853a0 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -67,10 +67,6 @@ private: /** The node responsible for the failure */ NodeTemplate<true>* d_node; -protected: - - TypeCheckingExceptionPrivate() throw() : Exception() {} - public: /** diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 0a13222dd..f040c7c72 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -320,7 +320,7 @@ Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const } if((flags & SKOLEM_NO_NOTIFY) == 0) { for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSkolem(n, comment); + (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL); } } return n; @@ -395,4 +395,38 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(bounds)); } +TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { + Assert(t.isTuple() || t.isRecord()); + + // if the type doesn't have an associated datatype, then make one for it + TypeNode& dtt = d_tupleAndRecordTypes[t]; + if(dtt.isNull()) { + if(t.isTuple()) { + Datatype dt("__cvc4_tuple"); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) { + c.addArg("__cvc4_tuple_stor", (*i).toType()); + } + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; + } else { + const Record& rec = t.getRecord(); + Datatype dt("__cvc4_record"); + DatatypeConstructor c("__cvc4_record_ctor"); + for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) { + c.addArg((*i).first, (*i).second); + } + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; + } + dtt.setAttribute(DatatypeRecordAttr(), t); + } else { + Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl; + } + Assert(!dtt.isNull()); + return dtt; +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ea733e771..6e08a9bc2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -53,10 +53,16 @@ class TypeChecker; namespace attr { struct VarNameTag { }; struct SortArityTag { }; + struct DatatypeTupleTag { }; + struct DatatypeRecordTag { }; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; +/** Attribute true for datatype types that are replacements for tuple types */ +typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; +/** Attribute true for datatype types that are replacements for record types */ +typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr; }/* CVC4::expr namespace */ @@ -71,8 +77,8 @@ public: virtual void nmNotifyNewSortConstructor(TypeNode tn) { } virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { } virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { } - virtual void nmNotifyNewVar(TNode n) { } - virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { } + virtual void nmNotifyNewVar(TNode n, bool isGlobal) { } + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { } };/* class NodeManagerListener */ class NodeManager { @@ -82,8 +88,8 @@ class NodeManager { friend class expr::TypeChecker; // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string&, Type); - friend Expr ExprManager::mkVar(Type); + friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal); + friend Expr ExprManager::mkVar(Type, bool isGlobal); // friend so it can access NodeManager's d_listeners and notify clients friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&); @@ -158,6 +164,11 @@ class NodeManager { std::vector<NodeManagerListener*> d_listeners; /** + * A map of tuple and record types to their corresponding datatype. + */ + std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes; + + /** * Look up a NodeValue in the pool associated to this NodeManager. * The NodeValue argument need not be a "completely-constructed" * NodeValue. In particular, "non-inlined" constants are permitted @@ -288,12 +299,12 @@ class NodeManager { * version of this is private to avoid internal uses of mkVar() from * within CVC4. Such uses should employ mkSkolem() instead. */ - Node mkVar(const std::string& name, const TypeNode& type); - Node* mkVarPtr(const std::string& name, const TypeNode& type); + Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false); + Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false); /** Create a variable with the given type. */ - Node mkVar(const TypeNode& type); - Node* mkVarPtr(const TypeNode& type); + Node mkVar(const TypeNode& type, bool isGlobal = false); + Node* mkVarPtr(const TypeNode& type, bool isGlobal = false); public: @@ -413,7 +424,8 @@ public: enum SkolemFlags { SKOLEM_DEFAULT = 0, /**< default behavior */ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ - SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */ + SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */ + SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ };/* enum SkolemFlags */ /** @@ -717,6 +729,14 @@ public: inline TypeNode mkTupleType(const std::vector<TypeNode>& types); /** + * Make a record type with the description from rec. + * + * @param rec a description of the record + * @returns the record type + */ + inline TypeNode mkRecordType(const Record& rec); + + /** * Make a symbolic expression type with types from * <code>types</code>. <code>types</code> may have any number of * elements. @@ -780,6 +800,12 @@ public: throw(TypeCheckingExceptionPrivate); /** + * Given a tuple or record type, get the internal datatype used for + * it. Makes the DatatypeType if necessary. + */ + TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); + + /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if @@ -1067,6 +1093,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { return mkTypeNode(kind::TUPLE_TYPE, typeNodes); } +inline TypeNode NodeManager::mkRecordType(const Record& rec) { + return mkTypeConst(rec); +} + inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { @@ -1456,25 +1486,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, } -inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { +inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n); + (*i)->nmNotifyNewVar(n, isGlobal); } return n; } inline Node* NodeManager::mkVarPtr(const std::string& name, - const TypeNode& type) { + const TypeNode& type, bool isGlobal) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n); + (*i)->nmNotifyNewVar(*n, isGlobal); } return n; } @@ -1492,22 +1522,22 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name, return n; } -inline Node NodeManager::mkVar(const TypeNode& type) { +inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n); + (*i)->nmNotifyNewVar(n, isGlobal); } return n; } -inline Node* NodeManager::mkVarPtr(const TypeNode& type) { +inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n); + (*i)->nmNotifyNewVar(*n, isGlobal); } return n; } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index cb1e829c4..cc52b11b9 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -350,6 +350,19 @@ Type::operator TupleType() const throw(IllegalArgumentException) { return TupleType(*this); } +/** Is this a record type? */ +bool Type::isRecord() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isRecord(); +} + +/** Cast to a record type */ +Type::operator RecordType() const throw(IllegalArgumentException) { + NodeManagerScope nms(d_nodeManager); + CheckArgument(isNull() || isRecord(), this); + return RecordType(*this); +} + /** Is this a symbolic expression type? */ bool Type::isSExpr() const { NodeManagerScope nms(d_nodeManager); @@ -449,6 +462,10 @@ Type FunctionType::getRangeType() const { return makeType(d_typeNode->getRangeType()); } +size_t TupleType::getLength() const { + return d_typeNode->getTupleLength(); +} + vector<Type> TupleType::getTypes() const { NodeManagerScope nms(d_nodeManager); vector<Type> types; @@ -461,6 +478,11 @@ vector<Type> TupleType::getTypes() const { return types; } +const Record& RecordType::getRecord() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getRecord(); +} + vector<Type> SExprType::getTypes() const { NodeManagerScope nms(d_nodeManager); vector<Type> types; @@ -565,6 +587,11 @@ TupleType::TupleType(const Type& t) throw(IllegalArgumentException) : CheckArgument(isNull() || isTuple(), this); } +RecordType::RecordType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + CheckArgument(isNull() || isRecord(), this); +} + SExprType::SExprType(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isSExpr(), this); @@ -633,12 +660,13 @@ std::vector<Type> ConstructorType::getArgTypes() const { } const Datatype& DatatypeType::getDatatype() const { + NodeManagerScope nms(d_nodeManager); if( d_typeNode->isParametricDatatype() ) { CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this); const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>(); return dt; } else { - return d_typeNode->getConst<Datatype>(); + return d_typeNode->getDatatype(); } } diff --git a/src/expr/type.h b/src/expr/type.h index e5590aa59..4223d71ab 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -38,6 +38,7 @@ class ExprManagerMapCollection; class SmtEngine; class Datatype; +class Record; template <bool ref_count> class NodeTemplate; @@ -54,6 +55,7 @@ class SelectorType; class TesterType; class FunctionType; class TupleType; +class RecordType; class SExprType; class SortType; class SortConstructorType; @@ -323,6 +325,18 @@ public: operator TupleType() const throw(IllegalArgumentException); /** + * Is this a record type? + * @return true if the type is a record type + */ + bool isRecord() const; + + /** + * Cast this type to a record type + * @return the RecordType + */ + operator RecordType() const throw(IllegalArgumentException); + + /** * Is this a symbolic expression type? * @return true if the type is a symbolic expression type */ @@ -527,11 +541,29 @@ public: /** Construct from the base type */ TupleType(const Type& type = Type()) throw(IllegalArgumentException); + /** Get the length of the tuple. The same as getTypes().size(). */ + size_t getLength() const; + /** Get the constituent types */ std::vector<Type> getTypes() const; + };/* class TupleType */ /** + * Class encapsulating a record type. + */ +class CVC4_PUBLIC RecordType : public Type { + +public: + + /** Construct from the base type */ + RecordType(const Type& type = Type()) throw(IllegalArgumentException); + + /** Get the constituent types */ + const Record& getRecord() const; +};/* class RecordType */ + +/** * Class encapsulating a tuple type. */ class CVC4_PUBLIC SExprType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ae870b1c2..236f48017 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -90,6 +90,22 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { t.getConst<TypeConstant>() == REAL_TYPE ); } } + if(isTuple() || isRecord()) { + if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { + return true; + } + if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || + getNumChildren() != t.getNumChildren()) { + return false; + } + // children must be subtypes of t's, in order + for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { + if(!(*i).isSubtypeOf(*j)) { + return false; + } + } + return true; + } if(isPredicateSubtype()) { return getSubtypeParentType().isSubtypeOf(t); } @@ -103,6 +119,30 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } + if(t.isDatatype() && (isTuple() || isRecord())) { + if(t.isTuple() || t.isRecord()) { + if(NodeManager::currentNM()->getDatatypeForTupleRecord(t) == + NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { + return true; + } + if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || + getNumChildren() != t.getNumChildren()) { + return false; + } + // children must be comparable to t's, in order + for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { + if(!(*i).isComparableTo(*j)) { + return false; + } + } + return true; + } else { + return t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this); + } + } else if(isDatatype() && (t.isTuple() || t.isRecord())) { + Assert(!isTuple() && !isRecord());// should have been handled above + return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t); + } if(isPredicateSubtype()) { return t.isComparableTo(getSubtypeParentType()); } @@ -123,6 +163,8 @@ TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; + } else if (isTuple() || isRecord()) { + return NodeManager::currentNM()->getDatatypeForTupleRecord(*this); } else if (isPredicateSubtype()) { return getSubtypeParentType().getBaseType(); } @@ -152,6 +194,11 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { return params; } +size_t TypeNode::getTupleLength() const { + Assert(isTuple()); + return getNumChildren(); +} + vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); vector<TypeNode> types; @@ -161,6 +208,11 @@ vector<TypeNode> TypeNode::getTupleTypes() const { return types; } +const Record& TypeNode::getRecord() const { + Assert(isRecord()); + return getConst<Record>(); +} + vector<TypeNode> TypeNode::getSExprTypes() const { Assert(isSExpr()); vector<TypeNode> types; @@ -205,41 +257,41 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(!t0.isNull()); Assert(!t1.isNull()); - if(EXPECT_TRUE(t0 == t1)){ + if(EXPECT_TRUE(t0 == t1)) { return t0; - }else{ // t0 != t1 - if(t0.getKind()== kind::TYPE_CONSTANT){ + } else { // t0 != t1 + if(t0.getKind()== kind::TYPE_CONSTANT) { switch(t0.getConst<TypeConstant>()) { case INTEGER_TYPE: - if(t1.isInteger()){ + if(t1.isInteger()) { // t0 == IntegerType && t1.isInteger() return t0; //IntegerType - }else if(t1.isReal()){ + } else if(t1.isReal()) { // t0 == IntegerType && t1.isReal() && !t1.isInteger() return NodeManager::currentNM()->realType(); // RealType - }else{ - return TypeNode(); //null type + } else { + return TypeNode(); // null type } case REAL_TYPE: - if(t1.isReal()){ + if(t1.isReal()) { return t0; // RealType - }else{ + } else { return TypeNode(); // null type } default: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){ + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { return t0; // t0 is a constant type - }else{ + } else { return TypeNode(); // null type } } - }else if(t1.getKind() == kind::TYPE_CONSTANT){ + } else if(t1.getKind() == kind::TYPE_CONSTANT) { return leastCommonTypeNode(t1, t0); //decrease the number of special cases - }else{ + } else { // t0 != t1 && // t0.getKind() == kind::TYPE_CONSTANT && // t1.getKind() == kind::TYPE_CONSTANT - switch(t0.getKind()){ + switch(t0.getKind()) { case kind::ARRAY_TYPE: case kind::BITVECTOR_TYPE: case kind::SORT_TYPE: @@ -247,9 +299,9 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){ + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { return t0; - }else{ + } else { return TypeNode(); } case kind::FUNCTION_TYPE: @@ -257,48 +309,96 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ case kind::SEXPR_TYPE: Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); return TypeNode(); // Not sure if this is right - case kind::TUPLE_TYPE: - Unimplemented("haven't implemented leastCommonType for tuples yet"); - 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 + }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(); + if(t1.isSubrange()) { + const SubrangeBounds& t0SR = t0.getSubrangeBounds(); const SubrangeBounds& t1SR = t1.getSubrangeBounds(); - if(SubrangeBounds::joinIsBounded(t0SR, t1SR)){ + if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) { SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR); return NodeManager::currentNM()->mkSubrangeType(j); - }else{ + } 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()){ + } 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()){ + } else if(t1.isReal()) { return NodeManager::currentNM()->realType(); - }else{ + } else { return TypeNode(); } - }else{ - //t0 is a subrange - //t1 is not a subrange + } 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(); } + case kind::TUPLE_TYPE: { + // if the other == this one, we returned already, above + if(t0.getBaseType() == t1) { + return t1; + } + if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) { + // no compatibility between t0, t1 + return TypeNode(); + } + std::vector<TypeNode> types; + // construct childwise leastCommonType, if one exists + for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) { + TypeNode kid = leastCommonTypeNode(*i, *j); + if(kid.isNull()) { + // no common supertype: types t0, t1 not compatible + return TypeNode(); + } + types.push_back(kid); + } + // if we make it here, we constructed the least common type + return NodeManager::currentNM()->mkTupleType(types); + } + case kind::RECORD_TYPE: { + // if the other == this one, we returned already, above + if(t0.getBaseType() == t1) { + return t1; + } + const Record& r0 = t0.getConst<Record>(); + if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) { + // no compatibility between t0, t1 + return TypeNode(); + } + std::vector< std::pair<std::string, Type> > fields; + const Record& r1 = t1.getConst<Record>(); + // construct childwise leastCommonType, if one exists + for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) { + TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); + if((*i).first != (*j).first || kid.isNull()) { + // if field names differ, or no common supertype, then + // types t0, t1 not compatible + return TypeNode(); + } + fields.push_back(std::make_pair((*i).first, kid.toType())); + } + // if we make it here, we constructed the least common type + return NodeManager::currentNM()->mkRecordType(Record(fields)); + } case kind::DATATYPE_TYPE: - // two datatypes that aren't == have no common ancestors + // t1 might be a subtype tuple or record + if(t1.getBaseType() == t0) { + return t0; + } + // otherwise no common ancestor return TypeNode(); default: Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index fc142191d..93e9f1ca7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -536,9 +536,18 @@ public: /** Is this a tuple type? */ bool isTuple() const; + /** Get the length of a tuple type */ + size_t getTupleLength() const; + /** Get the constituent types of a tuple type */ std::vector<TypeNode> getTupleTypes() const; + /** Is this a record type? */ + bool isRecord() const; + + /** Get the description of the record type */ + const Record& getRecord() const; + /** Is this a symbolic expression type? */ bool isSExpr() const; @@ -572,6 +581,9 @@ public: /** Is this a tester type */ bool isTester() const; + /** Get the Datatype specification from a datatype type */ + const Datatype& getDatatype() const; + /** Get the size of this bit-vector type */ unsigned getBitVectorSize() const; @@ -883,6 +895,12 @@ inline bool TypeNode::isTuple() const { ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); } +/** Is this a record type? */ +inline bool TypeNode::isRecord() const { + return getKind() == kind::RECORD_TYPE || + ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); +} + /** Is this a symbolic expression type? */ inline bool TypeNode::isSExpr() const { return getKind() == kind::SEXPR_TYPE || @@ -920,6 +938,7 @@ inline bool TypeNode::isBitVector() const { /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { return getKind() == kind::DATATYPE_TYPE || + getKind() == kind::TUPLE_TYPE || getKind() == kind::RECORD_TYPE || ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); } @@ -951,6 +970,16 @@ inline bool TypeNode::isBitVector(unsigned size) const { ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) ); } +/** Get the datatype specification from a datatype type */ +inline const Datatype& TypeNode::getDatatype() const { + Assert(isDatatype()); + if(getKind() == kind::DATATYPE_TYPE) { + return getConst<Datatype>(); + } else { + return NodeManager::currentNM()->getDatatypeForTupleRecord(*this).getConst<Datatype>(); + } +} + /** Get the size of this bit-vector type */ inline unsigned TypeNode::getBitVectorSize() const { Assert(isBitVector()); |