summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/node_manager.cpp18
-rw-r--r--src/expr/record.cpp97
-rw-r--r--src/expr/record.h37
3 files changed, 12 insertions, 140 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c70cfce3b..fde92c4e1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -736,13 +736,14 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto
}
TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
- if( index==rec.getNumFields() ){
+ if (index == rec.size())
+ {
if( d_data.isNull() ){
- const Record::FieldVector& fields = rec.getFields();
std::stringstream sst;
sst << "__cvc4_record";
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- sst << "_" << (*i).first << "_" << (*i).second;
+ for (const std::pair<std::string, TypeNode>& i : rec)
+ {
+ sst << "_" << i.first << "_" << i.second;
}
DType dt(sst.str());
dt.setRecord();
@@ -750,17 +751,18 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
ssc << sst.str() << "_ctor";
std::shared_ptr<DTypeConstructor> c =
std::make_shared<DTypeConstructor>(ssc.str());
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- c->addArg((*i).first, TypeNode::fromType((*i).second));
+ for (const std::pair<std::string, TypeNode>& i : rec)
+ {
+ c->addArg(i.first, i.second);
}
dt.addConstructor(c);
d_data = nm->mkDatatypeType(dt);
Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
}
return d_data;
- }else{
- return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 );
}
+ return d_children[rec[index].second][rec[index].first].getRecordType(
+ nm, rec, index + 1);
}
TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts)
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index f4004d2e7..08944912a 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -18,109 +18,12 @@
#include "base/check.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, const 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);
- PrettyCheckArgument(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;
- 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 << ", ";
- }
- os << (*i).first << ":" << (*i).second;
- first = false;
- }
- 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 RecordUpdate& t) {
return out << "[" << t.getField() << "]";
}
-
-const std::pair<std::string, Type>& Record::operator[](size_t index) const {
- PrettyCheckArgument(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 62ccd42db..a0d545a56 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -29,7 +29,7 @@
namespace CVC4 {
// This forward delcartion is required to resolve a cicular dependency with
// Record which is a referenced in a Kind file.
-class Type;
+class TypeNode;
} /* namespace CVC4 */
namespace CVC4 {
@@ -53,40 +53,7 @@ struct CVC4_PUBLIC RecordUpdateHashFunction {
std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
-// now an actual record definition
-class CVC4_PUBLIC Record {
- 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;
-
- Record(const FieldVector& fields);
- Record(const Record& other);
- ~Record();
- Record& operator=(const Record& r);
-
- bool contains(const std::string &name) const;
-
- size_t getIndex(std::string name) const;
- size_t getNumFields() const;
-
- 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 {
- size_t operator()(const Record& r) const;
-};/* struct RecordHashFunction */
-
-std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
+using Record = std::vector<std::pair<std::string, TypeNode>>;
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback