From: Andrew Reynolds Date: Wed, 2 Dec 2020 22:59:11 +0000 (-0600) Subject: Remove Record object and convert to Node-level API (#5575) X-Git-Tag: cvc5-1.0.0~2516 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7bdcfeb862aaf8156dca4aaec71aef9cdda1e56;p=cvc5.git Remove Record object and convert to Node-level API (#5575) Required for detangling NodeManager from the Expr layer. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 748a1ce06..36edfdb46 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3650,7 +3650,7 @@ Sort Solver::mkRecordSort( { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector> f; + std::vector> f; size_t i = 0; for (const auto& p : fields) { @@ -3661,10 +3661,10 @@ Sort Solver::mkRecordSort( this == p.second.d_solver, "parameter sort", p.second, i) << "sort associated to this solver object"; i += 1; - f.emplace_back(p.first, p.second.d_type->toType()); + f.emplace_back(p.first, *p.second.d_type); } - return Sort(this, getNodeManager()->mkRecordType(Record(f))); + return Sort(this, getNodeManager()->mkRecordType(f)); CVC4_API_SOLVER_TRY_CATCH_END; } 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& 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 c = std::make_shared(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& 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& 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& 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 > 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& 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>; }/* CVC4 namespace */