diff options
43 files changed, 1556 insertions, 304 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()); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 18dfcd473..c82a984d2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -11,7 +11,7 @@ ** ** \brief Parser for CVC presentation input language ** - ** Parser for CVC input language. + ** Parser for CVC presentation input language. **/ grammar Cvc; @@ -866,7 +866,7 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms, // NOTE: do not clear the vectors here! } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] - { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t); + { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t, false); terms.insert(terms.end(), vars.begin(), vars.end()); for(unsigned i = 0; i < vars.size(); ++i) { types.push_back(t); @@ -957,7 +957,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri } } else { Debug("parser") << " " << *i << " not declared" << std::endl; - Expr func = PARSER_STATE->mkVar(*i, t); + Expr func = PARSER_STATE->mkVar(*i, t, true); if(topLevel) { Command* decl = new DeclareFunctionCommand(*i, func, t); seq->addCommand(decl); @@ -977,7 +977,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri i != i_end; ++i) { PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); - Expr func = EXPR_MANAGER->mkVar(*i, t); + Expr func = EXPR_MANAGER->mkVar(*i, t, true); PARSER_STATE->defineFunction(*i, f); Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); @@ -1176,14 +1176,14 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } } else { // tuple type [ T, U, V... ] - t = PARSER_STATE->mkTupleType(types); + t = EXPR_MANAGER->mkTupleType(types); } } /* record types */ | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ - { t = PARSER_STATE->mkRecordType(typeIds); } + { t = EXPR_MANAGER->mkRecordType(typeIds); } /* bitvector types */ | BITVECTOR_TOK LPAREN k=numeral RPAREN @@ -1340,7 +1340,7 @@ prefixFormula[CVC4::Expr& f] boundVarDecl[ids,t] RPAREN COLON formula[f] { PARSER_STATE->popScope(); UNSUPPORTED("array literals not supported yet"); - f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType())); + f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), true); } ; @@ -1489,30 +1489,16 @@ tupleStore[CVC4::Expr& f] : k=numeral ASSIGN_TOK uminusTerm[f2] { Type t = f.getType(); - if(! t.isDatatype()) { + if(! t.isTuple()) { PARSER_STATE->parseError("tuple-update applied to non-tuple"); } - Datatype tuple = DatatypeType(f.getType()).getDatatype(); - if(tuple.getName() != "__cvc4_tuple") { - PARSER_STATE->parseError("tuple-update applied to non-tuple"); - } - if(k < tuple[0].getNumArgs()) { - std::vector<Expr> args; - for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) { - if(i == k) { - args.push_back(f2); - } else { - Expr selectorOp = tuple[0][i].getSelector(); - Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); - args.push_back(select); - } - } - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args); - } else { + size_t length = TupleType(t).getLength(); + if(k >= length) { std::stringstream ss; - ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k; + ss << "tuple is of length " << length << "; cannot update index " << k; PARSER_STATE->parseError(ss.str()); } + f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2); } ; @@ -1528,31 +1514,15 @@ recordStore[CVC4::Expr& f] : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] { Type t = f.getType(); - if(! t.isDatatype()) { - PARSER_STATE->parseError("record-update applied to non-record"); - } - Datatype record = DatatypeType(f.getType()).getDatatype(); - if(record.getName() != "__cvc4_record") { + if(! t.isRecord()) { PARSER_STATE->parseError("record-update applied to non-record"); } - const DatatypeConstructorArg* updateArg = 0; - try { - updateArg = &record[0][id]; - } catch(IllegalArgumentException& e) { + const Record& rec = RecordType(t).getRecord(); + Record::const_iterator fld = rec.find(id); + if(fld == rec.end()) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - std::vector<Expr> args; - for(unsigned i = 0; i < record[0].getNumArgs(); ++i) { - const DatatypeConstructorArg* thisArg = &record[0][i]; - if(thisArg == updateArg) { - args.push_back(f2); - } else { - Expr selectorOp = record[0][i].getSelector(); - Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); - args.push_back(select); - } - } - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args); + f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2); } ; @@ -1667,37 +1637,28 @@ postfixTerm[CVC4::Expr& f] | DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] { Type t = f.getType(); - if(! t.isDatatype()) { + if(! t.isRecord()) { PARSER_STATE->parseError("record-select applied to non-record"); } - Datatype record = DatatypeType(f.getType()).getDatatype(); - if(record.getName() != "__cvc4_record") { - PARSER_STATE->parseError("record-select applied to non-record"); - } - try { - Expr selectorOp = record[0][id].getSelector(); - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); - } catch(IllegalArgumentException& e) { + const Record& rec = RecordType(t).getRecord(); + Record::const_iterator fld = rec.find(id); + if(fld == rec.end()) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } + f = MK_EXPR(MK_CONST(RecordSelect(id)), f); } | k=numeral { Type t = f.getType(); - if(! t.isDatatype()) { - PARSER_STATE->parseError("tuple-select applied to non-tuple"); - } - Datatype tuple = DatatypeType(f.getType()).getDatatype(); - if(tuple.getName() != "__cvc4_tuple") { + if(! t.isTuple()) { PARSER_STATE->parseError("tuple-select applied to non-tuple"); } - try { - Expr selectorOp = tuple[0][k].getSelector(); - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); - } catch(IllegalArgumentException& e) { + size_t length = TupleType(t).getLength(); + if(k >= length) { std::stringstream ss; - ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k; + ss << "tuple is of length " << length << "; cannot access index " << k; PARSER_STATE->parseError(ss.str()); } + f = MK_EXPR(MK_CONST(TupleSelect(k)), f); } ) )* @@ -1871,8 +1832,8 @@ simpleTerm[CVC4::Expr& f] for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { types.push_back((*i).getType()); } - DatatypeType t = PARSER_STATE->mkTupleType(types); - f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); + TupleType t = EXPR_MANAGER->mkTupleType(types); + f = MK_EXPR(kind::TUPLE, args); } } @@ -1902,8 +1863,8 @@ simpleTerm[CVC4::Expr& f] for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } - DatatypeType t = PARSER_STATE->mkRecordType(typeIds); - f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); + RecordType t = EXPR_MANAGER->mkRecordType(typeIds); + f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args); } /* variable / zero-ary constructor application */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index ef386f57e..10ca16001 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -138,8 +138,8 @@ bool Parser::isPredicate(const std::string& name) { Expr Parser::mkVar(const std::string& name, const Type& type, bool levelZero) { - Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type); + Debug("parser") << "mkVar(" << name << ", " << type << ", " << levelZero << ")" << std::endl; + Expr expr = d_exprManager->mkVar(name, type, levelZero); defineVar(name, expr, levelZero); return expr; } @@ -156,7 +156,7 @@ Expr Parser::mkFunction(const std::string& name, const Type& type, bool levelZero) { Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type); + Expr expr = d_exprManager->mkVar(name, type, levelZero); defineFunction(name, expr, levelZero); return expr; } @@ -339,37 +339,6 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { return types; } -DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) { - DatatypeType& dtt = d_recordTypes[typeIds]; - if(dtt.isNull()) { - Datatype dt("__cvc4_record"); -Debug("datatypes") << "make new record_ctor" << std::endl; - DatatypeConstructor c("__cvc4_record_ctor"); - for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) { - c.addArg((*i).first, (*i).second); - } - dt.addConstructor(c); - dtt = d_exprManager->mkDatatypeType(dt); - } else { -Debug("datatypes") << "use old record_ctor" << std::endl; -} - return dtt; -} - -DatatypeType Parser::mkTupleType(const std::vector<Type>& types) { - DatatypeType& dtt = d_tupleTypes[types]; - if(dtt.isNull()) { - Datatype dt("__cvc4_tuple"); - DatatypeConstructor c("__cvc4_tuple_ctor"); - for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) { - c.addArg("__cvc4_tuple_stor", *i); - } - dt.addConstructor(c); - dtt = d_exprManager->mkDatatypeType(dt); - } - return dtt; -} - bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index eb76900d2..eed8531a5 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -141,20 +141,6 @@ class CVC4_PUBLIC Parser { /** Are we only parsing? */ bool d_parseOnly; - /** - * We might see the same record type multiple times; we have - * to match always to the same Type. This map contains all the - * record types we have. - */ - std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes; - - /** - * We might see the same tuple type multiple times; we have - * to match always to the same Type. This map contains all the - * tuple types we have. - */ - std::map<std::vector<Type>, DatatypeType> d_tupleTypes; - /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; @@ -420,16 +406,6 @@ public: mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); /** - * Create a record type, or if there's already a matching one, return that one. - */ - DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds); - - /** - * Create a tuple type, or if there's already a matching one, return that one. - */ - DatatypeType mkTupleType(const std::vector<Type>& types); - - /** * Add an operator to the current legal set. * * @param kind the built-in operator to add diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f190b81bf..b3e16b38e 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -207,7 +207,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ']'; return; break; - case kind::TUPLE: case kind::SEXPR: // no-op break; @@ -291,6 +290,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; // DATATYPES + case kind::APPLY_TYPE_ASCRIPTION: { + toStream(out, n[0], depth, types, false); + out << "::"; + TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType()); + out << (t.isFunctionLike() ? t.getRangeType() : t); + } + return; + break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: case kind::APPLY_TESTER: @@ -321,6 +328,49 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << " -> BOOLEAN"; return; break; + case kind::TUPLE_SELECT: + toStream(out, n[0], depth, types, true); + out << '.' << n.getOperator().getConst<TupleSelect>().getIndex(); + return; + break; + case kind::RECORD_SELECT: + toStream(out, n[0], depth, types, true); + out << '.' << n.getOperator().getConst<RecordSelect>().getField(); + return; + break; + case kind::TUPLE_UPDATE: + toStream(out, n[0], depth, types, true); + out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := "; + toStream(out, n[1], depth, types, true); + return; + break; + case kind::RECORD_UPDATE: + toStream(out, n[0], depth, types, true); + out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := "; + toStream(out, n[1], depth, types, true); + return; + break; + case kind::TUPLE: + // no-op + break; + case kind::RECORD: { + // (# _a := 2, _b := 2 #) + const Record& rec = n.getOperator().getConst<Record>(); + out << "(# "; + TNode::iterator i = n.begin(); + bool first = true; + for(Record::const_iterator j = rec.begin(); j != rec.end(); ++i, ++j) { + if(!first) { + out << ", "; + } + out << (*j).first << " := "; + toStream(out, *i, depth, types, false); + first = false; + } + out << " #)"; + return; + break; + } // ARRAYS case kind::ARRAY_TYPE: @@ -413,6 +463,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << ">="; opType = INFIX; break; + case kind::PARAMETRIC_DATATYPE: + out << n[0].getConst<Datatype>().getName(); + break; // BITVECTORS case kind::BITVECTOR_XOR: @@ -748,14 +801,14 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ - //print the cardinality + // print the cardinality if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; } } out << c << std::endl; if( tn.isSort() ){ - //print the representatives + // print the representatives if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ @@ -780,7 +833,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t }else{ out << tn; } - out << " = " << tm.getValue( n ) << ";" << std::endl; + out << " = " << tm.getValue(n.toExpr()) << ";" << std::endl; /* //for table format (work in progress) @@ -916,10 +969,11 @@ static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { } static void toStream(std::ostream& out, const GetValueCommand* c) throw() { - out << "% (get-value ( "; const vector<Expr>& terms = c->getTerms(); - copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " ")); - out << " ))"; + Assert(!terms.empty()); + out << "GET_VALUE "; + copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE ")); + out << terms.back() << ";"; } static void toStream(std::ostream& out, const GetModelCommand* c) throw() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c3fb3b782..ae589eba6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -281,6 +281,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; // datatypes + case kind::APPLY_TYPE_ASCRIPTION: { + out << "as "; + toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types); + out << ' '; + TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType()); + out << (t.isFunctionLike() ? t.getRangeType() : t); + stillNeedToPrintParams = false; + } + break; case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 5555a6190..82601e3c3 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ smt_engine.h \ + model_postprocessor.cpp \ + model_postprocessor.h \ smt_engine_scope.cpp \ smt_engine_scope.h \ command_list.cpp \ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp new file mode 100644 index 000000000..38fd3ab8b --- /dev/null +++ b/src/smt/model_postprocessor.cpp @@ -0,0 +1,52 @@ +/********************* */ +/*! \file model_postprocessor.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** + **/ + +#include "smt/model_postprocessor.h" + +using namespace CVC4; +using namespace CVC4::smt; + +void ModelPostprocessor::visit(TNode current, TNode parent) { + Debug("tuprec") << "visiting " << current << std::endl; + Assert(!alreadyVisited(current, TNode::null())); + if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { + Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + NodeBuilder<> b(kind::TUPLE); + for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Assert(alreadyVisited(*i, TNode::null())); + TNode n = d_nodes[*i]; + b << (n.isNull() ? *i : n); + } + d_nodes[current] = b; + Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { + Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + NodeBuilder<> b(kind::RECORD); + b << current.getType().getAttribute(expr::DatatypeRecordAttr()); + for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Assert(alreadyVisited(*i, TNode::null())); + TNode n = d_nodes[*i]; + b << (n.isNull() ? *i : n); + } + d_nodes[current] = b; + Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + } else { + Debug("tuprec") << "returning self" << std::endl; + // rewrite to self + d_nodes[current] = Node::null(); + } +}/* ModelPostprocessor::visit() */ + diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h new file mode 100644 index 000000000..08e6168d9 --- /dev/null +++ b/src/smt/model_postprocessor.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file model_postprocessor.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MODEL_POSTPROCESSOR_H +#define __CVC4__MODEL_POSTPROCESSOR_H + +#include "expr/node.h" + +namespace CVC4 { +namespace smt { + +class ModelPostprocessor { +public: + typedef Node return_type; + std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; + + bool alreadyVisited(TNode current, TNode parent) { + return d_nodes.find(current) != d_nodes.end(); + } + + void visit(TNode current, TNode parent); + + void start(TNode n) { } + + Node done(TNode n) { + Assert(alreadyVisited(n, TNode::null())); + TNode retval = d_nodes[n]; + return retval.isNull() ? n : retval; + } +};/* class ModelPostprocessor */ + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__MODEL_POSTPROCESSOR_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5ea16f20f..07e3439fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -40,11 +40,13 @@ #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/model_postprocessor.h" #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" #include "util/boolean_simplification.h" +#include "util/node_visitor.h" #include "util/configuration.h" #include "util/exception.h" #include "smt/command_list.h" @@ -366,14 +368,14 @@ public: d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewVar(TNode n) { + void nmNotifyNewVar(TNode n, bool isGlobal) { DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); - d_smt.addToModelCommandAndDump(c); + d_smt.addToModelCommandAndDump(c, isGlobal); } - void nmNotifyNewSkolem(TNode n, const std::string& comment) { + void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { std::string id = n.getAttribute(expr::VarNameAttr()); DeclareFunctionCommand c(id, n.toExpr(), @@ -381,7 +383,7 @@ public: if(Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); } - d_smt.addToModelCommandAndDump(c, false, "skolems"); + d_smt.addToModelCommandAndDump(c, isGlobal, false, "skolems"); } Node applySubstitutions(TNode node) const { @@ -502,6 +504,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), + d_modelGlobalCommands(), d_modelCommands(NULL), d_dumpCommands(), d_logic(), @@ -2020,7 +2023,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, return false; } - void SmtEnginePrivate::processAssertions() { Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -2389,6 +2391,9 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Add the formula d_problemExtended = true; + if(d_assertionList != NULL) { + d_assertionList->push_back(e.notExpr()); + } d_private->addFormula(e.getNode().notNode()); // Run the check @@ -2440,6 +2445,12 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log return quickCheck().asValidityResult(); } +Node SmtEngine::postprocess(TNode node) { + ModelPostprocessor mpost; + NodeVisitor<ModelPostprocessor> visitor; + return visitor.run(mpost, node); +} + Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -2458,7 +2469,9 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep // Make sure all preprocessing is done d_private->processAssertions(); - return d_private->simplify(Node::fromExpr(e)).toExpr(); + Node n = d_private->simplify(Node::fromExpr(e)); + n = postprocess(n); + return n.toExpr(); } Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) { @@ -2478,7 +2491,9 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L Dump("benchmark") << ExpandDefinitionsCommand(e); } hash_map<Node, Node, NodeHashFunction> cache; - return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); + Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); + n = postprocess(n); + return n.toExpr(); } Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { @@ -2520,10 +2535,12 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { Trace("smt") << "--- getting value of " << n << endl; TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; - if( m ){ - resultNode = m->getValue( n ); + if(m != NULL) { + resultNode = m->getValue(n); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; + resultNode = postprocess(resultNode); + Trace("smt") << "--- model-post returned " << resultNode << endl; // type-check the result we got Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); @@ -2630,7 +2647,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { return SExpr(sexprs); } -void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, const char* dumpTag) { +void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool userVisible, const char* dumpTag) { Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl; SmtScope smts(this); // If we aren't yet fully inited, the user might still turn on @@ -2643,7 +2660,11 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, con // and expects to find their cardinalities in the model. if(/* userVisible && */ (!d_fullyInited || options::produceModels())) { doPendingPops(); - d_modelCommands->push_back(c.clone()); + if(isGlobal) { + d_modelGlobalCommands.push_back(c.clone()); + } else { + d_modelCommands->push_back(c.clone()); + } } if(Dump.isOn(dumpTag)) { if(d_fullyInited) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2590bc8e2..b6fb156f6 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -87,6 +87,10 @@ namespace smt { typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ +namespace theory { + class TheoryModel; +}/* CVC4::theory namespace */ + namespace stats { StatisticsRegistry* getStatisticsRegistry(SmtEngine*); }/* CVC4::stats namespace */ @@ -144,8 +148,16 @@ class CVC4_PUBLIC SmtEngine { AssignmentSet* d_assignments; /** - * A list of commands that should be in the Model. Only maintained - * if produce-models option is on. + * A list of commands that should be in the Model globally (i.e., + * regardless of push/pop). Only maintained if produce-models option + * is on. + */ + std::vector<Command*> d_modelGlobalCommands; + + /** + * A list of commands that should be in the Model locally (i.e., + * it is context-dependent on push/pop). Only maintained if + * produce-models option is on. */ smt::CommandList* d_modelCommands; @@ -232,6 +244,13 @@ class CVC4_PUBLIC SmtEngine { void checkModel(bool hardFailure = true); /** + * Postprocess a value for output to the user. Involves doing things + * like turning datatypes back into tuples, length-1-bitvectors back + * into booleans, etc. + */ + Node postprocess(TNode n); + + /** * This is something of an "init" procedure, but is idempotent; call * as often as you like. Should be called whenever the final options * and logic for the problem are set (at least, those options that are @@ -293,6 +312,7 @@ class CVC4_PUBLIC SmtEngine { friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); // to access d_modelCommands friend class ::CVC4::Model; + friend class ::CVC4::theory::TheoryModel; // to access getModel(), which is private (for now) friend class GetModelCommand; @@ -304,7 +324,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index bcf787f6b..e3bc506e2 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -296,7 +296,6 @@ operator DISTINCT 2: "disequality" variable VARIABLE "variable" variable BOUND_VARIABLE "bound variable" variable SKOLEM "skolem var" -operator TUPLE 1: "a tuple" operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" @@ -313,14 +312,6 @@ cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" well-founded FUNCTION_TYPE false -operator TUPLE_TYPE 1: "tuple type" -cardinality TUPLE_TYPE \ - "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" -well-founded TUPLE_TYPE \ - "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" operator SEXPR_TYPE 0: "symbolic expression type" cardinality SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \ @@ -350,7 +341,6 @@ typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule -typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 720e55be3..4aa7c0982 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -115,19 +115,6 @@ public: } };/* class DistinctTypeRule */ -class TupleTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - std::vector<TypeNode> types; - for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); - child_it != child_it_end; - ++child_it) { - types.push_back((*child_it).getType(check)); - } - return nodeManager->mkTupleType(types); - } -};/* class TupleTypeRule */ - class SExprTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -269,58 +256,6 @@ public: } };/* class FuctionProperties */ -class TupleProperties { -public: - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - Cardinality card(1); - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - card *= (*i).getCardinality(); - } - - return card; - } - - inline static bool isWellFounded(TypeNode type) { - // Don't assert this; allow other theories to use this - // wellfoundedness computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - if(! (*i).isWellFounded()) { - return false; - } - } - - return true; - } - - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::TUPLE_TYPE); - - std::vector<Node> children; - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - children.push_back((*i).mkGroundTerm()); - } - - return NodeManager::currentNM()->mkNode(kind::TUPLE, children); - } -};/* class TupleProperties */ - class SExprProperties { public: inline static Cardinality computeCardinality(TypeNode type) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 42b999561..f9fb00a75 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -54,6 +54,43 @@ public: } } } + if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); + } + if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); + return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]); + } + if(in.getKind() == kind::APPLY_SELECTOR && + (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { + // These strange (half-tuple-converted) terms can be created by + // the system if you have something like "foo.1" for a tuple + // term foo. The select is rewritten to "select_1(foo)". If + // foo gets a value in the model from the TypeEnumerator, you + // then have a select of a tuple, and we should flatten that + // here. Ditto for records, below. + Expr selectorExpr = in.getOperator().toExpr(); + const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr); + TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType()); + size_t selectorIndex = Datatype::indexOf(selectorExpr); + Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl; +#ifdef CVC4_ASSERTIONS + // sanity checks: tuple- and record-converted datatypes should have one constructor + Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt); + if(in[0].getKind() == kind::TUPLE) { + Assert(dtt.hasAttribute(expr::DatatypeTupleAttr())); + Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType()); + } else { + Assert(dtt.hasAttribute(expr::DatatypeRecordAttr())); + Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType()); + } + Assert(dt.getNumConstructors() == 1); + Assert(dt[0].getNumArgs() > selectorIndex); + Assert(dt[0][selectorIndex].getSelector() == selectorExpr); +#endif /* CVC4_ASSERTIONS */ + Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; + return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); + } if(in.getKind() == kind::APPLY_SELECTOR && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions @@ -90,6 +127,45 @@ public: } } } + if(in.getKind() == kind::TUPLE_SELECT && + in[0].getKind() == kind::TUPLE) { + return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); + } + if(in.getKind() == kind::TUPLE_UPDATE && + in[0].getKind() == kind::TUPLE) { + size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex(); + NodeBuilder<> b(kind::TUPLE); + for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { + if(ix == 0) { + b << in[1]; + } else { + b << *i; + } + } + Node n = b; + Assert(n.getType().isSubtypeOf(in.getType())); + return RewriteResponse(REWRITE_DONE, n); + } + if(in.getKind() == kind::RECORD_SELECT && + in[0].getKind() == kind::RECORD) { + return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]); + } + if(in.getKind() == kind::RECORD_UPDATE && + in[0].getKind() == kind::RECORD) { + size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getConst<RecordUpdate>().getField()); + NodeBuilder<> b(kind::RECORD); + b << in[0].getOperator(); + for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { + if(ix == 0) { + b << in[1]; + } else { + b << *i; + } + } + Node n = b; + Assert(n.getType().isSubtypeOf(in.getType())); + return RewriteResponse(REWRITE_DONE, n); + } if(in.getKind() == kind::EQUAL && in[0] == in[1]) { return RewriteResponse(REWRITE_DONE, @@ -113,7 +189,9 @@ public: static inline void shutdown() {} static bool checkClash( Node n1, Node n2 ) { - if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { + if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || + (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || + (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { if( n1.getOperator() != n2.getOperator() ) { return true; } else { @@ -137,7 +215,8 @@ public: /** is this term a datatype */ static bool isTermDatatype( Node n ){ TypeNode tn = n.getType(); - return tn.isDatatype() || tn.isParametricDatatype(); + return tn.isDatatype() || tn.isParametricDatatype() || + tn.isTuple() || tn.isRecord(); } };/* class DatatypesRewriter */ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index eac3d6eac..d1fbf82bc 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -84,4 +84,72 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule +operator TUPLE_TYPE 1: "tuple type" +cardinality TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +well-founded TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +enumerator TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleEnumerator" \ + "theory/datatypes/type_enumerator.h" + +operator TUPLE 1: "a tuple" +typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule +construle TUPLE ::CVC4::theory::datatypes::TupleProperties + +constant TUPLE_SELECT_OP \ + ::CVC4::TupleSelect \ + ::CVC4::TupleSelectHashFunction \ + "util/tuple.h" \ + "operator for a tuple select" +parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select" +typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule + +constant TUPLE_UPDATE_OP \ + ::CVC4::TupleUpdate \ + ::CVC4::TupleUpdateHashFunction \ + "util/tuple.h" \ + "operator for a tuple update" +parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update" +typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule + +constant RECORD_TYPE \ + ::CVC4::Record \ + "::CVC4::RecordHashFunction" \ + "util/record.h" \ + "record type" +cardinality RECORD_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +well-founded RECORD_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +enumerator RECORD_TYPE \ + "::CVC4::theory::datatypes::RecordEnumerator" \ + "theory/datatypes/type_enumerator.h" + +parameterized RECORD RECORD_TYPE 1: "a record" +typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule +construle RECORD ::CVC4::theory::datatypes::RecordProperties + +constant RECORD_SELECT_OP \ + ::CVC4::RecordSelect \ + ::CVC4::RecordSelectHashFunction \ + "util/record.h" \ + "operator for a record select" +parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select" +typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule + +constant RECORD_UPDATE_OP \ + ::CVC4::RecordUpdate \ + ::CVC4::RecordUpdateHashFunction \ + "util/record.h" \ + "operator for a record update" +parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update" +typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8ec45efb9..6273eb2c2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -22,6 +22,7 @@ #include "util/cvc4_assert.h" #include "theory/datatypes/theory_datatypes_instantiator.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" @@ -94,6 +95,19 @@ void TheoryDatatypes::check(Effort e) { Assertion assertion = get(); TNode fact = assertion.assertion; Trace("datatypes-assert") << "Assert " << fact << std::endl; + + TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact; + + // extra debug check to make sure that the rewriter did its job correctly + Assert( atom.getKind() != kind::EQUAL || + ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE && + atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD && + atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE && + atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE && + atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT && + atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ), + "tuple/record escaped into datatypes decision procedure; should have been rewritten away" ); + //assert the fact assertFact( fact, fact ); flushPendingFacts(); @@ -275,6 +289,90 @@ void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } +Node TheoryDatatypes::ppRewrite(TNode in) { + Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; + + if(in.getKind() == kind::TUPLE_SELECT) { + TypeNode t = in[0].getType(); + if(t.hasAttribute(expr::DatatypeTupleAttr())) { + t = t.getAttribute(expr::DatatypeTupleAttr()); + } + TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]); + } else if(in.getKind() == kind::RECORD_SELECT) { + TypeNode t = in[0].getType(); + if(t.hasAttribute(expr::DatatypeRecordAttr())) { + t = t.getAttribute(expr::DatatypeRecordAttr()); + } + TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); + } + + // we only care about tuples and records here + if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE && + in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) { + // nothing to do + return in; + } + + TypeNode t = in.getType(); + + if(t.hasAttribute(expr::DatatypeTupleAttr())) { + t = t.getAttribute(expr::DatatypeTupleAttr()); + } else if(t.hasAttribute(expr::DatatypeRecordAttr())) { + t = t.getAttribute(expr::DatatypeRecordAttr()); + } + + // if the type doesn't have an associated datatype, then make one for it + TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t; + + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + + // now rewrite the expression + Node n; + if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + b << Node::fromExpr(dt[0].getConstructor()); + b.append(in.begin(), in.end()); + n = b; + } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + b << Node::fromExpr(dt[0].getConstructor()); + size_t size, updateIndex; + if(in.getKind() == kind::TUPLE_UPDATE) { + size = t.getNumChildren(); + updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex(); + } else { // kind::RECORD_UPDATE + const Record& record = t.getConst<Record>(); + size = record.getNumFields(); + updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField()); + } + Debug("tuprec") << "expr is " << in << std::endl; + Debug("tuprec") << "updateIndex is " << updateIndex << std::endl; + Debug("tuprec") << "t is " << t << std::endl; + Debug("tuprec") << "t has arity " << size << std::endl; + for(size_t i = 0; i < size; ++i) { + if(i == updateIndex) { + b << in[1]; + Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; + } else { + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; + } + } + Debug("tuprec") << "builder says " << b << std::endl; + n = b; + } + + Assert(!n.isNull()); + + Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; + + return n; +} + void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " << t << endl; @@ -719,7 +817,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); collectTerms( n_ic ); //add type ascription for ambiguous constructor types - if( n_ic.getType()!=n.getType() ){ + if(!n_ic.getType().isComparableTo(n.getType())) { Assert( dt.isParametric() ); Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 5cda9eeae..4380eca58 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -52,6 +52,7 @@ private: /** inferences */ NodeList d_infer; NodeList d_infer_exp; + private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -202,6 +203,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index eb50def01..ade9ffc26 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #include "util/matcher.h" +#include "expr/attribute.h" namespace CVC4 { @@ -70,7 +71,7 @@ struct DatatypeConstructorTypeRule { TypeNode childType = (*child_it).getType(check); Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; - if(!childType.isSubtypeOf(argumentType)) { + if(!childType.isComparableTo(argumentType)) { std::stringstream ss; ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot : " << childType; throw TypeCheckingExceptionPrivate(n, ss.str()); @@ -127,7 +128,7 @@ struct DatatypeSelectorTypeRule { Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; Debug("typecheck-idt") << "sel type: " << selType << std::endl; TypeNode childType = n[0].getType(check); - if(selType[0] != childType) { + if(!selType[0].isComparableTo(childType)) { Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl; throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); } @@ -150,16 +151,16 @@ struct DatatypeTesterTypeRule { Type t = testType[0].toType(); Assert( t.isDatatype() ); DatatypeType dt = DatatypeType(t); - if( dt.isParametric() ){ + if(dt.isParametric()) { Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl; Matcher m( dt ); if( !m.doMatching( testType[0], childType ) ){ throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype"); } - }else{ + } else { Debug("typecheck-idt") << "typecheck test: " << n << std::endl; Debug("typecheck-idt") << "test type: " << testType << std::endl; - if(testType[0] != childType) { + if(!testType[0].isComparableTo(childType)) { throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); } } @@ -265,6 +266,231 @@ struct ConstructorProperties { } };/* struct ConstructorProperties */ +struct TupleTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE); + std::vector<TypeNode> types; + for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); + child_it != child_it_end; + ++child_it) { + types.push_back((*child_it).getType(check)); + } + return nodeManager->mkTupleType(types); + } +};/* struct TupleTypeRule */ + +struct TupleSelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE_SELECT); + const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); + TypeNode tupleType = n[0].getType(check); + if(!tupleType.isTuple()) { + if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple"); + } + tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); + } + if(ts.getIndex() >= tupleType.getNumChildren()) { + std::stringstream ss; + ss << "Tuple-select expression index `" << ts.getIndex() + << "' is not a valid index; tuple type only has " + << tupleType.getNumChildren() << " fields"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + return tupleType[ts.getIndex()]; + } +};/* struct TupleSelectTypeRule */ + +struct TupleUpdateTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE_UPDATE); + const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>(); + TypeNode tupleType = n[0].getType(check); + TypeNode newValue = n[1].getType(check); + if(check) { + if(!tupleType.isTuple()) { + if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); + } + tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); + } + if(tu.getIndex() >= tupleType.getNumChildren()) { + std::stringstream ss; + ss << "Tuple-update expression index `" << tu.getIndex() + << "' is not a valid index; tuple type only has " + << tupleType.getNumChildren() << " fields"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + } + return tupleType; + } +};/* struct TupleUpdateTypeRule */ + +struct TupleProperties { + inline static Cardinality computeCardinality(TypeNode type) { + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); + + Cardinality card(1); + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + card *= (*i).getCardinality(); + } + + return card; + } + + inline static bool isWellFounded(TypeNode type) { + // Don't assert this; allow other theories to use this + // wellfoundedness computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); + + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + if(! (*i).isWellFounded()) { + return false; + } + } + + return true; + } + + inline static Node mkGroundTerm(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + std::vector<Node> children; + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + children.push_back((*i).mkGroundTerm()); + } + + return NodeManager::currentNM()->mkNode(kind::TUPLE, children); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::TUPLE); + NodeManagerScope nms(nodeManager); + + for(TNode::iterator i = n.begin(), + i_end = n.end(); + i != i_end; + ++i) { + if(! (*i).isConst()) { + return false; + } + } + + return true; + } +};/* struct TupleProperties */ + +struct RecordTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD); + NodeManagerScope nms(nodeManager); + const Record& rec = n.getOperator().getConst<Record>(); + if(check) { + Record::iterator i = rec.begin(); + for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); + child_it != child_it_end; + ++child_it, ++i) { + if(i == rec.end()) { + throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); + } + if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) { + throw TypeCheckingExceptionPrivate(n, "record description types differ from record literal types"); + } + } + if(i != rec.end()) { + throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); + } + } + return nodeManager->mkRecordType(rec); + } +};/* struct RecordTypeRule */ + +struct RecordSelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD_SELECT); + NodeManagerScope nms(nodeManager); + const RecordSelect& rs = n.getOperator().getConst<RecordSelect>(); + TypeNode recordType = n[0].getType(check); + if(!recordType.isRecord()) { + if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record"); + } + recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); + } + const Record& rec = recordType.getRecord(); + Record::const_iterator field = rec.find(rs.getField()); + if(field == rec.end()) { + std::stringstream ss; + ss << "Record-select field `" << rs.getField() + << "' is not a valid field name for the record type"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + return TypeNode::fromType((*field).second); + } +};/* struct RecordSelectTypeRule */ + +struct RecordUpdateTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD_UPDATE); + NodeManagerScope nms(nodeManager); + const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>(); + TypeNode recordType = n[0].getType(check); + TypeNode newValue = n[1].getType(check); + if(check) { + if(!recordType.isRecord()) { + if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); + } + recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); + } + const Record& rec = recordType.getRecord(); + Record::const_iterator field = rec.find(ru.getField()); + if(field == rec.end()) { + std::stringstream ss; + ss << "Record-update field `" << ru.getField() + << "' is not a valid field name for the record type"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + } + return recordType; + } +};/* struct RecordUpdateTypeRule */ + +struct RecordProperties { + inline static Node mkGroundTerm(TypeNode type) { + Unimplemented(); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::RECORD); + NodeManagerScope nms(nodeManager); + + for(TNode::iterator i = n.begin(), + i_end = n.end(); + i != i_end; + ++i) { + if(! (*i).isConst()) { + return false; + } + } + + return true; + } +};/* struct RecordProperties */ + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 0f365bd71..ea68e8957 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -147,6 +147,146 @@ public: };/* DatatypesEnumerator */ +class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { + TypeEnumerator** d_enumerators; + + void deleteEnumerators() throw() { + if(d_enumerators != NULL) { + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + delete d_enumerators[i]; + } + delete [] d_enumerators; + d_enumerators = NULL; + } + } + +public: + + TupleEnumerator(TypeNode type) throw() : + TypeEnumeratorBase<TupleEnumerator>(type) { + Assert(type.isTuple()); + d_enumerators = new TypeEnumerator*[type.getNumChildren()]; + for(size_t i = 0; i < type.getNumChildren(); ++i) { + d_enumerators[i] = new TypeEnumerator(type[i]); + } + } + + ~TupleEnumerator() throw() { + deleteEnumerators(); + } + + Node operator*() throw(NoMoreValuesException) { + if(isFinished()) { + throw NoMoreValuesException(getType()); + } + + NodeBuilder<> nb(kind::TUPLE); + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + nb << **d_enumerators[i]; + } + return Node(nb); + } + + TupleEnumerator& operator++() throw() { + if(isFinished()) { + return *this; + } + + size_t i; + for(i = 0; i < getType().getNumChildren(); ++i) { + if(d_enumerators[i]->isFinished()) { + *d_enumerators[i] = TypeEnumerator(getType()[i]); + } else { + ++*d_enumerators[i]; + return *this; + } + } + + deleteEnumerators(); + + return *this; + } + + bool isFinished() throw() { + return d_enumerators == NULL; + } + +};/* TupleEnumerator */ + +class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> { + TypeEnumerator** d_enumerators; + + void deleteEnumerators() throw() { + if(d_enumerators != NULL) { + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + delete d_enumerators[i]; + } + delete [] d_enumerators; + d_enumerators = NULL; + } + } + +public: + + RecordEnumerator(TypeNode type) throw() : + TypeEnumeratorBase<RecordEnumerator>(type) { + Assert(type.isRecord()); + const Record& rec = getType().getConst<Record>(); + Debug("te") << "creating record enumerator for " << type << std::endl; + d_enumerators = new TypeEnumerator*[rec.getNumFields()]; + for(size_t i = 0; i < rec.getNumFields(); ++i) { + Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl; + d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second)); + } + } + + ~RecordEnumerator() throw() { + deleteEnumerators(); + } + + Node operator*() throw(NoMoreValuesException) { + if(isFinished()) { + throw NoMoreValuesException(getType()); + } + + NodeBuilder<> nb(kind::RECORD); + Debug("te") << "record enumerator: creating record of type " << getType() << std::endl; + nb << getType(); + const Record& rec = getType().getConst<Record>(); + for(size_t i = 0; i < rec.getNumFields(); ++i) { + Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl; + nb << **d_enumerators[i]; + } + return Node(nb); + } + + RecordEnumerator& operator++() throw() { + if(isFinished()) { + return *this; + } + + size_t i; + const Record& rec = getType().getConst<Record>(); + for(i = 0; i < rec.getNumFields(); ++i) { + if(d_enumerators[i]->isFinished()) { + *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second)); + } else { + ++*d_enumerators[i]; + return *this; + } + } + + deleteEnumerators(); + + return *this; + } + + bool isFinished() throw() { + return d_enumerators == NULL; + } + +};/* RecordEnumerator */ + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 8dacf86e9..66f0c8824 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/type_enumerator.h" #include "smt/options.h" +#include "smt/smt_engine.h" #include "theory/uf/theory_uf_model.h" using namespace std; @@ -56,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{ Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); - return ret.toExpr(); + return d_smt.postprocess(ret).toExpr(); } /** get cardinality for sort */ diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 9add67441..42cb998be 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -97,8 +97,40 @@ public: ~TypeEnumerator() { delete d_te; } - bool isFinished() throw() { return d_te->isFinished(); } - Node operator*() throw(NoMoreValuesException) { return **d_te; } + bool isFinished() throw() { +#ifdef CVC4_ASSERTIONS + if(d_te->isFinished()) { + try { + **d_te; + Assert(false, "expected an NoMoreValuesException to be thrown"); + } catch(NoMoreValuesException&) { + // ignore the exception, we're just asserting that it would be thrown + } + } else { + try { + **d_te; + } catch(NoMoreValuesException&) { + Assert(false, "didn't expect a NoMoreValuesException to be thrown"); + } + } +#endif /* CVC4_ASSERTIONS */ + return d_te->isFinished(); + } + Node operator*() throw(NoMoreValuesException) { +#ifdef CVC4_ASSERTIONS + try { + Node n = **d_te; + Assert(n.isConst()); + Assert(! isFinished()); + return n; + } catch(NoMoreValuesException&) { + Assert(isFinished()); + throw; + } +#else /* CVC4_ASSERTIONS */ + return **d_te; +#endif /* CVC4_ASSERTIONS */ + } TypeEnumerator& operator++() throw() { ++*d_te; return *this; } TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e72706ea3..804bcde11 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,9 @@ libutil_la_SOURCES = \ array.h \ datatype.h \ datatype.cpp \ + tuple.h \ + record.h \ + record.cpp \ matcher.h \ gmp_util.h \ sexpr.h \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index a225339cd..be98e40e1 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -558,6 +558,7 @@ Expr DatatypeConstructor::getConstructor() const { Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + ExprManagerScope ems(d_constructor); const Datatype& dt = Datatype::datatypeOf(d_constructor); CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); DatatypeType dtt = dt.getDatatypeType(); diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index ad21be287..07e85c118 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -59,7 +59,9 @@ private: void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) { try { if(s.find_first_not_of('0') == std::string::npos) { - // string of all zeroes, CLN has a bug for these inputs + // String of all zeroes, CLN has a bug for these inputs up to and + // including CLN v1.3.2. + // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details. d_value = read_integer(flags, "0", NULL, NULL); } else { d_value = read_integer(flags, s.c_str(), NULL, NULL); diff --git a/src/util/record.cpp b/src/util/record.cpp new file mode 100644 index 000000000..f3dc29f81 --- /dev/null +++ b/src/util/record.cpp @@ -0,0 +1,40 @@ +/********************* */ +/*! \file record.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a record definition + ** + ** A class representing a record definition. + **/ + +#include "util/record.h" + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const Record& r) { + os << "[# "; + bool first = true; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + if(!first) { + os << ", "; + } + os << (*i).first << ":" << (*i).second; + first = false; + } + os << " #]"; + + return os; +} + +}/* CVC4 namespace */ diff --git a/src/util/record.h b/src/util/record.h new file mode 100644 index 000000000..2c15d30e0 --- /dev/null +++ b/src/util/record.h @@ -0,0 +1,156 @@ +/********************* */ +/*! \file record.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a Record definition + ** + ** A class representing a Record definition. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RECORD_H +#define __CVC4__RECORD_H + +#include <iostream> +#include <string> +#include <vector> +#include <utility> +#include "util/hash.h" + +namespace CVC4 { + +class Record; + +// operators for record select and update + +class CVC4_PUBLIC RecordSelect { + std::string d_field; +public: + RecordSelect(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; } +};/* class RecordSelect */ + +class CVC4_PUBLIC RecordUpdate { + std::string d_field; +public: + RecordUpdate(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; } +};/* class RecordUpdate */ + +struct CVC4_PUBLIC RecordSelectHashFunction { + inline size_t operator()(const RecordSelect& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordSelectHashFunction */ + +struct CVC4_PUBLIC RecordUpdateHashFunction { + inline size_t operator()(const RecordUpdate& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordUpdateHashFunction */ + +std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) { + return out << "[" << t.getField() << "]"; +} + +inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { + return out << "[" << t.getField() << "]"; +} + +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" + +namespace CVC4 { + +// now an actual record definition + +class CVC4_PUBLIC Record { + std::vector< std::pair<std::string, Type> > d_fields; + +public: + + typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator; + typedef const_iterator iterator; + + Record(const std::vector< std::pair<std::string, Type> >& fields) : + d_fields(fields) { + CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty"); + } + + const_iterator find(std::string name) const { + const_iterator i; + for(i = begin(); i != end(); ++i) { + if((*i).first == name) { + break; + } + } + return i; + } + + size_t getIndex(std::string name) const { + const_iterator i = find(name); + CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str()); + return i - begin(); + } + + size_t getNumFields() const { + return d_fields.size(); + } + + const_iterator begin() const { + return d_fields.begin(); + } + + const_iterator end() const { + return d_fields.end(); + } + + std::pair<std::string, Type> operator[](size_t index) const { + CheckArgument(index < d_fields.size(), index, "index out of bounds for record type"); + return d_fields[index]; + } + + bool operator==(const Record& r) const { + return d_fields == r.d_fields; + } + + bool operator!=(const Record& r) const { + return !(*this == r); + } + +};/* class Record */ + +struct CVC4_PUBLIC RecordHashFunction { + inline size_t operator()(const Record& r) const { + size_t n = 0; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + n = (n << 3) ^ TypeHashFunction()((*i).second); + } + return n; + } +};/* struct RecordHashFunction */ + +std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RECORD_H */ diff --git a/src/util/record.i b/src/util/record.i new file mode 100644 index 000000000..f662178c2 --- /dev/null +++ b/src/util/record.i @@ -0,0 +1,5 @@ +%{ +#include "util/record.h" +%} + +%include "util/record.h" diff --git a/src/util/tuple.h b/src/util/tuple.h new file mode 100644 index 000000000..6c1e981a4 --- /dev/null +++ b/src/util/tuple.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file tuple.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Tuple operators + ** + ** Tuple operators. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__TUPLE_H +#define __CVC4__TUPLE_H + +#include <iostream> +#include <string> +#include <vector> +#include <utility> + +namespace CVC4 { + +class CVC4_PUBLIC TupleSelect { + unsigned d_index; +public: + TupleSelect(unsigned index) throw() : d_index(index) { } + unsigned getIndex() const throw() { return d_index; } + bool operator==(const TupleSelect& t) const throw() { return d_index == t.d_index; } + bool operator!=(const TupleSelect& t) const throw() { return d_index != t.d_index; } +};/* class TupleSelect */ + +class CVC4_PUBLIC TupleUpdate { + unsigned d_index; +public: + TupleUpdate(unsigned index) throw() : d_index(index) { } + unsigned getIndex() const throw() { return d_index; } + bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; } + bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; } +};/* class TupleUpdate */ + +struct CVC4_PUBLIC TupleSelectHashFunction { + inline size_t operator()(const TupleSelect& t) const { + return t.getIndex(); + } +};/* struct TupleSelectHashFunction */ + +struct CVC4_PUBLIC TupleUpdateHashFunction { + inline size_t operator()(const TupleUpdate& t) const { + return t.getIndex(); + } +};/* struct TupleUpdateHashFunction */ + +std::ostream& operator<<(std::ostream& out, const TupleSelect& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const TupleSelect& t) { + return out << "[" << t.getIndex() << "]"; +} + +inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { + return out << "[" << t.getIndex() << "]"; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__TUPLE_H */ diff --git a/src/util/tuple.i b/src/util/tuple.i new file mode 100644 index 000000000..d7301d201 --- /dev/null +++ b/src/util/tuple.i @@ -0,0 +1,5 @@ +%{ +#include "util/tuple.h" +%} + +%include "util/tuple.h" diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp index bb2924b51..0c058fce9 100644 --- a/src/util/util_model.cpp +++ b/src/util/util_model.cpp @@ -36,11 +36,17 @@ Model::Model() : } size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size(); + return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); } const Command* Model::getCommand(size_t i) const { - return (*d_smt.d_modelCommands)[i]; + Assert(i < getNumCommands()); + // index the global commands first, then the locals + if(i < d_smt.d_modelGlobalCommands.size()) { + return d_smt.d_modelGlobalCommands[i]; + } else { + return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; + } } }/* CVC4 namespace */ diff --git a/src/util/util_model.h b/src/util/util_model.h index 72ff8af60..21c3fb400 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -35,8 +35,8 @@ class Model { friend std::ostream& operator<<(std::ostream&, Model&); protected: - /** The SmtEngine we're associated to */ - const SmtEngine& d_smt; + /** The SmtEngine we're associated with */ + SmtEngine& d_smt; /** construct the base class; users cannot do this, only CVC4 internals */ Model(); @@ -48,6 +48,8 @@ public: size_t getNumCommands() const; /** get command */ const Command* getCommand(size_t i) const; + /** get the smt engine that this model is hooked up to */ + SmtEngine* getSmtEngine() { return &d_smt; } public: /** get value for expression */ diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 458b42843..a3392f0f3 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -45,6 +45,7 @@ TESTS = \ wrong-sel-simp.cvc FAILING_TESTS = \ + bug438.cvc \ datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/bug438.cvc b/test/regress/regress0/datatypes/bug438.cvc new file mode 100644 index 000000000..05079d287 --- /dev/null +++ b/test/regress/regress0/datatypes/bug438.cvc @@ -0,0 +1,6 @@ +% EXPECT: sat +% EXIT: 10 +DATATYPE list[T] = cons(car:T, cdr:list[T]) | nil END; +x : list[REAL]; +ASSERT x = cons(1.0,nil::list[REAL])::list[REAL]; +CHECKSAT; |