From 99465e5ed6ee1415c060dc89cc666b562045cf20 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 13 Jul 2018 01:57:24 -0700 Subject: [PATCH] New C++ API: Implementation of datatype classes. (#2142) --- src/api/cvc4cpp.cpp | 251 +++++++++++++++++++++++++++++++++++++++++- src/expr/datatype.cpp | 11 ++ src/expr/datatype.h | 10 ++ 3 files changed, 270 insertions(+), 2 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ceed73d5b..958438751 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -769,7 +769,6 @@ bool Sort::isSortConstructor() const return d_type->isSortConstructor(); } -#if 0 Datatype Sort::getDatatype() const { // CHECK: is this a datatype sort? @@ -791,7 +790,6 @@ Sort Sort::instantiate(const std::vector& params) const Assert (d_type->isSortConstructor()); return static_cast(d_type.get())->instantiate(tparams); } -#endif std::string Sort::toString() const { @@ -1209,6 +1207,255 @@ std::ostream& operator<<(std::ostream& out, return out; } +/* DatatypeSelector --------------------------------------------------------- */ + +DatatypeSelector::DatatypeSelector() +{ + d_stor = nullptr; +} + +DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor) + : d_stor(new CVC4::DatatypeConstructorArg(stor)) +{ +} + +DatatypeSelector::~DatatypeSelector() +{ +} + +std::string DatatypeSelector::toString() const +{ + std::stringstream ss; + ss << *d_stor; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) +{ + out << stor.toString(); + return out; +} + +/* DatatypeConstructor ------------------------------------------------------ */ + +DatatypeConstructor::DatatypeConstructor() +{ + d_ctor = nullptr; +} + +DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor) +: d_ctor(new CVC4::DatatypeConstructor(ctor)) +{ +} + +DatatypeConstructor::~DatatypeConstructor() +{ +} + +DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const +{ + // CHECK: selector with name exists? + // CHECK: is resolved? + return (*d_ctor)[name]; +} + +DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const +{ + // CHECK: cons with name exists? + // CHECK: is resolved? + return (*d_ctor)[name]; +} + +Term DatatypeConstructor::getSelectorTerm(const std::string& name) const +{ + // CHECK: cons with name exists? + // CHECK: is resolved? + return d_ctor->getSelector(name); +} + +DatatypeConstructor::const_iterator DatatypeConstructor::begin() const +{ + return DatatypeConstructor::const_iterator(*d_ctor, true); +} + +DatatypeConstructor::const_iterator DatatypeConstructor::end() const +{ + return DatatypeConstructor::const_iterator(*d_ctor, false); +} + +DatatypeConstructor::const_iterator::const_iterator( + const CVC4::DatatypeConstructor& ctor, bool begin) +{ + d_int_stors = ctor.getArgs(); + const std::vector* sels = + static_cast*>( + d_int_stors); + for (const auto& s : *sels) + { + /* Can not use emplace_back here since constructor is private. */ + d_stors.push_back(DatatypeSelector(s)); + } + d_idx = begin ? 0 : sels->size(); +} + +DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: +operator=(const DatatypeConstructor::const_iterator& it) +{ + d_int_stors = it.d_int_stors; + d_stors = it.d_stors; + d_idx = it.d_idx; + return *this; +} + +const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const +{ + return d_stors[d_idx]; +} + +const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const +{ + return &d_stors[d_idx]; +} + +DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: +operator++() +{ + ++d_idx; + return *this; +} + +DatatypeConstructor::const_iterator DatatypeConstructor::const_iterator:: +operator++(int) +{ + DatatypeConstructor::const_iterator it(*this); + ++d_idx; + return it; +} + +bool DatatypeConstructor::const_iterator::operator==( + const DatatypeConstructor::const_iterator& other) const +{ + return d_int_stors == other.d_int_stors && d_idx == other.d_idx; +} + +bool DatatypeConstructor::const_iterator::operator!=( + const DatatypeConstructor::const_iterator& other) const +{ + return d_int_stors != other.d_int_stors || d_idx != other.d_idx; +} + +std::string DatatypeConstructor::toString() const +{ + std::stringstream ss; + ss << *d_ctor; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) +{ + out << ctor.toString(); + return out; +} + +/* Datatype ----------------------------------------------------------------- */ + +Datatype::Datatype(const CVC4::Datatype& dtype) +: d_dtype(new CVC4::Datatype(dtype)) +{ +} + +Datatype::~Datatype() +{ +} + +DatatypeConstructor Datatype::operator[](const std::string& name) const +{ + // CHECK: cons with name exists? + // CHECK: is resolved? + return (*d_dtype)[name]; +} + +DatatypeConstructor Datatype::getConstructor(const std::string& name) const +{ + // CHECK: cons with name exists? + // CHECK: is resolved? + return (*d_dtype)[name]; +} + +Term Datatype::getConstructorTerm(const std::string& name) const +{ + // CHECK: cons with name exists? + // CHECK: is resolved? + return d_dtype->getConstructor(name); +} + +Datatype::const_iterator Datatype::begin() const +{ + return Datatype::const_iterator(*d_dtype, true); +} + +Datatype::const_iterator Datatype::end() const +{ + return Datatype::const_iterator(*d_dtype, false); +} + +Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin) +{ + d_int_ctors = dtype.getConstructors(); + const std::vector* cons = + static_cast*>(d_int_ctors); + for (const auto& c : *cons) + { + /* Can not use emplace_back here since constructor is private. */ + d_ctors.push_back(DatatypeConstructor(c)); + } + d_idx = begin ? 0 : cons->size(); +} + +Datatype::const_iterator& Datatype::const_iterator::operator=( + const Datatype::const_iterator& it) +{ + d_int_ctors = it.d_int_ctors; + d_ctors = it.d_ctors; + d_idx = it.d_idx; + return *this; +} + +const DatatypeConstructor& Datatype::const_iterator::operator*() const +{ + return d_ctors[d_idx]; +} + +const DatatypeConstructor* Datatype::const_iterator::operator->() const +{ + return &d_ctors[d_idx]; +} + +Datatype::const_iterator& Datatype::const_iterator::operator++() +{ + ++d_idx; + return *this; +} + +Datatype::const_iterator Datatype::const_iterator::operator++(int) +{ + Datatype::const_iterator it(*this); + ++d_idx; + return it; +} + +bool Datatype::const_iterator::operator==( + const Datatype::const_iterator& other) const +{ + return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx; +} + +bool Datatype::const_iterator::operator!=( + const Datatype::const_iterator& other) const +{ + return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx; +} + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 9b33b314c..8747c530e 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -695,6 +695,11 @@ bool Datatype::involvesUninterpretedType() const{ return d_involvesUt; } +const std::vector* Datatype::getConstructors() const +{ + return &d_constructors; +} + void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::map& resolutions, const std::vector& placeholders, @@ -834,6 +839,12 @@ void DatatypeConstructor::setSygus(Expr op, d_sygus_pc = spc; } +const std::vector* DatatypeConstructor::getArgs() + const +{ + return &d_args; +} + void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // We don't want to introduce a new data member, because eventually // we're going to be a constant stuffed inside a node. So we stow diff --git a/src/expr/datatype.h b/src/expr/datatype.h index a56a4f993..c2cf80158 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -450,6 +450,11 @@ class CVC4_PUBLIC DatatypeConstructor { */ void setSygus(Expr op, std::shared_ptr spc); + /** + * Get the list of arguments to this constructor. + */ + const std::vector* getArgs() const; + private: /** the name of the constructor */ std::string d_name; @@ -938,6 +943,11 @@ public: */ bool involvesUninterpretedType() const; + /** + * Get the list of constructors. + */ + const std::vector* getConstructors() const; + private: /** name of this datatype */ std::string d_name; -- 2.30.2