diff options
25 files changed, 383 insertions, 938 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index ed8478ee8..f2ef9b95f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1782,14 +1782,16 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { CVC4::Type t = recordType(field, expr.getType()); - return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1) { CVC4::Type t = recordType(field0, expr0.getType(), field1, expr1.getType()); - return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, @@ -1798,7 +1800,8 @@ Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, CVC4::Type t = recordType(field0, expr0.getType(), field1, expr1.getType(), field2, expr2.getType()); - return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1, expr2); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1, expr2); } Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields, @@ -1808,11 +1811,16 @@ Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields, types.push_back(exprs[i].getType()); } CVC4::Type t = recordType(fields, types); - return d_em->mkExpr(d_em->mkConst(CVC4::RecordType(t).getRecord()), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs)); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs)); } Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { - return d_em->mkExpr(d_em->mkConst(CVC4::RecordSelect(field)), record); + Type t = record.getType(); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + const CVC4::Record& rec = t.getRecord(); + unsigned index = rec.getIndex(field); + return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record); } Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, @@ -2200,15 +2208,23 @@ Rational ValidityChecker::computeBVConst(const Expr& e) { } Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { - const vector<CVC4::Expr>& v = - *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs); - return d_em->mkExpr(CVC4::kind::TUPLE, v); + std::vector< Type > types; + std::vector<CVC4::Expr> v; + for( unsigned i=0; i<exprs.size(); i++ ){ + types.push_back( exprs[i].getType() ); + v.push_back( exprs[i] ); + } + Type t = tupleType( types ); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + v.insert( v.begin(), dt[0].getConstructor() ); + return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, v); } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(), + CompatCheckArgument(index >= 0 && index < tuple.getType().getTupleLength(), "invalid index in tuple select"); - return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)tuple.getType()).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), tuple); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index b9870afb4..32c0bb6dd 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -151,6 +151,13 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_allow_all = allow_all; } +void Datatype::setTuple() { + d_isTuple = true; +} + +void Datatype::setRecord() { + d_isRecord = true; +} Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); @@ -663,7 +670,6 @@ void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& d_sygus_num_let_input_args = num_let_input_args; } - void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // We don't want to introduce a new data member, because eventually // we're going to be a constant stuffed inside a node. So we stow diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 5f80c54f7..625fbb5d4 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -237,9 +237,6 @@ public: */ DatatypeConstructor(std::string name, std::string tester); - /** set sygus */ - void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); - /** * Add an argument (i.e., a data field) of the given name and type * to this Datatype constructor. Selector names need not be unique; @@ -382,6 +379,8 @@ public: bool involvesExternalType() const; bool involvesUninterpretedType() const; + /** set sygus */ + void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); };/* class DatatypeConstructor */ /** @@ -473,6 +472,8 @@ private: std::string d_name; std::vector<Type> d_params; bool d_isCo; + bool d_isTuple; + bool d_isRecord; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -565,6 +566,12 @@ public: */ void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); + /** set tuple */ + void setTuple(); + + /** set tuple */ + void setRecord(); + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -589,6 +596,12 @@ public: /** is this a sygus datatype? */ inline bool isSygus() const; + /** is this a tuple datatype? */ + inline bool isTuple() const; + + /** is this a record datatype? */ + inline bool isRecord() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -757,6 +770,8 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -771,6 +786,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_name(name), d_params(params), d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -819,6 +836,14 @@ inline bool Datatype::isSygus() const { return !d_sygus_type.isNull(); } +inline bool Datatype::isTuple() const { + return d_isTuple; +} + +inline bool Datatype::isRecord() const { + return d_isRecord; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 0b9557cc8..ce7a92b48 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -20,6 +20,7 @@ #include "expr/node_manager.h" #include "expr/variable_type_map.h" +#include "expr/node_manager_attributes.h" #include "options/options.h" #include "util/statistics_registry.h" @@ -596,18 +597,18 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); } -TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { +DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) { NodeManagerScope nms(d_nodeManager); std::vector<TypeNode> typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); } - return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); + return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } -RecordType ExprManager::mkRecordType(const Record& rec) { +DatatypeType ExprManager::mkRecordType(const Record& rec) { NodeManagerScope nms(d_nodeManager); - return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); + return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); } SExprType ExprManager::mkSExprType(const std::vector<Type>& types) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index e65cfc358..37ef128f4 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -341,12 +341,12 @@ public: * <code>types[0..types.size()-1]</code>. <code>types</code> must * have at least one element. */ - TupleType mkTupleType(const std::vector<Type>& types); + DatatypeType mkTupleType(const std::vector<Type>& types); /** * Make a record type with types from the rec parameter. */ - RecordType mkRecordType(const Record& rec); + DatatypeType mkRecordType(const Record& rec); /** * Make a symbolic expressiontype with types from diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e52776fce..e6e44928d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(bounds)); } -TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { - Assert(t.isTuple() || t.isRecord()); - - //AJR: not sure why .getBaseType() was used in two cases below, - // disabling this, which is necessary to fix bug 605/667, - // which involves records of INT which were mapped to records of REAL below. - TypeNode tOrig = t; - if(t.isTuple()) { - vector<TypeNode> v; - bool changed = false; - for(size_t i = 0; i < t.getNumChildren(); ++i) { - TypeNode tn = t[i]; - TypeNode base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(tn); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(base); - } - if(changed) { - t = mkTupleType(v); - } - } else { - const Record& r = t.getRecord(); - std::vector< std::pair<std::string, Type> > v; - bool changed = false; - const Record::FieldVector& fields = r.getFields(); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - Type tn = (*i).second; - Type base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType(); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(std::make_pair((*i).first, base)); - } - if(changed) { - t = mkRecordType(Record(v)); +TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { + std::vector< TypeNode > ts; + Debug("tuprec-debug") << "Make tuple type : "; + for (unsigned i = 0; i < types.size(); ++ i) { + CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); + ts.push_back( types[i] ); + Debug("tuprec-debug") << types[i] << " "; + } + Debug("tuprec-debug") << std::endl; + //index based on function type + TypeNode tindex; + if( types.empty() ){ + //do nothing (will index on null type) + }else if( types.size()==1 ){ + tindex = types[0]; + }else{ + TypeNode tt = ts.back(); + ts.pop_back(); + tindex = mkFunctionType( ts, tt ); + ts.push_back( tt ); + } + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; + if(dtt.isNull()) { + Datatype dt("__cvc4_tuple"); + dt.setTuple(); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for (unsigned i = 0; i < ts.size(); ++ i) { + std::stringstream ss; + ss << "__cvc4_tuple_stor_" << i; + c.addArg(ss.str().c_str(), ts[i].toType()); } + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeTupleAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } + Assert(!dtt.isNull()); + return dtt; +} - // if the type doesn't have an associated datatype, then make one for it - TypeNode& dtt = d_tupleAndRecordTypes[t]; +TypeNode NodeManager::mkRecordType(const Record& rec) { + //index based on type constant + TypeNode tindex = mkTypeConst(rec); + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; 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; - dtt.setAttribute(DatatypeTupleAttr(), tOrig); - } else { - const Record& rec = t.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - Datatype dt("__cvc4_record"); - DatatypeConstructor c("__cvc4_record_ctor"); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.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(), tOrig); + const Record::FieldVector& fields = rec.getFields(); + Datatype dt("__cvc4_record"); + dt.setRecord(); + DatatypeConstructor c("__cvc4_record_ctor"); + for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { + c.addArg((*i).first, (*i).second); } - } else { - Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl; + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeRecordAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } Assert(!dtt.isNull()); return dtt; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1ae9f1e8e..45c9afbde 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -756,7 +756,7 @@ public: * @param types a vector of types * @returns the tuple type (types[0], ..., types[n]) */ - inline TypeNode mkTupleType(const std::vector<TypeNode>& types); + TypeNode mkTupleType(const std::vector<TypeNode>& types); /** * Make a record type with the description from rec. @@ -764,7 +764,7 @@ public: * @param rec a description of the record * @returns the record type */ - inline TypeNode mkRecordType(const Record& rec); + TypeNode mkRecordType(const Record& rec); /** * Make a symbolic expression type with types from @@ -839,12 +839,6 @@ 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 @@ -1063,20 +1057,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { - std::vector<TypeNode> typeNodes; - for (unsigned i = 0; i < types.size(); ++ i) { - CheckArgument(!types[i].isFunctionLike(), types, - "cannot put function-like types in tuples"); - typeNodes.push_back(types[i]); - } - 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) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 99d04d658..6a8e6609c 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -292,6 +292,29 @@ bool Type::isRecord() const { return d_typeNode->isRecord(); } +/** Get the length of a tuple type */ +size_t Type::getTupleLength() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getTupleLength(); +} + +/** Get the constituent types of a tuple type */ +std::vector<Type> Type::getTupleTypes() const { + NodeManagerScope nms(d_nodeManager); + std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); + std::vector< Type > vect; + for( unsigned i=0; i<vec.size(); i++ ){ + vect.push_back( vec[i].toType() ); + } + return vect; +} + +/** Get the description of the record type */ +const Record& Type::getRecord() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getRecord(); +} + /** Is this a symbolic expression type? */ bool Type::isSExpr() const { NodeManagerScope nms(d_nodeManager); @@ -358,27 +381,6 @@ 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; - vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); - vector<TypeNode>::iterator it = typeNodes.begin(); - vector<TypeNode>::iterator it_end = typeNodes.end(); - for(; it != it_end; ++ it) { - types.push_back(makeType(*it)); - } - 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; @@ -488,16 +490,6 @@ FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) PrettyCheckArgument(isNull() || isFunction(), this); } -TupleType::TupleType(const Type& t) throw(IllegalArgumentException) - : Type(t) { - PrettyCheckArgument(isNull() || isTuple(), this); -} - -RecordType::RecordType(const Type& t) throw(IllegalArgumentException) - : Type(t) { - PrettyCheckArgument(isNull() || isRecord(), this); -} - SExprType::SExprType(const Type& t) throw(IllegalArgumentException) : Type(t) { PrettyCheckArgument(isNull() || isSExpr(), this); diff --git a/src/expr/type.h b/src/expr/type.h index 0f2118c44..b7ea14f78 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -56,8 +56,6 @@ class ConstructorType; class SelectorType; class TesterType; class FunctionType; -class TupleType; -class RecordType; class SExprType; class SortType; class SortConstructorType; @@ -302,6 +300,15 @@ public: */ bool isRecord() const; + /** Get the length of a tuple type */ + size_t getTupleLength() const; + + /** Get the constituent types of a tuple type */ + std::vector<Type> getTupleTypes() const; + + /** Get the description of the record type */ + const Record& getRecord() const; + /** * Is this a symbolic expression type? * @return true if the type is a symbolic expression type @@ -459,39 +466,7 @@ public: };/* class FunctionType */ /** - * Class encapsulating a tuple type. - */ -class CVC4_PUBLIC TupleType : public Type { - -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 encapsulating a sexpr type. */ class CVC4_PUBLIC SExprType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ea185f98b..755b16e46 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -94,9 +94,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } } if(isTuple() || isRecord()) { - if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { - return true; - } if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { return false; } @@ -111,8 +108,8 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } } } else { - const Record& r1 = getConst<Record>(); - const Record& r2 = t.getConst<Record>(); + const Record& r1 = getRecord(); + const Record& r2 = t.getRecord(); if(r1.getNumFields() != r2.getNumFields()) { return false; } @@ -166,12 +163,8 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(t.isDatatype() && (isTuple() || isRecord())) { + if(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()) { return false; } @@ -186,8 +179,8 @@ bool TypeNode::isComparableTo(TypeNode t) const { } } } else { - const Record& r1 = getConst<Record>(); - const Record& r2 = t.getConst<Record>(); + const Record& r1 = getRecord(); + const Record& r2 = t.getRecord(); if(r1.getNumFields() != r2.getNumFields()) { return false; } @@ -202,12 +195,7 @@ bool TypeNode::isComparableTo(TypeNode t) const { } } 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); } else if(isParametricDatatype() && t.isParametricDatatype()) { Assert(getKind() == kind::PARAMETRIC_DATATYPE); Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); @@ -244,8 +232,6 @@ 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(); } else if (isParametricDatatype()) { @@ -282,23 +268,40 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { return params; } + +/** Is this a tuple type? */ +bool TypeNode::isTuple() const { + return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) || + ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); +} + +/** Is this a record type? */ +bool TypeNode::isRecord() const { + return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) || + ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); +} + size_t TypeNode::getTupleLength() const { Assert(isTuple()); - return getNumChildren(); + const Datatype& dt = getConst<Datatype>(); + Assert(dt.getNumConstructors()==1); + return dt[0].getNumArgs(); } vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); + const Datatype& dt = getConst<Datatype>(); + Assert(dt.getNumConstructors()==1); vector<TypeNode> types; - for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { - types.push_back((*this)[i]); + for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { + types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType())); } return types; } const Record& TypeNode::getRecord() const { Assert(isRecord()); - return getConst<Record>(); + return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); } vector<TypeNode> TypeNode::getSExprTypes() const { @@ -446,6 +449,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(t1.isInteger()); return TypeNode(); } +/* case kind::TUPLE_TYPE: { // if the other == this one, we returned already, above if(t0.getBaseType() == t1) { @@ -495,6 +499,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ // if we make it here, we constructed the least common type return NodeManager::currentNM()->mkRecordType(Record(fields)); } +*/ case kind::DATATYPE_TYPE: // t1 might be a subtype tuple or record if(t1.getBaseType() == t0) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 59f602f09..4c48cc3ca 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -929,18 +929,6 @@ inline TypeNode TypeNode::getRangeType() const { return (*this)[getNumChildren() - 1]; } -/** Is this a tuple type? */ -inline bool TypeNode::isTuple() const { - return getKind() == kind::TUPLE_TYPE || - ( 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 || @@ -973,7 +961,6 @@ 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() ); } @@ -1027,11 +1014,7 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** 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>(); - } + return getConst<Datatype>(); } /** Get the exponent size of this floating-point type */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d57aea93c..4aff5cd2f 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1103,7 +1103,7 @@ type[CVC4::Type& t, : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { assert(t.isTuple()); - args = TupleType(t).getTypes(); + args = t.getTupleTypes(); } else { args.push_back(t); } @@ -1539,13 +1539,17 @@ tupleStore[CVC4::Expr& f] if(! t.isTuple()) { PARSER_STATE->parseError("tuple-update applied to non-tuple"); } - size_t length = TupleType(t).getLength(); + size_t length = t.getTupleLength(); if(k >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot update index " << k; PARSER_STATE->parseError(ss.str()); } - f2 = MK_EXPR(MK_CONST(TupleSelect(k)), f); + std::vector<Expr> args; + const Datatype & dt = ((DatatypeType)t).getDatatype(); + args.push_back( dt[0][k].getSelector() ); + args.push_back( f ); + f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1572,11 +1576,15 @@ recordStore[CVC4::Expr& f] << "its type: " << t; PARSER_STATE->parseError(ss.str()); } - const Record& rec = RecordType(t).getRecord(); + const Record& rec = t.getRecord(); if(! rec.contains(id)) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f); + std::vector<Expr> args; + const Datatype & dt = ((DatatypeType)t).getDatatype(); + args.push_back( dt[0][id].getSelector() ); + args.push_back( f ); + f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1699,24 +1707,32 @@ postfixTerm[CVC4::Expr& f] if(! t.isRecord()) { PARSER_STATE->parseError("record-select applied to non-record"); } - const Record& rec = RecordType(t).getRecord(); + const Record& rec = t.getRecord(); if(!rec.contains(id)){ PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - f = MK_EXPR(MK_CONST(RecordSelect(id)), f); + const Datatype & dt = ((DatatypeType)t).getDatatype(); + std::vector<Expr> sargs; + sargs.push_back( dt[0][id].getSelector() ); + sargs.push_back( f ); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs); } | k=numeral { Type t = f.getType(); if(! t.isTuple()) { PARSER_STATE->parseError("tuple-select applied to non-tuple"); } - size_t length = TupleType(t).getLength(); + size_t length = t.getTupleLength(); if(k >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot access index " << k; PARSER_STATE->parseError(ss.str()); } - f = MK_EXPR(MK_CONST(TupleSelect(k)), f); + const Datatype & dt = ((DatatypeType)t).getDatatype(); + std::vector<Expr> sargs; + sargs.push_back( dt[0][k].getSelector() ); + sargs.push_back( f ); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs); } ) )* @@ -1937,20 +1953,25 @@ simpleTerm[CVC4::Expr& f] for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { types.push_back((*i).getType()); } - TupleType t = EXPR_MANAGER->mkTupleType(types); - f = MK_EXPR(kind::TUPLE, args); + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert( args.begin(), dt[0].getConstructor() ); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } } /* empty tuple literal */ | LPAREN RPAREN - { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); } + { std::vector<Type> types; + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } /* empty record literal */ | PARENHASH HASHPAREN - { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); - f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>()); + { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); + const Datatype& dt = t.getDatatype(); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } - /* empty set literal */ | LBRACE RBRACE { f = MK_CONST(EmptySet(Type())); } @@ -2016,8 +2037,10 @@ simpleTerm[CVC4::Expr& f] for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } - RecordType t = EXPR_MANAGER->mkRecordType(typeIds); - f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args); + DatatypeType t = EXPR_MANAGER->mkRecordType(typeIds); + const Datatype& dt = t.getDatatype(); + args.insert( args.begin(), dt[0].getConstructor() ); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } /* variable / zero-ary constructor application */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 25f958963..b525c4329 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -162,8 +162,32 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } break; - case kind::DATATYPE_TYPE: - out << n.getConst<Datatype>().getName(); + case kind::DATATYPE_TYPE: { + const Datatype& dt = n.getConst<Datatype>(); + if( dt.isTuple() ){ + out << '['; + for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { + if (i > 0) { + out << ", "; + } + Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + out << t; + } + out << ']'; + }else if( dt.isRecord() ){ + out << "[# "; + for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { + if (i > 0) { + out << ", "; + } + Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + out << dt[0][i].getSelector() << ":" << t; + } + out << " #]"; + }else{ + out << dt.getName(); + } + } break; case kind::EMPTYSET: @@ -214,7 +238,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << " ENDIF"; return; break; - case kind::TUPLE_TYPE: case kind::SEXPR_TYPE: out << '['; for (unsigned i = 0; i < n.getNumChildren(); ++ i) { @@ -329,9 +352,48 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } return; break; - case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_CONSTRUCTOR: { + TypeNode t = n.getType(); + if( t.isTuple() ){ + //no-op + }else if( t.isRecord() ){ + const Record& rec = t.getRecord(); + out << "(# "; + TNode::iterator i = n.begin(); + bool first = true; + const Record::FieldVector& fields = rec.getFields(); + for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { + if(!first) { + out << ", "; + } + out << (*j).first << " := "; + toStream(out, *i, depth, types, false); + first = false; + } + out << " #)"; + return; + }else{ + toStream(op, n.getOperator(), depth, types, false); + } + } + break; case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: + case kind::APPLY_SELECTOR_TOTAL: { + TypeNode t = n.getType(); + if( t.isTuple() ){ + toStream(out, n[0], depth, types, true); + out << '.' << Datatype::indexOf( n.getOperator().toExpr() ); + }else if( t.isRecord() ){ + toStream(out, n[0], depth, types, true); + const Record& rec = t.getRecord(); + unsigned index = Datatype::indexOf( n.getOperator().toExpr() ); + std::pair<std::string, Type> fld = rec[index]; + out << '.' << fld.first; + }else{ + toStream(op, n.getOperator(), depth, types, false); + } + } + break; case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; @@ -359,16 +421,6 @@ 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() << " := "; @@ -381,28 +433,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo 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; - const Record::FieldVector& fields = rec.getFields(); - for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.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: @@ -1106,8 +1136,9 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() { if(c->getArity() > 0) { + //TODO? out << "ERROR: Don't know how to print parameterized type declaration " - "in CVC language:" << endl << c->toString() << endl; + "in CVC language." << endl; } else { out << c->getSymbol() << " : TYPE;"; } @@ -1229,7 +1260,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, boo } firstSelector = false; const DatatypeConstructorArg& selector = *k; - out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType(); + Type t = SelectorType(selector.getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype & sdt = ((DatatypeType)t).getDatatype(); + out << selector.getName() << ": " << sdt.getName(); + }else{ + out << selector.getName() << ": " << t; + } } out << ')'; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ece4e9177..657d288e7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -333,7 +333,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::EQUAL: case kind::DISTINCT: out << smtKindString(k) << " "; break; case kind::CHAIN: break; - case kind::TUPLE: break; case kind::FUNCTION_TYPE: for(size_t i = 0; i < n.getNumChildren() - 1; ++i) { if(i > 0) { @@ -694,7 +693,6 @@ static string smtKindString(Kind k) throw() { case kind::EQUAL: return "="; case kind::DISTINCT: return "distinct"; case kind::CHAIN: break; - case kind::TUPLE: break; case kind::SEXPR: break; // bool theory diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 4372c0c18..07d78a6fd 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -139,14 +139,15 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, processing[in_t] = true; if(in.getType().isRecord()) { Assert(as.isRecord()); - const Record& inRec = in.getType().getConst<Record>(); - const Record& asRec = as.getConst<Record>(); + const Record& inRec = in.getType().getRecord(); + const Record& asRec = as.getRecord(); Assert(inRec.getNumFields() == asRec.getNumFields()); - NodeBuilder<> nb(kind::RECORD); + const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype(); + NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR); nb << NodeManager::currentNM()->mkConst(asRec); for(size_t i = 0; i < asRec.getNumFields(); ++i) { Assert(inRec[i].first == asRec[i].first); - Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in); + Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in); if(inRec[i].second != asRec[i].second) { arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing); } @@ -156,21 +157,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, processing.erase( in_t ); return out; } - if(in.getType().isTuple()) { - Assert(as.isTuple()); - Assert(in.getType().getNumChildren() == as.getNumChildren()); - NodeBuilder<> nb(kind::TUPLE); - for(size_t i = 0; i < as.getNumChildren(); ++i) { - Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in); - if(in.getType()[i] != as[i]) { - arg = rewriteAs(arg, as[i], processing); - } - nb << arg; - } - Node out = nb; - processing.erase( in_t ); - return out; - } if(in.getType().isDatatype()) { if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { processing.erase( in_t ); @@ -387,25 +373,6 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl; return out; } - if(type.isRecord()) { - const Record& rec = type.getConst<Record>(); - const Record::FieldVector& fields = rec.getFields(); - vector< pair<string, Type> > flds; - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - TypeNode converted = convertType(TypeNode::fromType((*i).second), true); - if(TypeNode::fromType((*i).second) != converted) { - flds.push_back(make_pair((*i).first, converted.toType())); - } else { - flds.push_back(*i); - } - } - TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds)); - Debug("tuprec") << "converted " << type << " to " << newRec << endl; - if(newRec != type) { - outNode = newRec;// cache it - } - return newRec; - } if(!type.isSort() && type.getNumChildren() > 0) { Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl; // This should handle tuples and arrays ok. @@ -460,7 +427,9 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa stack< triple<TNode, theory::TheoryId, bool> > worklist; worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false)); stack< NodeBuilder<> > result; - result.push(NodeBuilder<>(kind::TUPLE)); + //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND". + //result.push(NodeBuilder<>(kind::TUPLE)); + result.push(NodeBuilder<>(kind::AND)); NodeManager* nm = NodeManager::currentNM(); @@ -670,26 +639,6 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa result.top() << top; worklist.pop(); goto next_worklist; - } else if(t.isTuple() || t.isRecord()) { - TypeNode newType = convertType(t, true); - if(t != newType) { - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "a tuple/record variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - n.setAttribute(BooleanTermAttr(), top); - Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; } else if(t.isDatatype() || t.isParametricDatatype()) { Debug("boolean-terms") << "found a var of datatype type" << endl; TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES); @@ -857,17 +806,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Debug("bt") << "looking at: " << top << endl; // rewrite the operator, as necessary if(mk == kind::metakind::PARAMETERIZED) { - if(k == kind::RECORD) { - result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES); - } else if(k == kind::APPLY_TYPE_ASCRIPTION) { + if(k == kind::APPLY_TYPE_ASCRIPTION) { Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType())); result.top() << asc; Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl; asc.setAttribute(BooleanTermAttr(), top.getOperator()); } else if(kindToTheoryId(k) != THEORY_BV && - k != kind::TUPLE_SELECT && k != kind::TUPLE_UPDATE && - k != kind::RECORD_SELECT && k != kind::RECORD_UPDATE && k != kind::DIVISIBLE && // Theory parametric functions go here @@ -899,7 +844,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa } else { Node n = result.top(); result.pop(); - Debug("boolean-terms") << "constructed: " << n << endl; + Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl; if(parentTheory == theory::THEORY_BOOL) { if(n.getType().isBitVector() && n.getType().getBitVectorSize() == 1) { diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 0ba668b33..aa645954b 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -71,21 +71,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor()); } } - if(n.getType().isRecord() && asType.isRecord()) { - Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl; - const Record& rec CVC4_UNUSED = n.getType().getConst<Record>(); - const Record& asRec = asType.getConst<Record>(); - Assert(rec.getNumFields() == asRec.getNumFields()); - Assert(n.getNumChildren() == asRec.getNumFields()); - NodeBuilder<> b(n.getKind()); - b << asType; - for(size_t i = 0; i < n.getNumChildren(); ++i) { - b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second)); - } - Node out = b; - Debug("boolean-terms") << "+++ returning record " << out << endl; - return out; - } Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; if(n.getType().isArray()) { Assert(asType.isArray()); @@ -157,80 +142,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { Debug("tuprec") << "visiting " << current << endl; Assert(!alreadyVisited(current, TNode::null())); bool rewriteChildren = false; - if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { - if(current.getKind() == kind::APPLY_CONSTRUCTOR){ - TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr()); - NodeBuilder<> b(kind::TUPLE); - TypeNode::iterator t = expectType.begin(); - for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { - Assert(alreadyVisited(*i, TNode::null())); - Assert(t != expectType.end()); - TNode n = d_nodes[*i]; - n = n.isNull() ? *i : n; - if(!n.getType().isSubtypeOf(*t)) { - Assert(n.getType().isBitVector(1u) || - (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); - Assert(n.isConst()); - Assert((*t).isBoolean()); - if(n.getType().isBitVector(1u)) { - b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); - } else { - // we assume (by construction) false is first; see boolean_terms.cpp - b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); - } - } else { - b << n; - } - } - Assert(t == expectType.end()); - d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl; - // The assert below is too strong---we might be returning a model value but - // expect a type that still uses datatypes for tuples/records. If it's - // really not the right type we should catch it in SmtEngine anyway. - // Assert(d_nodes[current].getType() == expectType); - return; - }else{ - rewriteChildren = true; - } - } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { - if(current.getKind() == kind::APPLY_CONSTRUCTOR){ - //Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); - TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr()); - const Record& expectRec = expectType.getConst<Record>(); - NodeBuilder<> b(kind::RECORD); - b << current.getType().getAttribute(expr::DatatypeRecordAttr()); - const Record::FieldVector& fields = expectRec.getFields(); - Record::FieldVector::const_iterator t = fields.begin(); - for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { - Assert(alreadyVisited(*i, TNode::null())); - Assert(t != fields.end()); - TNode n = d_nodes[*i]; - n = n.isNull() ? *i : n; - if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) { - Assert(n.getType().isBitVector(1u) || - (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); - Assert(n.isConst()); - Assert((*t).second.isBoolean()); - if(n.getType().isBitVector(1u)) { - b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); - } else { - // we assume (by construction) false is first; see boolean_terms.cpp - b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); - } - } else { - b << n; - } - } - Assert(t == fields.end()); - d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl; - Assert(d_nodes[current].getType() == expectType); - return; - }else{ - rewriteChildren = true; - } - } else if(current.getKind() == kind::APPLY_CONSTRUCTOR && + if(current.getKind() == kind::APPLY_CONSTRUCTOR && ( current.getOperator().hasAttribute(BooleanTermAttr()) || ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index deb9770c0..007c5e049 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2587,6 +2587,9 @@ bool SmtEnginePrivate::nonClausalSimplify() { TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl; + } if(d_propagatorNeedsFinish) { d_propagator.finish(); @@ -2622,6 +2625,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { return false; } + + Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl; // No conflict, go through the literals and solve them SubstitutionMap constantPropagations(d_smt.d_context); SubstitutionMap newSubstitutions(d_smt.d_context); @@ -2632,10 +2637,12 @@ bool SmtEnginePrivate::nonClausalSimplify() { Node learnedLiteral = d_nonClausalLearnedLiterals[i]; Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral); Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral); + Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl; Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral); if (learnedLiteral != learnedLiteralNew) { learnedLiteral = Rewriter::rewrite(learnedLiteralNew); } + Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl; for (;;) { learnedLiteralNew = constantPropagations.apply(learnedLiteral); if (learnedLiteralNew == learnedLiteral) { @@ -2644,6 +2651,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { ++d_smt.d_stats->d_numConstantProps; learnedLiteral = Rewriter::rewrite(learnedLiteralNew); } + Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl; // It might just simplify to a constant if (learnedLiteral.isConst()) { if (learnedLiteral.getConst<bool>()) { @@ -2763,6 +2771,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { #endif /* CVC4_ASSERTIONS */ } // Resize the learnt + Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; d_nonClausalLearnedLiterals.resize(j); hash_set<TNode, TNodeHashFunction> s; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 1e7e714cf..0c00ed8df 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -100,43 +100,6 @@ 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_TOTAL && - (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_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, @@ -236,45 +199,6 @@ public: return RewriteResponse(REWRITE_AGAIN_FULL, res ); } } - 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.getOperator().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, @@ -306,10 +230,7 @@ public: static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl; - 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) ) { - //n1.getKind()==kind::APPLY_CONSTRUCTOR + if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { if( n1.getOperator() != n2.getOperator() ) { Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; return true; @@ -459,12 +380,10 @@ public: /** is this term a datatype */ static bool isTermDatatype( TNode n ){ TypeNode tn = n.getType(); - return tn.isDatatype() || tn.isParametricDatatype() || - tn.isTuple() || tn.isRecord(); + return tn.isDatatype() || tn.isParametricDatatype(); } static bool isTypeDatatype( TypeNode tn ){ - return tn.isDatatype() || tn.isParametricDatatype() || - tn.isTuple() || tn.isRecord(); + return tn.isDatatype() || tn.isParametricDatatype(); } private: static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending, diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 749d6b58a..c31a462bd 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -91,30 +91,6 @@ typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule # mu applications are constant expressions construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule -operator TUPLE_TYPE 0: "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 0: "a tuple (N-ary)" -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; payload is an instance of the CVC4::TupleSelect class" -parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple" -typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule - constant TUPLE_UPDATE_OP \ ::CVC4::TupleUpdate \ ::CVC4::TupleUpdateHashFunction \ @@ -129,33 +105,21 @@ constant RECORD_TYPE \ "expr/record.h" \ "record type" cardinality RECORD_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \ "theory/datatypes/theory_datatypes_type_rules.h" well-founded RECORD_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::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 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order" -typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule -construle RECORD ::CVC4::theory::datatypes::RecordProperties - -constant RECORD_SELECT_OP \ - ::CVC4::RecordSelect \ - ::CVC4::RecordSelectHashFunction \ - "expr/record.h" \ - "operator for a record select; payload is an instance CVC4::RecordSelect class" -parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from" -typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule - constant RECORD_UPDATE_OP \ ::CVC4::RecordUpdate \ ::CVC4::RecordUpdateHashFunction \ "expr/record.h" \ - "operator for a record update; payload is an instance CVC4::RecordSelect class" + "operator for a record update; payload is an instance CVC4::RecordUpdate class" parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c8d7338a7..ad2b1a297 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -147,12 +147,8 @@ void TheoryDatatypes::check(Effort e) { // 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 ), + ( atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE && + atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE), "tuple/record escaped into datatypes decision procedure; should have been rewritten away" ); //assert the fact @@ -550,86 +546,21 @@ void TheoryDatatypes::presolve() { 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_TOTAL, 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_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); - } - TypeNode t = in.getType(); - // 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) { - if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { - Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; - Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl; - if(t.isTuple()) { - Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl; - Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl; - NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr())); - } else { - Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl; - Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl; - NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); - } - } - - if( in.getKind()==EQUAL ){ - Node nn; - std::vector< Node > rew; - if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ - nn = NodeManager::currentNM()->mkConst(false); - }else{ - nn = rew.size()==0 ? d_true : - ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); - } - return nn; - } - - // nothing to do - return in; - } - - 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) { + if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) { + Assert( t.isDatatype() ); + const Datatype& dt = DatatypeType(t.toType()).getDatatype(); NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); b << Node::fromExpr(dt[0].getConstructor()); size_t size, updateIndex; if(in.getKind() == kind::TUPLE_UPDATE) { - size = t.getNumChildren(); + Assert( t.isTuple() ); + size = t.getTupleLength(); updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex(); } else { // kind::RECORD_UPDATE - const Record& record = t.getConst<Record>(); + Assert( t.isRecord() ); + const Record& record = t.getRecord(); size = record.getNumFields(); updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField()); } @@ -647,15 +578,39 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } } Debug("tuprec") << "builder says " << b << std::endl; - n = b; + Node n = b; + return n; } - Assert(!n.isNull()); + if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { + Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; + Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl; + if(t.isTuple()) { + Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl; + Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl; + t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr())); + } else { + Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl; + Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl; + t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr())); + } + } + if( in.getKind()==EQUAL ){ + Node nn; + std::vector< Node > rew; + if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ + nn = NodeManager::currentNM()->mkConst(false); + }else{ + nn = rew.size()==0 ? d_true : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + } + return nn; + } - Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; + // nothing to do + return in; - return n; } void TheoryDatatypes::addSharedTerm(TNode t) { @@ -2123,9 +2078,7 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { } bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) { - 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.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { if( n1.getOperator() != n2.getOperator() ) { return true; } else { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 8b723f43e..477ce6ba5 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -267,44 +267,6 @@ 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); - if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) { - throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); - } - const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); - TypeNode tupleType = n[0].getType(check); - if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { - 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); @@ -313,16 +275,14 @@ struct TupleUpdateTypeRule { TypeNode newValue = n[1].getType(check); if(check) { if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { - throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); - } + throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); } - if(tu.getIndex() >= tupleType.getNumChildren()) { + if(tu.getIndex() >= tupleType.getTupleLength()) { std::stringstream ss; ss << "Tuple-update expression index `" << tu.getIndex() << "' is not a valid index; tuple type only has " - << tupleType.getNumChildren() << " fields"; + << tupleType.getTupleLength() << " fields"; throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); } } @@ -330,138 +290,6 @@ struct TupleUpdateTypeRule { } };/* 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>(); - const Record::FieldVector& fields = rec.getFields(); - if(check) { - Record::FieldVector::const_iterator i = fields.begin(); - for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); - child_it != child_it_end; - ++child_it, ++i) { - if(i == fields.end()) { - throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); - } - if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) { - std::stringstream ss; - ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - if(i != fields.end()) { - throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); - } - } - return nodeManager->mkRecordType(rec); - } -};/* struct RecordTypeRule */ - -struct RecordSelectTypeRule { - inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){ - for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){ - if((*i).first == name) { - return i; - } - } - return fields.end(); - } - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::RECORD_SELECT); - NodeManagerScope nms(nodeManager); - if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) { - throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); - } - 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(); - const Record::FieldVector& fields = rec.getFields(); - Record::FieldVector::const_iterator field = record_find(fields, rs.getField()); - if(field == fields.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); @@ -471,10 +299,7 @@ struct RecordUpdateTypeRule { 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()); + throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); } const Record& rec = recordType.getRecord(); if(!rec.contains(ru.getField())) { @@ -491,33 +316,16 @@ struct RecordUpdateTypeRule { struct RecordProperties { inline static Node mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::RECORD_TYPE); - - const Record& rec = type.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - std::vector<Node> children; - for(Record::FieldVector::const_iterator i = fields.begin(), - i_end = fields.end(); - i != i_end; - ++i) { - children.push_back((*i).second.mkGroundTerm()); - } - - return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children); + return Node::null(); } - 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; + } + inline static Cardinality computeCardinality(TypeNode type) { + Cardinality card(1); + return card; + } + inline static bool isWellFounded(TypeNode type) { return true; } };/* struct RecordProperties */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 62446a937..77db1968a 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -221,3 +221,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ ++*this; //increment( d_ctor ); AlwaysAssert( !isFinished() ); } + diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 921ba403c..1f30498d6 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -177,90 +177,6 @@ public: };/* DatatypesEnumerator */ -class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { - TypeEnumeratorProperties * d_tep; - TypeEnumerator** d_enumerators; - - /** Allocate and initialize the delegate enumerators */ - void newEnumerators() { - d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep); - } - } - - 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, TypeEnumeratorProperties * tep = NULL) throw() : - TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) { - Assert(type.isTuple()); - newEnumerators(); - } - - TupleEnumerator(const TupleEnumerator& te) throw() : - TypeEnumeratorBase<TupleEnumerator>(te.getType()), - d_tep(te.d_tep), - d_enumerators(NULL) { - - if(te.d_enumerators != NULL) { - newEnumerators(); - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]); - } - } - } - - virtual ~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], d_tep); - } else { - ++*d_enumerators[i]; - return *this; - } - } - - deleteEnumerators(); - - return *this; - } - - bool isFinished() throw() { - return d_enumerators == NULL; - } - -};/* TupleEnumerator */ class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> { TypeEnumeratorProperties * d_tep; @@ -316,15 +232,8 @@ public: 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); + + return Node::null(); } RecordEnumerator& operator++() throw() { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index d024e0270..0eff9bd5d 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -784,9 +784,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) continue; } TypeNode t = TypeSet::getType(it); - if(t.isTuple() || t.isRecord()) { - t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); - } //get properties of this type bool isCorecursive = false; diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 040bd7161..17efaf2a5 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -123,7 +123,7 @@ public: void testMkAssociativeBadKind() { std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10); - TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(LEQ,vars), IllegalArgumentException); } }; |