diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
commit | 62b673a6b8444c14c169a984dd6e3fc8f685851e (patch) | |
tree | f0703edec34e3512dac340ce0059cba6368d7dd8 /src/theory | |
parent | 7acc2844df65ab6fdbf8166653c71eaa26d4d151 (diff) |
Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 87 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 42 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 123 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 216 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 1 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 95 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 3 |
7 files changed, 59 insertions, 508 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 1e7e714cf..0c00ed8df 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -100,43 +100,6 @@ public: } } } - if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { - return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); - } - if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { - const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); - return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]); - } - if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && - (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { - // These strange (half-tuple-converted) terms can be created by - // the system if you have something like "foo.1" for a tuple - // term foo. The select is rewritten to "select_1(foo)". If - // foo gets a value in the model from the TypeEnumerator, you - // then have a select of a tuple, and we should flatten that - // here. Ditto for records, below. - Expr selectorExpr = in.getOperator().toExpr(); - const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr); - TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType()); - size_t selectorIndex = Datatype::indexOf(selectorExpr); - Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl; -#ifdef CVC4_ASSERTIONS - // sanity checks: tuple- and record-converted datatypes should have one constructor - Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt); - if(in[0].getKind() == kind::TUPLE) { - Assert(dtt.hasAttribute(expr::DatatypeTupleAttr())); - Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType()); - } else { - Assert(dtt.hasAttribute(expr::DatatypeRecordAttr())); - Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType()); - } - Assert(dt.getNumConstructors() == 1); - Assert(dt[0].getNumArgs() > selectorIndex); - Assert(dt[0][selectorIndex].getSelector() == selectorExpr); -#endif /* CVC4_ASSERTIONS */ - Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; - return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); - } if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, @@ -236,45 +199,6 @@ public: return RewriteResponse(REWRITE_AGAIN_FULL, res ); } } - if(in.getKind() == kind::TUPLE_SELECT && - in[0].getKind() == kind::TUPLE) { - return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); - } - if(in.getKind() == kind::TUPLE_UPDATE && - in[0].getKind() == kind::TUPLE) { - size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex(); - NodeBuilder<> b(kind::TUPLE); - for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { - if(ix == 0) { - b << in[1]; - } else { - b << *i; - } - } - Node n = b; - Assert(n.getType().isSubtypeOf(in.getType())); - return RewriteResponse(REWRITE_DONE, n); - } - if(in.getKind() == kind::RECORD_SELECT && - in[0].getKind() == kind::RECORD) { - return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]); - } - if(in.getKind() == kind::RECORD_UPDATE && - in[0].getKind() == kind::RECORD) { - size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordUpdate>().getField()); - NodeBuilder<> b(kind::RECORD); - b << in[0].getOperator(); - for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { - if(ix == 0) { - b << in[1]; - } else { - b << *i; - } - } - Node n = b; - Assert(n.getType().isSubtypeOf(in.getType())); - return RewriteResponse(REWRITE_DONE, n); - } if(in.getKind() == kind::EQUAL && in[0] == in[1]) { return RewriteResponse(REWRITE_DONE, @@ -306,10 +230,7 @@ public: static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl; - if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || - (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || - (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { - //n1.getKind()==kind::APPLY_CONSTRUCTOR + if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { if( n1.getOperator() != n2.getOperator() ) { Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; return true; @@ -459,12 +380,10 @@ public: /** is this term a datatype */ static bool isTermDatatype( TNode n ){ TypeNode tn = n.getType(); - return tn.isDatatype() || tn.isParametricDatatype() || - tn.isTuple() || tn.isRecord(); + return tn.isDatatype() || tn.isParametricDatatype(); } static bool isTypeDatatype( TypeNode tn ){ - return tn.isDatatype() || tn.isParametricDatatype() || - tn.isTuple() || tn.isRecord(); + return tn.isDatatype() || tn.isParametricDatatype(); } private: static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending, diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 749d6b58a..c31a462bd 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -91,30 +91,6 @@ typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule # mu applications are constant expressions construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule -operator TUPLE_TYPE 0: "tuple type" -cardinality TUPLE_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ - "theory/datatypes/theory_datatypes_type_rules.h" -well-founded TUPLE_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \ - "theory/datatypes/theory_datatypes_type_rules.h" -enumerator TUPLE_TYPE \ - "::CVC4::theory::datatypes::TupleEnumerator" \ - "theory/datatypes/type_enumerator.h" - -operator TUPLE 0: "a tuple (N-ary)" -typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule -construle TUPLE ::CVC4::theory::datatypes::TupleProperties - -constant TUPLE_SELECT_OP \ - ::CVC4::TupleSelect \ - ::CVC4::TupleSelectHashFunction \ - "util/tuple.h" \ - "operator for a tuple select; payload is an instance of the CVC4::TupleSelect class" -parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple" -typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule - constant TUPLE_UPDATE_OP \ ::CVC4::TupleUpdate \ ::CVC4::TupleUpdateHashFunction \ @@ -129,33 +105,21 @@ constant RECORD_TYPE \ "expr/record.h" \ "record type" cardinality RECORD_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \ "theory/datatypes/theory_datatypes_type_rules.h" well-founded RECORD_TYPE \ - "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::isWellFounded(%TYPE%)" \ "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \ "theory/datatypes/theory_datatypes_type_rules.h" enumerator RECORD_TYPE \ "::CVC4::theory::datatypes::RecordEnumerator" \ "theory/datatypes/type_enumerator.h" -parameterized RECORD RECORD_TYPE 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order" -typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule -construle RECORD ::CVC4::theory::datatypes::RecordProperties - -constant RECORD_SELECT_OP \ - ::CVC4::RecordSelect \ - ::CVC4::RecordSelectHashFunction \ - "expr/record.h" \ - "operator for a record select; payload is an instance CVC4::RecordSelect class" -parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from" -typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule - constant RECORD_UPDATE_OP \ ::CVC4::RecordUpdate \ ::CVC4::RecordUpdateHashFunction \ "expr/record.h" \ - "operator for a record update; payload is an instance CVC4::RecordSelect class" + "operator for a record update; payload is an instance CVC4::RecordUpdate class" parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c8d7338a7..ad2b1a297 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -147,12 +147,8 @@ void TheoryDatatypes::check(Effort e) { // extra debug check to make sure that the rewriter did its job correctly Assert( atom.getKind() != kind::EQUAL || - ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE && - atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD && - atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE && - atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE && - atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT && - atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ), + ( atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE && + atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE), "tuple/record escaped into datatypes decision procedure; should have been rewritten away" ); //assert the fact @@ -550,86 +546,21 @@ void TheoryDatatypes::presolve() { Node TheoryDatatypes::ppRewrite(TNode in) { Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; - if(in.getKind() == kind::TUPLE_SELECT) { - TypeNode t = in[0].getType(); - if(t.hasAttribute(expr::DatatypeTupleAttr())) { - t = t.getAttribute(expr::DatatypeTupleAttr()); - } - TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); - const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]); - } else if(in.getKind() == kind::RECORD_SELECT) { - TypeNode t = in[0].getType(); - if(t.hasAttribute(expr::DatatypeRecordAttr())) { - t = t.getAttribute(expr::DatatypeRecordAttr()); - } - TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); - const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); - } - TypeNode t = in.getType(); - // we only care about tuples and records here - if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE && - in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) { - if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { - Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; - Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl; - if(t.isTuple()) { - Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl; - Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl; - NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr())); - } else { - Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl; - Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl; - NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); - } - } - - if( in.getKind()==EQUAL ){ - Node nn; - std::vector< Node > rew; - if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ - nn = NodeManager::currentNM()->mkConst(false); - }else{ - nn = rew.size()==0 ? d_true : - ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); - } - return nn; - } - - // nothing to do - return in; - } - - if(t.hasAttribute(expr::DatatypeTupleAttr())) { - t = t.getAttribute(expr::DatatypeTupleAttr()); - } else if(t.hasAttribute(expr::DatatypeRecordAttr())) { - t = t.getAttribute(expr::DatatypeRecordAttr()); - } - - // if the type doesn't have an associated datatype, then make one for it - TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t; - - const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - - // now rewrite the expression - Node n; - if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) { - NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); - b << Node::fromExpr(dt[0].getConstructor()); - b.append(in.begin(), in.end()); - n = b; - } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) { + if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) { + Assert( t.isDatatype() ); + const Datatype& dt = DatatypeType(t.toType()).getDatatype(); NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); b << Node::fromExpr(dt[0].getConstructor()); size_t size, updateIndex; if(in.getKind() == kind::TUPLE_UPDATE) { - size = t.getNumChildren(); + Assert( t.isTuple() ); + size = t.getTupleLength(); updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex(); } else { // kind::RECORD_UPDATE - const Record& record = t.getConst<Record>(); + Assert( t.isRecord() ); + const Record& record = t.getRecord(); size = record.getNumFields(); updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField()); } @@ -647,15 +578,39 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } } Debug("tuprec") << "builder says " << b << std::endl; - n = b; + Node n = b; + return n; } - Assert(!n.isNull()); + if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { + Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; + Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl; + if(t.isTuple()) { + Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl; + Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl; + t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr())); + } else { + Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl; + Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl; + t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr())); + } + } + if( in.getKind()==EQUAL ){ + Node nn; + std::vector< Node > rew; + if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ + nn = NodeManager::currentNM()->mkConst(false); + }else{ + nn = rew.size()==0 ? d_true : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + } + return nn; + } - Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; + // nothing to do + return in; - return n; } void TheoryDatatypes::addSharedTerm(TNode t) { @@ -2123,9 +2078,7 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { } bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) { - if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || - (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || - (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { + if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { if( n1.getOperator() != n2.getOperator() ) { return true; } else { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 8b723f43e..477ce6ba5 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -267,44 +267,6 @@ struct ConstructorProperties { } };/* struct ConstructorProperties */ -struct TupleTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::TUPLE); - std::vector<TypeNode> types; - for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); - child_it != child_it_end; - ++child_it) { - types.push_back((*child_it).getType(check)); - } - return nodeManager->mkTupleType(types); - } -};/* struct TupleTypeRule */ - -struct TupleSelectTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::TUPLE_SELECT); - if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) { - throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); - } - const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); - TypeNode tupleType = n[0].getType(check); - if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { - throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple"); - } - tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); - } - if(ts.getIndex() >= tupleType.getNumChildren()) { - std::stringstream ss; - ss << "Tuple-select expression index `" << ts.getIndex() - << "' is not a valid index; tuple type only has " - << tupleType.getNumChildren() << " fields"; - throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); - } - return tupleType[ts.getIndex()]; - } -};/* struct TupleSelectTypeRule */ - struct TupleUpdateTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::TUPLE_UPDATE); @@ -313,16 +275,14 @@ struct TupleUpdateTypeRule { TypeNode newValue = n[1].getType(check); if(check) { if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { - throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); - } + throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); } - if(tu.getIndex() >= tupleType.getNumChildren()) { + if(tu.getIndex() >= tupleType.getTupleLength()) { std::stringstream ss; ss << "Tuple-update expression index `" << tu.getIndex() << "' is not a valid index; tuple type only has " - << tupleType.getNumChildren() << " fields"; + << tupleType.getTupleLength() << " fields"; throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); } } @@ -330,138 +290,6 @@ struct TupleUpdateTypeRule { } };/* struct TupleUpdateTypeRule */ -struct TupleProperties { - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - Cardinality card(1); - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - card *= (*i).getCardinality(); - } - - return card; - } - - inline static bool isWellFounded(TypeNode type) { - // Don't assert this; allow other theories to use this - // wellfoundedness computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - if(! (*i).isWellFounded()) { - return false; - } - } - - return true; - } - - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::TUPLE_TYPE); - - std::vector<Node> children; - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - children.push_back((*i).mkGroundTerm()); - } - - return NodeManager::currentNM()->mkNode(kind::TUPLE, children); - } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::TUPLE); - NodeManagerScope nms(nodeManager); - - for(TNode::iterator i = n.begin(), - i_end = n.end(); - i != i_end; - ++i) { - if(! (*i).isConst()) { - return false; - } - } - - return true; - } -};/* struct TupleProperties */ - -struct RecordTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::RECORD); - NodeManagerScope nms(nodeManager); - const Record& rec = n.getOperator().getConst<Record>(); - const Record::FieldVector& fields = rec.getFields(); - if(check) { - Record::FieldVector::const_iterator i = fields.begin(); - for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); - child_it != child_it_end; - ++child_it, ++i) { - if(i == fields.end()) { - throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); - } - if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) { - std::stringstream ss; - ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - if(i != fields.end()) { - throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); - } - } - return nodeManager->mkRecordType(rec); - } -};/* struct RecordTypeRule */ - -struct RecordSelectTypeRule { - inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){ - for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){ - if((*i).first == name) { - return i; - } - } - return fields.end(); - } - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::RECORD_SELECT); - NodeManagerScope nms(nodeManager); - if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) { - throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); - } - const RecordSelect& rs = n.getOperator().getConst<RecordSelect>(); - TypeNode recordType = n[0].getType(check); - if(!recordType.isRecord()) { - if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { - throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record"); - } - recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); - } - const Record& rec = recordType.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - Record::FieldVector::const_iterator field = record_find(fields, rs.getField()); - if(field == fields.end()) { - std::stringstream ss; - ss << "Record-select field `" << rs.getField() - << "' is not a valid field name for the record type"; - throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); - } - return TypeNode::fromType((*field).second); - } -};/* struct RecordSelectTypeRule */ - struct RecordUpdateTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::RECORD_UPDATE); @@ -471,10 +299,7 @@ struct RecordUpdateTypeRule { TypeNode newValue = n[1].getType(check); if(check) { if(!recordType.isRecord()) { - if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { - throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); - } - recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); + throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); } const Record& rec = recordType.getRecord(); if(!rec.contains(ru.getField())) { @@ -491,33 +316,16 @@ struct RecordUpdateTypeRule { struct RecordProperties { inline static Node mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::RECORD_TYPE); - - const Record& rec = type.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - std::vector<Node> children; - for(Record::FieldVector::const_iterator i = fields.begin(), - i_end = fields.end(); - i != i_end; - ++i) { - children.push_back((*i).second.mkGroundTerm()); - } - - return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children); + return Node::null(); } - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::RECORD); - NodeManagerScope nms(nodeManager); - - for(TNode::iterator i = n.begin(), - i_end = n.end(); - i != i_end; - ++i) { - if(! (*i).isConst()) { - return false; - } - } - + return true; + } + inline static Cardinality computeCardinality(TypeNode type) { + Cardinality card(1); + return card; + } + inline static bool isWellFounded(TypeNode type) { return true; } };/* struct RecordProperties */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 62446a937..77db1968a 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -221,3 +221,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ ++*this; //increment( d_ctor ); AlwaysAssert( !isFinished() ); } + diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 921ba403c..1f30498d6 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -177,90 +177,6 @@ public: };/* DatatypesEnumerator */ -class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { - TypeEnumeratorProperties * d_tep; - TypeEnumerator** d_enumerators; - - /** Allocate and initialize the delegate enumerators */ - void newEnumerators() { - d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep); - } - } - - void deleteEnumerators() throw() { - if(d_enumerators != NULL) { - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - delete d_enumerators[i]; - } - delete [] d_enumerators; - d_enumerators = NULL; - } - } - -public: - - TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : - TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) { - Assert(type.isTuple()); - newEnumerators(); - } - - TupleEnumerator(const TupleEnumerator& te) throw() : - TypeEnumeratorBase<TupleEnumerator>(te.getType()), - d_tep(te.d_tep), - d_enumerators(NULL) { - - if(te.d_enumerators != NULL) { - newEnumerators(); - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]); - } - } - } - - virtual ~TupleEnumerator() throw() { - deleteEnumerators(); - } - - Node operator*() throw(NoMoreValuesException) { - if(isFinished()) { - throw NoMoreValuesException(getType()); - } - - NodeBuilder<> nb(kind::TUPLE); - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - nb << **d_enumerators[i]; - } - return Node(nb); - } - - TupleEnumerator& operator++() throw() { - if(isFinished()) { - return *this; - } - - size_t i; - for(i = 0; i < getType().getNumChildren(); ++i) { - if(d_enumerators[i]->isFinished()) { - *d_enumerators[i] = TypeEnumerator(getType()[i], d_tep); - } else { - ++*d_enumerators[i]; - return *this; - } - } - - deleteEnumerators(); - - return *this; - } - - bool isFinished() throw() { - return d_enumerators == NULL; - } - -};/* TupleEnumerator */ class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> { TypeEnumeratorProperties * d_tep; @@ -316,15 +232,8 @@ public: throw NoMoreValuesException(getType()); } - NodeBuilder<> nb(kind::RECORD); - Debug("te") << "record enumerator: creating record of type " << getType() << std::endl; - nb << getType(); - const Record& rec = getType().getConst<Record>(); - for(size_t i = 0; i < rec.getNumFields(); ++i) { - Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl; - nb << **d_enumerators[i]; - } - return Node(nb); + + return Node::null(); } RecordEnumerator& operator++() throw() { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index d024e0270..0eff9bd5d 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -784,9 +784,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) continue; } TypeNode t = TypeSet::getType(it); - if(t.isTuple() || t.isRecord()) { - t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); - } //get properties of this type bool isCorecursive = false; |