diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:41:56 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:41:56 -0600 |
commit | 464e5839579ebe43eef8f6ab9a05766056ab0896 (patch) | |
tree | 49d99eecf671a7844259e6dd0cb8d425babbecd7 /src | |
parent | 51fbe09f8b16ad0a49b2add0801b2963de08427e (diff) | |
parent | f31163c1f6bb1816365e9f22505d9558a7bc1802 (diff) |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src')
32 files changed, 575 insertions, 1011 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index ed8478ee8..52174dce0 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 = ((CVC4::DatatypeType)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 < ((CVC4::DatatypeType)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..6b5bdf07c 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -358,27 +358,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 +467,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); @@ -640,6 +609,29 @@ DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const { return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes))); } +/** Get the length of a tuple type */ +size_t DatatypeType::getTupleLength() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getTupleLength(); +} + +/** Get the constituent types of a tuple type */ +std::vector<Type> DatatypeType::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& DatatypeType::getRecord() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getRecord(); +} + DatatypeType SelectorType::getDomain() const { return DatatypeType(makeType((*d_typeNode)[0])); } diff --git a/src/expr/type.h b/src/expr/type.h index 0f2118c44..67d259fec 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; @@ -459,39 +457,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 { @@ -704,6 +670,15 @@ public: /** Instantiate a datatype using this datatype constructor */ DatatypeType instantiate(const std::vector<Type>& params) 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; + };/* class DatatypeType */ /** 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 f3a2bbe02..3991da886 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1116,7 +1116,7 @@ type[CVC4::Type& t, : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { assert(t.isTuple()); - args = TupleType(t).getTypes(); + args = ((DatatypeType)t).getTupleTypes(); } else { args.push_back(t); } @@ -1554,13 +1554,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 = ((DatatypeType)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] @@ -1587,11 +1591,15 @@ recordStore[CVC4::Expr& f] << "its type: " << t; PARSER_STATE->parseError(ss.str()); } - const Record& rec = RecordType(t).getRecord(); + const Record& rec = ((DatatypeType)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] @@ -1718,24 +1726,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 = ((DatatypeType)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 = ((DatatypeType)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); } ) )* @@ -1956,20 +1972,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())); } @@ -2035,8 +2056,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 db4949c1f..58835d4e6 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: @@ -1122,8 +1152,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;"; } @@ -1245,7 +1276,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 7afbf4e40..d37f4ae99 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) { @@ -698,7 +697,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 f9e449be3..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()); @@ -156,71 +141,8 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { void ModelPostprocessor::visit(TNode current, TNode parent) { Debug("tuprec") << "visiting " << current << endl; Assert(!alreadyVisited(current, TNode::null())); - if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { - Assert(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); - } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { - 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); - } else if(current.getKind() == kind::APPLY_CONSTRUCTOR && + bool rewriteChildren = false; + if(current.getKind() == kind::APPLY_CONSTRUCTOR && ( current.getOperator().hasAttribute(BooleanTermAttr()) || ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { @@ -257,9 +179,13 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { Debug("boolean-terms") << "model-post: " << current << endl << "- returning " << n << endl; d_nodes[current] = n; + return; //all kinds with children that can occur in nodes in a model go here } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) { + rewriteChildren = true; + } + if( rewriteChildren ){ // rewrite based on children bool self = true; for(size_t i = 0; i < current.getNumChildren(); ++i) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 850b37fe0..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; @@ -3895,14 +3904,11 @@ void SmtEnginePrivate::processAssertions() { //apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node prev = d_assertions[i]; - Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; - vector< TypeNode > fvTypes; - vector< TNode > fvs; - d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs )); - if( prev!=d_assertions[i] ){ - d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] )); - Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; + Node next = quantifiers::QuantifiersRewriter::preprocess( prev ); + if( next!=prev ){ + d_assertions.replace(i, Rewriter::rewrite( next )); + Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; + Trace("quantifiers-preprocess") << " ...got " << d_assertions[i] << endl; } } } 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/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 00a5241f5..ff0da13e1 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No } } d_addedLemmas += addedLemmas; - Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl; - return true; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl; + return addedLemmas>0 || !riter.d_incomplete; }else{ Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; return false; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index fc1f052c3..bf91f74c6 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& }else if( n.getKind()==ITE ){ newHasPol = (child!=0) && hasPol; newPol = pol; + }else if( n.getKind()==FORALL ){ + newHasPol = (child==1) && hasPol; + newPol = pol; }else{ newHasPol = false; newPol = pol; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fc5b692b2..afe8cd598 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ - Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; Node x = n[0][0]; std::map< Node, Node >::iterator itp = pcons.find( x ); if( itp!=pcons.end() ){ @@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ return 0; } -bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { std::map< Node, bool >::iterator it = currCond.find( n ); if( it==currCond.end() ){ - Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl; + Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl; new_cond.push_back( n ); currCond[n] = pol; return true; }else{ - Assert( it->second==pol ); + if( it->second!=pol ){ + Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl; + conflict = true; + } return false; } } -void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ - setEntailedCond( n[i], pol, currCond, new_cond ); + setEntailedCond( n[i], pol, currCond, new_cond, conflict ); + if( conflict ){ + break; + } } }else if( n.getKind()==NOT ){ - setEntailedCond( n[0], !pol, currCond, new_cond ); + setEntailedCond( n[0], !pol, currCond, new_cond, conflict ); + return; }else if( n.getKind()==ITE ){ int pol = getEntailedCond( n, currCond ); if( pol==1 ){ - setEntailedCond( n[1], pol, currCond, new_cond ); + setEntailedCond( n[1], pol, currCond, new_cond, conflict ); }else if( pol==-1 ){ - setEntailedCond( n[2], pol, currCond, new_cond ); + setEntailedCond( n[2], pol, currCond, new_cond, conflict ); } } - if( addEntailedCond( n, pol, currCond, new_cond ) ){ + if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){ if( n.getKind()==APPLY_TESTER ){ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); unsigned index = Datatype::indexOf(n.getOperator().toExpr()); @@ -543,14 +550,14 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ if( i!=index ){ Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); - addEntailedCond( t, false, currCond, new_cond ); + addEntailedCond( t, false, currCond, new_cond, conflict ); } } }else{ if( dt.getNumConstructors()==2 ){ int oindex = 1-index; Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] ); - addEntailedCond( t, true, currCond, new_cond ); + addEntailedCond( t, true, currCond, new_cond, conflict ); } } } @@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ) { + Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl; Node ret; std::map< Node, Node >::iterator iti = cache.find( body ); if( iti!=cache.end() ){ ret = iti->second; + Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl; }else{ - bool do_ite = false; - //only do context dependent processing up to ITE depth 8 - if( body.getKind()==ITE && nCurrCond<8 ){ - do_ite = true; - nCurrCond = nCurrCond + 1; - } + bool firstTimeCD = true; bool changed = false; std::vector< Node > children; for( size_t i=0; i<body.getNumChildren(); i++ ){ std::vector< Node > new_cond; - if( do_ite && i>0 ){ - setEntailedCond( children[0], i==1, currCond, new_cond ); - cache.clear(); + bool conflict = false; + //only do context dependent processing up to depth 8 + if( nCurrCond<8 ){ + if( firstTimeCD ){ + firstTimeCD = false; + nCurrCond = nCurrCond + 1; + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl; + } + } + if( body.getKind()==ITE && i>0 ){ + setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); + //should not conflict (entailment check failed) + Assert( !conflict ); + } + //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){ + // bool use_pol = !pol; + if( body.getKind()==OR || body.getKind()==AND ){ + bool use_pol = body.getKind()==AND; + for( unsigned j=0; j<body.getNumChildren(); j++ ){ + if( j<i ){ + setEntailedCond( children[j], use_pol, currCond, new_cond, conflict ); + }else if( j>i ){ + setEntailedCond( body[j], use_pol, currCond, new_cond, conflict ); + } + } + if( conflict ){ + Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; + ret = NodeManager::currentNM()->mkConst( !use_pol ); + } + } + if( !new_cond.empty() ){ + cache.clear(); + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl; + } + } } - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); - Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - if( body.getKind()==ITE ){ - if( i==0 ){ + if( !conflict ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); + Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + if( body.getKind()==ITE && i==0 ){ int res = getEntailedCond( nn, currCond ); + Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl; if( res==1 ){ ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; }else if( res==-1 ){ ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; - } - }else{ - if( !new_cond.empty() ){ - for( unsigned j=0; j<new_cond.size(); j++ ){ - currCond.erase( new_cond[j] ); - } - cache.clear(); } } + children.push_back( nn ); + changed = changed || nn!=body[i]; + } + if( !new_cond.empty() ){ + for( unsigned j=0; j<new_cond.size(); j++ ){ + currCond.erase( new_cond[j] ); + } + cache.clear(); + } + if( !ret.isNull() ){ + break; } - children.push_back( nn ); - changed = changed || nn!=body[i]; } - if( ret.isNull() && changed ){ - if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), body.getOperator() ); + if( ret.isNull() ){ + if( changed ){ + if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), body.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); + }else{ + ret = body; } - ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); - }else{ - ret = body; } + Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; cache[body] = ret; } @@ -1737,6 +1785,18 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } +Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + //apply pre-skolemization to existential quantifiers + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs ); + } + } + return n; +} Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, std::map< Node, std::vector< int > >& var_parent, int parentId ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 38c1bdd58..47997f9a7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -91,10 +91,12 @@ public: private: /** options */ static bool doOperation( Node f, bool isNested, int computeOption ); +private: + static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: static Node rewriteRewriteRule( Node r ); static bool containsQuantifiers(Node n); - static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); + static Node preprocess( Node n, bool isInst = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8bc9689bd..560f68810 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -976,6 +976,16 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes if( f.hasAttribute(InstLevelAttribute()) ){ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); } + + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; i<sk.size(); i++ ){ + Trace("quantifiers-sk") << sk[i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } + return ret; } @@ -1002,14 +1012,6 @@ Node TermDb::getSkolemizedBody( Node f ){ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); } } - if( Trace.isOn("quantifiers-sk") ){ - Trace("quantifiers-sk") << "Skolemize : "; - for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){ - Trace("quantifiers-sk") << d_skolem_constants[f][i] << " "; - } - Trace("quantifiers-sk") << "for " << std::endl; - Trace("quantifiers-sk") << " " << f << std::endl; - } } return d_skolem_body[ f ]; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 19d66165a..6fedc14f0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -695,6 +695,8 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } + body = quantifiers::QuantifiersRewriter::preprocess( body, true ); + Trace("inst-debug") << "...preprocess to " << body << std::endl; Trace("inst-assert") << "(assert " << body << ")" << std::endl; //make the lemma Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body ); 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/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 9fceedc96..3ed1c4d40 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -26,6 +26,7 @@ //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE +//#define LAZY_REL_EQC using namespace std; using namespace CVC4; @@ -406,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ), d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ), - d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ){ + d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){ d_cardinality_term = n; //if( d_type.isSort() ){ // TypeEnumerator te(tn); @@ -1070,11 +1071,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //add splitting lemma for cardinality constraint Assert( !d_cardinality_term.isNull() ); Node lem = getCardinalityLiteral( d_aloc_cardinality ); - Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl; lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); d_cardinality_lemma[ d_aloc_cardinality ] = lem; //add as lemma to output channel - out->lemma( lem ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl; + } //require phase out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); //add the appropriate lemma, propagate as decision @@ -1121,7 +1123,6 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ if (!s.isNull() ){ //add lemma to output channel Assert( s.getKind()==EQUAL ); - Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; Node ss = Rewriter::rewrite( s ); if( ss.getKind()!=EQUAL ){ Node b_t = NodeManager::currentNM()->mkConst( true ); @@ -1150,10 +1151,13 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; //Notice() << "*** Split on " << s << std::endl; //split on the equality s - out->split( ss ); - //tell the sat solver to explore the equals branch first - out->requirePhase( ss, true ); - ++( d_thss->d_statistics.d_split_lemmas ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + //tell the sat solver to explore the equals branch first + out->requirePhase( ss, true ); + ++( d_thss->d_statistics.d_split_lemmas ); + } return 1; }else{ return 0; @@ -1185,9 +1189,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() ); Node lem = NodeManager::currentNM()->mkNode( OR, eqs ); - Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; - ++( d_thss->d_statistics.d_clique_lemmas ); - out->lemma( lem ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; + ++( d_thss->d_statistics.d_clique_lemmas ); + } }else{ //found a clique Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; @@ -1303,9 +1308,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu //Assert( hasValue ); //Assert( value ); conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); - Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl; - out->lemma( conflictNode ); - ++( d_thss->d_statistics.d_clique_lemmas ); + if( doSendLemma( conflictNode ) ){ + Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl; + ++( d_thss->d_statistics.d_clique_lemmas ); + } } //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique. @@ -1364,10 +1370,9 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, } void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) { - - if( d_clique_trie[c].add( clique ) ){ - d_cliques[ c ].push_back( clique ); - } + //if( d_clique_trie[c].add( clique ) ){ + // d_cliques[ c ].push_back( clique ); + //} } @@ -1395,6 +1400,16 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() { } } +bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) { + if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){ + d_lemma_cache[lem] = true; + d_thss->getOutputChannel().lemma( lem ); + return true; + }else{ + return false; + } +} + void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ Debug( c ) << "-- Conflict Find:" << std::endl; Debug( c ) << "Number of reps = " << d_reps << std::endl; @@ -1568,10 +1583,19 @@ bool StrongSolverTheoryUF::hasEqc( Node a ) { } /** new node */ -void StrongSolverTheoryUF::newEqClass( Node n ){ - SortModel* c = getSortModel( n ); +void StrongSolverTheoryUF::newEqClass( Node a ){ + SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC //do nothing +#else + Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + c->newEqClass( a ); + if( options::ufssSymBreak() ){ + d_sym_break->newEqClass( a ); + } + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; +#endif } } @@ -1580,6 +1604,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ //TODO: ensure they are relevant SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC ensureEqc( c, a ); if( hasEqc( b ) ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; @@ -1589,6 +1614,11 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ //c->assignEqClass( b, a ); d_rel_eqc[b] = true; } +#else + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + c->merge( a, b ); + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; +#endif }else{ if( options::ufssDiseqPropagation() ){ d_deq_prop->merge(a, b); @@ -1600,8 +1630,10 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC ensureEqc( c, a ); ensureEqc( c, b ); +#endif Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); @@ -1617,7 +1649,9 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ /** assert a node */ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; +#ifdef LAZY_REL_EQC ensureEqcRec( n ); +#endif bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; if( lit.getKind()==CARDINALITY_CONSTRAINT ){ @@ -2042,6 +2076,7 @@ void StrongSolverTheoryUF::allocateCombinedCardinality() { d_com_card_literal[ d_aloc_com_card.get() ] = lem; lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); //add as lemma to output channel + Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl; getOutputChannel().lemma( lem ); //require phase getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true ); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 24d7f840f..db4c50423 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -244,6 +244,8 @@ public: std::vector< Node > d_fresh_aloc_reps; /** whether we are initialized */ context::CDO< bool > d_initialized; + /** cache for lemmas */ + NodeBoolMap d_lemma_cache; private: /** apply totality */ bool applyTotality( int cardinality ); @@ -251,6 +253,8 @@ public: Node getTotalityLemmaTerm( int cardinality, int i ); /** simple check cardinality */ void simpleCheckCardinality(); + private: + bool doSendLemma( Node lem ); public: SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ); virtual ~SortModel(){} |