From: Tim King Date: Tue, 15 Dec 2015 22:35:34 +0000 (-0800) Subject: Breaking the include cycle between Record and Expr. X-Git-Tag: cvc5-1.0.0~6139 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f29ad74a705883181d9c934a0f772d4850b0b0e;p=cvc5.git Breaking the include cycle between Record and Expr. --- diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1b9bfcd10..17524a3c0 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -447,8 +447,8 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& 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, + //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()) { @@ -472,7 +472,8 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { const Record& r = t.getRecord(); std::vector< std::pair > v; bool changed = false; - for(Record::iterator i = r.begin(); i != r.end(); ++i) { + 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()) { @@ -503,9 +504,10 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { 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::const_iterator i = rec.begin(); i != rec.end(); ++i) { + for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { c.addArg((*i).first, (*i).second); } dt.addConstructor(c); diff --git a/src/expr/record.cpp b/src/expr/record.cpp index dfcba0d46..2dee03dbf 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -16,12 +16,74 @@ #include "expr/record.h" +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "expr/expr.h" +#include "expr/type.h" + + namespace CVC4 { +static Record::FieldVector::const_iterator 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(); +} + +Record::Record(const FieldVector& fields) + : d_fields(new FieldVector(fields)) +{ + Debug("record") << "making " << this << " " << d_fields << std::endl; +} + +Record::Record(const Record& other) + : d_fields(new FieldVector(other.getFields())) +{ + Debug("record") << "copy constructor " << this << " " << d_fields << std::endl; +} + +Record::~Record() { + Debug("record") << "deleting " << this << " " << d_fields << std::endl; + delete d_fields; +} + +Record& Record::operator=(const Record& r) { + Debug("record") << "setting " << this << " " << d_fields << std::endl; + Record::FieldVector& local = *d_fields; + local = r.getFields(); + return *this; +} + +const Record::FieldVector& Record::getFields() const { + return *d_fields; +} + +bool Record::contains(const std::string& name) const { + return find(*d_fields, name) != d_fields->end(); +} + + +size_t Record::getIndex(std::string name) const { + FieldVector::const_iterator i = find(*d_fields, name); + CheckArgument(i != d_fields->end(), name, + "requested field `%s' does not exist in record", name.c_str()); + return i - d_fields->begin(); +} + +size_t Record::getNumFields() const { + return d_fields->size(); +} + + std::ostream& operator<<(std::ostream& os, const Record& r) { os << "[# "; bool first = true; - for(Record::iterator i = r.begin(); i != r.end(); ++i) { + const Record::FieldVector& fields = r.getFields(); + for(Record::FieldVector::const_iterator i = fields.begin(), + i_end = fields.end(); i != i_end; ++i) { if(!first) { os << ", "; } @@ -33,4 +95,32 @@ std::ostream& operator<<(std::ostream& os, const Record& r) { return os; } +size_t RecordHashFunction::operator()(const Record& r) const { + size_t n = 0; + const Record::FieldVector& fields = r.getFields(); + for(Record::FieldVector::const_iterator i = fields.begin(), + i_end = fields.end(); i != i_end; ++i) { + n = (n << 3) ^ TypeHashFunction()((*i).second); + } + return n; +} + +std::ostream& operator<<(std::ostream& out, const RecordSelect& t) { + return out << "[" << t.getField() << "]"; +} + +std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { + return out << "[" << t.getField() << "]"; +} + + +const std::pair& Record::operator[](size_t index) const { + CheckArgument(index < d_fields->size(), index, "index out of bounds for record type"); + return (*d_fields)[index]; +} + +bool Record::operator==(const Record& r) const { + return (*d_fields) == *(r.d_fields); +} + }/* CVC4 namespace */ diff --git a/src/expr/record.h b/src/expr/record.h index a255649da..2cd7defe9 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -25,9 +25,14 @@ #include #include "util/hash.h" +// Forward Declarations namespace CVC4 { +// This forward delcartion is required to resolve a cicular dependency with +// Record which is a referenced in a Kind file. +class CVC4_PUBLIC Type; +} /* namespace CVC4 */ -class CVC4_PUBLIC Record; +namespace CVC4 { // operators for record select and update @@ -64,87 +69,37 @@ struct CVC4_PUBLIC RecordUpdateHashFunction { std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) { - return out << "[" << t.getField() << "]"; -} - -inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { - return out << "[" << t.getField() << "]"; -} - -}/* CVC4 namespace */ - -#warning "TODO: Address circular dependence in Record." -#include "expr/expr.h" -#include "expr/type.h" - -namespace CVC4 { - // now an actual record definition - class CVC4_PUBLIC Record { - std::vector< std::pair > d_fields; - public: + // Type must stay as incomplete types throughout this header! + // Everything containing a Type must be a pointer or a reference. + typedef std::vector< std::pair > FieldVector; - typedef std::vector< std::pair >::const_iterator const_iterator; - typedef const_iterator iterator; - - Record(const std::vector< std::pair >& fields) : - d_fields(fields) { - } - - const_iterator find(std::string name) const { - const_iterator i; - for(i = begin(); i != end(); ++i) { - if((*i).first == name) { - break; - } - } - return i; - } - - size_t getIndex(std::string name) const { - const_iterator i = find(name); - CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str()); - return i - begin(); - } - - size_t getNumFields() const { - return d_fields.size(); - } - - const_iterator begin() const { - return d_fields.begin(); - } + Record(const FieldVector& fields); + Record(const Record& other); + ~Record(); + Record& operator=(const Record& r); - const_iterator end() const { - return d_fields.end(); - } + bool contains(const std::string &name) const; - std::pair operator[](size_t index) const { - CheckArgument(index < d_fields.size(), index, "index out of bounds for record type"); - return d_fields[index]; - } + size_t getIndex(std::string name) const; + size_t getNumFields() const; - bool operator==(const Record& r) const { - return d_fields == r.d_fields; - } + const FieldVector& getFields() const; + const std::pair& operator[](size_t index) const; + bool operator==(const Record& r) const; bool operator!=(const Record& r) const { return !(*this == r); } +private: + FieldVector* d_fields; };/* class Record */ struct CVC4_PUBLIC RecordHashFunction { - inline size_t operator()(const Record& r) const { - size_t n = 0; - for(Record::iterator i = r.begin(); i != r.end(); ++i) { - n = (n << 3) ^ TypeHashFunction()((*i).second); - } - return n; - } + size_t operator()(const Record& r) const; };/* struct RecordHashFunction */ std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 869304c0a..659e80550 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -114,9 +114,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(r1.getNumFields() != r2.getNumFields()) { return false; } + const Record::FieldVector& fields1 = r1.getFields(); + const Record::FieldVector& fields2 = r2.getFields(); // r1's fields must be subtypes of r2's, in order // names must match also - for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) { return false; } @@ -125,7 +127,7 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { return true; } if(isFunction()) { - // A function is a subtype of another if the args are the same type, and + // A function is a subtype of another if the args are the same type, and // the return type is a subtype of the other's. This is enough for now // (and it's necessary for model generation, since a Real-valued function // might return a constant Int and thus the model value is typed differently). @@ -189,7 +191,9 @@ bool TypeNode::isComparableTo(TypeNode t) const { } // r1's fields must be comparable to r2's, in order // names must match also - for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + const Record::FieldVector& fields1 = r1.getFields(); + const Record::FieldVector& fields2 = r2.getFields(); + for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) { return false; } @@ -474,8 +478,10 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ } std::vector< std::pair > fields; const Record& r1 = t1.getConst(); + const Record::FieldVector& fields0 = r0.getFields(); + const Record::FieldVector& fields1 = r1.getFields(); // construct childwise leastCommonType, if one exists - for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) { + for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.end(); ++i, ++j) { TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); if((*i).first != (*j).first || kid.isNull()) { // if field names differ, or no common supertype, then diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 460b1ee03..ff3753a67 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1559,8 +1559,7 @@ recordStore[CVC4::Expr& f] PARSER_STATE->parseError(ss.str()); } const Record& rec = RecordType(t).getRecord(); - Record::const_iterator fld = rec.find(id); - if(fld == rec.end()) { + if(! rec.contains(id)) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f); @@ -1687,8 +1686,7 @@ postfixTerm[CVC4::Expr& f] PARSER_STATE->parseError("record-select applied to non-record"); } const Record& rec = RecordType(t).getRecord(); - Record::const_iterator fld = rec.find(id); - if(fld == rec.end()) { + if(!rec.contains(id)){ PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } f = MK_EXPR(MK_CONST(RecordSelect(id)), f); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index d33b97d66..db4558af6 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -390,7 +390,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << "(# "; TNode::iterator i = n.begin(); bool first = true; - for(Record::const_iterator j = rec.begin(); j != rec.end(); ++i, ++j) { + const Record::FieldVector& fields = rec.getFields(); + for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { if(!first) { out << ", "; } diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index f7dfdb410..4372c0c18 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -389,8 +389,9 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) } if(type.isRecord()) { const Record& rec = type.getConst(); + const Record::FieldVector& fields = rec.getFields(); vector< pair > flds; - for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) { + 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())); diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 485b2c9a9..f9e449be3 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -15,12 +15,15 @@ **/ #include "smt/model_postprocessor.h" -#include "smt/boolean_terms.h" + #include "expr/node_manager_attributes.h" +#include "expr/record.h" +#include "smt/boolean_terms.h" using namespace std; -using namespace CVC4; -using namespace CVC4::smt; + +namespace CVC4 { +namespace smt { Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { if(n.getType().isSubtypeOf(asType)) { @@ -191,10 +194,11 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { const Record& expectRec = expectType.getConst(); NodeBuilder<> b(kind::RECORD); b << current.getType().getAttribute(expr::DatatypeRecordAttr()); - Record::const_iterator t = expectRec.begin(); + 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 != expectRec.end()); + Assert(t != fields.end()); TNode n = d_nodes[*i]; n = n.isNull() ? *i : n; if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) { @@ -212,7 +216,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { b << n; } } - Assert(t == expectRec.end()); + 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); @@ -298,3 +302,6 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { d_nodes[current] = Node::null(); } }/* ModelPostprocessor::visit() */ + +} /* namespace smt */ +} /* namespace CVC4 */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 23e68a6a8..8b723f43e 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -35,6 +35,7 @@ namespace datatypes { typedef expr::Attribute GroundTermAttr; + struct DatatypeConstructorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate, AssertionException) { @@ -401,12 +402,13 @@ struct RecordTypeRule { Assert(n.getKind() == kind::RECORD); NodeManagerScope nms(nodeManager); const Record& rec = n.getOperator().getConst(); + const Record::FieldVector& fields = rec.getFields(); if(check) { - Record::iterator i = rec.begin(); + 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 == rec.end()) { + 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))) { @@ -415,7 +417,7 @@ struct RecordTypeRule { throw TypeCheckingExceptionPrivate(n, ss.str()); } } - if(i != rec.end()) { + if(i != fields.end()) { throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); } } @@ -424,6 +426,15 @@ struct RecordTypeRule { };/* 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); @@ -439,8 +450,9 @@ struct RecordSelectTypeRule { recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); } const Record& rec = recordType.getRecord(); - Record::const_iterator field = rec.find(rs.getField()); - if(field == rec.end()) { + 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"; @@ -465,8 +477,7 @@ struct RecordUpdateTypeRule { recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); } const Record& rec = recordType.getRecord(); - Record::const_iterator field = rec.find(ru.getField()); - if(field == rec.end()) { + if(!rec.contains(ru.getField())) { std::stringstream ss; ss << "Record-update field `" << ru.getField() << "' is not a valid field name for the record type"; @@ -482,9 +493,10 @@ struct RecordProperties { Assert(type.getKind() == kind::RECORD_TYPE); const Record& rec = type.getRecord(); + const Record::FieldVector& fields = rec.getFields(); std::vector children; - for(Record::iterator i = rec.begin(), - i_end = rec.end(); + for(Record::FieldVector::const_iterator i = fields.begin(), + i_end = fields.end(); i != i_end; ++i) { children.push_back((*i).second.mkGroundTerm());