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()) {
const Record& r = t.getRecord();
std::vector< std::pair<std::string, Type> > 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()) {
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);
#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 << ", ";
}
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<std::string, Type>& 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 */
#include <utility>
#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
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<std::string, Type> > 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<std::string, Type> > FieldVector;
- typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
- typedef const_iterator iterator;
-
- Record(const std::vector< std::pair<std::string, Type> >& fields) :
- d_fields(fields) {
- }
-
- 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<std::string, Type> operator[](size_t index) const {
- CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
- return d_fields[index];
- }
+ 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<std::string, Type>& 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;
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;
}
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).
}
// 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;
}
}
std::vector< std::pair<std::string, Type> > fields;
const Record& r1 = t1.getConst<Record>();
+ 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
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);
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);
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 << ", ";
}
}
if(type.isRecord()) {
const Record& rec = type.getConst<Record>();
+ const Record::FieldVector& fields = rec.getFields();
vector< pair<string, Type> > 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()));
**/
#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)) {
const Record& expectRec = expectType.getConst<Record>();
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))) {
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);
d_nodes[current] = Node::null();
}
}/* ModelPostprocessor::visit() */
+
+} /* namespace smt */
+} /* namespace CVC4 */
typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
+
struct DatatypeConstructorTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw(TypeCheckingExceptionPrivate, AssertionException) {
Assert(n.getKind() == kind::RECORD);
NodeManagerScope nms(nodeManager);
const Record& rec = n.getOperator().getConst<Record>();
+ 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))) {
throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
- if(i != rec.end()) {
+ if(i != fields.end()) {
throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
}
}
};/* 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);
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";
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";
Assert(type.getKind() == kind::RECORD_TYPE);
const Record& rec = type.getRecord();
+ const Record::FieldVector& fields = rec.getFields();
std::vector<Node> 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());
projects / cvc5.git / commitdiff