From: Andrew Reynolds Date: Fri, 6 Dec 2019 07:22:01 +0000 (-0600) Subject: Introduce the Node-level Datatypes API (#3462) X-Git-Tag: cvc5-1.0.0~3793 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=46bae5d2a8b22867f917c6f644e46e29884049f9;p=cvc5.git Introduce the Node-level Datatypes API (#3462) This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype. Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 0c1044e74..f6b48048f 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -46,6 +46,12 @@ libcvc4_add_sources( variable_type_map.h datatype.h datatype.cpp + dtype.h + dtype.cpp + dtype_cons.h + dtype_cons.cpp + dtype_selector.h + dtype_selector.cpp record.cpp record.h sygus_datatype.cpp diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index d52023b4c..f3f4c10d3 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -21,6 +21,7 @@ #include "base/check.h" #include "expr/attribute.h" +#include "expr/dtype.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" #include "expr/node.h" @@ -54,6 +55,48 @@ typedef expr::Attribute DatatypeFin typedef expr::Attribute DatatypeUFiniteAttr; typedef expr::Attribute DatatypeUFiniteComputedAttr; +Datatype::Datatype(std::string name, bool isCo) + : d_internal(nullptr), // until the Node-level datatype API is activated + d_name(name), + d_params(), + d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), + d_record(NULL), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_involvesUt(false), + d_sygus_allow_const(false), + d_sygus_allow_all(false), + d_card(CardinalityUnknown()), + d_well_founded(0) +{ +} + +Datatype::Datatype(std::string name, + const std::vector& params, + bool isCo) + : d_internal(nullptr), // until the Node-level datatype API is activated + d_name(name), + d_params(params), + d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), + d_record(NULL), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_involvesUt(false), + d_sygus_allow_const(false), + d_sygus_allow_all(false), + d_card(CardinalityUnknown()), + d_well_founded(0) +{ +} + Datatype::~Datatype(){ delete d_record; } @@ -837,6 +880,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name) // we're going to be a constant stuffed inside a node. So we stow // the tester name away inside the constructor name until // resolution. + d_internal(nullptr), // until the Node-level datatype API is activated d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO" d_tester(), d_args(), @@ -853,6 +897,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name, // we're going to be a constant stuffed inside a node. So we stow // the tester name away inside the constructor name until // resolution. + d_internal(nullptr), // until the Node-level datatype API is activated d_name(name + '\0' + tester), d_tester(), d_args(), @@ -1233,10 +1278,12 @@ bool DatatypeConstructor::involvesUninterpretedType() const{ return false; } -DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) : - d_name(name), - d_selector(selector), - d_resolved(false) { +DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) + : d_internal(nullptr), // until the Node-level datatype API is activated + d_name(name), + d_selector(selector), + d_resolved(false) +{ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index b32001a89..c78fbc436 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -101,6 +101,8 @@ class CVC4_PUBLIC DatatypeResolutionException : public Exception { class CVC4_PUBLIC DatatypeSelfType { };/* class DatatypeSelfType */ +class DTypeSelector; + /** * An unresolved type (used in calls to * DatatypeConstructor::addArg()) to allow a Datatype to refer to @@ -159,6 +161,8 @@ class CVC4_PUBLIC DatatypeConstructorArg { void toStream(std::ostream& out) const; private: + /** The internal representation */ + std::shared_ptr d_internal; /** the name of this selector */ std::string d_name; /** the selector expression */ @@ -199,6 +203,8 @@ class CVC4_PUBLIC SygusPrintCallback Expr e) const = 0; }; +class DTypeConstructor; + /** * A constructor for a Datatype. */ @@ -454,6 +460,8 @@ class CVC4_PUBLIC DatatypeConstructor { void toStream(std::ostream& out) const; private: + /** The internal representation */ + std::shared_ptr d_internal; /** the name of the constructor */ std::string d_name; /** the constructor expression */ @@ -552,6 +560,8 @@ class CVC4_PUBLIC DatatypeConstructor { void computeSharedSelectors(Type domainType) const; };/* class DatatypeConstructor */ +class DType; + /** * The representation of an inductive datatype. * @@ -613,7 +623,8 @@ class CVC4_PUBLIC DatatypeConstructor { */ class CVC4_PUBLIC Datatype { friend class DatatypeConstructor; -public: + friend class NodeManager; // temporary, for access to d_internal + public: /** * Get the datatype of a constructor, selector, or tester operator. */ @@ -645,13 +656,15 @@ public: typedef DatatypeConstructorIterator const_iterator; /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name, bool isCo = false); + explicit Datatype(std::string name, bool isCo = false); /** * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, const std::vector& params, bool isCo = false); + Datatype(std::string name, + const std::vector& params, + bool isCo = false); ~Datatype(); @@ -963,6 +976,8 @@ public: void toStream(std::ostream& out) const; private: + /** The internal representation */ + std::shared_ptr d_internal; /** name of this datatype */ std::string d_name; /** the type parameters of this datatype (if this is a parametric datatype) @@ -1183,40 +1198,6 @@ inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : } inline std::string DatatypeUnresolvedType::getName() const { return d_name; } -inline Datatype::Datatype(std::string name, bool isCo) - : d_name(name), - d_params(), - d_isCo(isCo), - d_isTuple(false), - d_isRecord(false), - d_record(NULL), - d_constructors(), - d_resolved(false), - d_self(), - d_involvesExt(false), - d_involvesUt(false), - d_sygus_allow_const(false), - d_sygus_allow_all(false), - d_card(CardinalityUnknown()), - d_well_founded(0) {} - -inline Datatype::Datatype(std::string name, const std::vector& params, - bool isCo) - : d_name(name), - d_params(params), - d_isCo(isCo), - d_isTuple(false), - d_isRecord(false), - d_record(NULL), - d_constructors(), - d_resolved(false), - d_self(), - d_involvesExt(false), - d_involvesUt(false), - d_sygus_allow_const(false), - d_sygus_allow_all(false), - d_card(CardinalityUnknown()), - d_well_founded(0) {} inline std::string Datatype::getName() const { return d_name; } inline size_t Datatype::getNumConstructors() const diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp new file mode 100644 index 000000000..f16b193ce --- /dev/null +++ b/src/expr/dtype.cpp @@ -0,0 +1,739 @@ +/********************* */ +/*! \file dtype.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype definition + **/ +#include "expr/dtype.h" + +#include "expr/node_algorithm.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +DType::DType(std::string name, bool isCo) + : d_name(name), + d_params(), + d_isCo(isCo), + d_isTuple(false), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_involvesUt(false), + d_sygusAllowConst(false), + d_sygusAllowAll(false), + d_card(CardinalityUnknown()), + d_wellFounded(0) +{ +} + +DType::DType(std::string name, const std::vector& params, bool isCo) + : d_name(name), + d_params(params), + d_isCo(isCo), + d_isTuple(false), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_involvesUt(false), + d_sygusAllowConst(false), + d_sygusAllowAll(false), + d_card(CardinalityUnknown()), + d_wellFounded(0) +{ +} + +DType::~DType() {} + +std::string DType::getName() const { return d_name; } +size_t DType::getNumConstructors() const { return d_constructors.size(); } + +bool DType::isParametric() const { return d_params.size() > 0; } +size_t DType::getNumParameters() const { return d_params.size(); } +TypeNode DType::getParameter(size_t i) const +{ + Assert(isParametric()); + Assert(i < d_params.size()); + return d_params[i]; +} + +std::vector DType::getParameters() const +{ + Assert(isParametric()); + return d_params; +} + +bool DType::isCodatatype() const { return d_isCo; } + +bool DType::isSygus() const { return !d_sygusType.isNull(); } + +bool DType::isTuple() const { return d_isTuple; } + +bool DType::isResolved() const { return d_resolved; } + +const DType& DType::datatypeOf(Node item) +{ + TypeNode t = item.getType(); + switch (t.getKind()) + { + case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); + case SELECTOR_TYPE: + case TESTER_TYPE: return t[0].getDType(); + default: + Unhandled() << "arg must be a datatype constructor, selector, or tester"; + } +} + +size_t DType::indexOf(Node item) +{ + Assert(item.getType().isConstructor() || item.getType().isTester() + || item.getType().isSelector()); + return indexOfInternal(item); +} + +size_t DType::indexOfInternal(Node item) +{ + if (item.getKind() == APPLY_TYPE_ASCRIPTION) + { + return indexOf(item[0]); + } + Assert(item.hasAttribute(DTypeIndexAttr())); + return item.getAttribute(DTypeIndexAttr()); +} + +size_t DType::cindexOf(Node item) +{ + Assert(item.getType().isSelector()); + return cindexOfInternal(item); +} +size_t DType::cindexOfInternal(Node item) +{ + if (item.getKind() == APPLY_TYPE_ASCRIPTION) + { + return cindexOf(item[0]); + } + Assert(item.hasAttribute(DTypeConsIndexAttr())); + return item.getAttribute(DTypeConsIndexAttr()); +} + +bool DType::resolve(const std::map& resolutions, + const std::vector& placeholders, + const std::vector& replacements, + const std::vector& paramTypes, + const std::vector& paramReplacements) +{ + Trace("datatypes-init") << "DType::resolve: " << std::endl; + Assert(!d_resolved); + Assert(resolutions.find(d_name) != resolutions.end()); + Assert(placeholders.size() == replacements.size()); + Assert(paramTypes.size() == paramReplacements.size()); + Assert(getNumConstructors() > 0); + TypeNode self = (*resolutions.find(d_name)).second; + Assert(&self.getDType() == this); + d_resolved = true; + size_t index = 0; + for (std::shared_ptr ctor : d_constructors) + { + Trace("datatypes-init") << "DType::resolve ctor " << std::endl; + if (!ctor->resolve(self, + resolutions, + placeholders, + replacements, + paramTypes, + paramReplacements, + index)) + { + return false; + } + ctor->d_constructor.setAttribute(DTypeIndexAttr(), index); + ctor->d_tester.setAttribute(DTypeIndexAttr(), index++); + Assert(ctor->isResolved()); + Trace("datatypes-init") << "DType::resolve ctor finished" << std::endl; + } + d_self = self; + + d_involvesExt = false; + d_involvesUt = false; + for (const std::shared_ptr ctor : d_constructors) + { + if (ctor->involvesExternalType()) + { + d_involvesExt = true; + } + if (ctor->involvesUninterpretedType()) + { + d_involvesUt = true; + } + } + + if (isSygus()) + { + // all datatype constructors should be sygus and have sygus operators whose + // free variables are subsets of sygus bound var list. + std::unordered_set svs; + for (const Node& sv : d_sygusBvl) + { + svs.insert(sv); + } + for (size_t i = 0, ncons = d_constructors.size(); i < ncons; i++) + { + Node sop = d_constructors[i]->getSygusOp(); + Assert(!sop.isNull()) + << "Sygus datatype contains a non-sygus constructor"; + std::unordered_set fvs; + expr::getFreeVariables(sop, fvs); + for (const Node& v : fvs) + { + if (svs.find(v) == svs.end()) + { + // return false, indicating we should abort, since this datatype is + // not well formed. + return false; + } + } + } + } + Trace("datatypes-init") << "DType::resolve: finished" << std::endl; + return true; +} + +void DType::addConstructor(std::shared_ptr c) +{ + Assert(!d_resolved); + d_constructors.push_back(c); +} + +void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) +{ + Assert(!d_resolved); + d_sygusType = st; + d_sygusBvl = bvl; + d_sygusAllowConst = allowConst || allowAll; + d_sygusAllowAll = allowAll; +} + +void DType::setTuple() +{ + Assert(!d_resolved); + d_isTuple = true; +} + +Cardinality DType::getCardinality(TypeNode t) const +{ + Trace("datatypes-init") << "DType::getCardinality " << std::endl; + Assert(isResolved()); + Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); + std::vector processing; + computeCardinality(t, processing); + return d_card; +} + +Cardinality DType::getCardinality() const +{ + Assert(!isParametric()); + return getCardinality(d_self); +} + +Cardinality DType::computeCardinality(TypeNode t, + std::vector& processing) const +{ + Trace("datatypes-init") << "DType::computeCardinality " << std::endl; + Assert(isResolved()); + if (std::find(processing.begin(), processing.end(), d_self) + != processing.end()) + { + d_card = Cardinality::INTEGERS; + return d_card; + } + processing.push_back(d_self); + Cardinality c = 0; + for (std::shared_ptr ctor : d_constructors) + { + c += ctor->computeCardinality(t, processing); + } + d_card = c; + processing.pop_back(); + return d_card; +} + +bool DType::isRecursiveSingleton(TypeNode t) const +{ + Trace("datatypes-init") << "DType::isRecursiveSingleton " << std::endl; + Assert(isResolved()); + Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); + if (d_cardRecSingleton.find(t) != d_cardRecSingleton.end()) + { + return d_cardRecSingleton[t] == 1; + } + if (isCodatatype()) + { + Assert(d_cardUAssume[t].empty()); + std::vector processing; + if (computeCardinalityRecSingleton(t, processing, d_cardUAssume[t])) + { + d_cardRecSingleton[t] = 1; + if (Trace.isOn("dt-card")) + { + Trace("dt-card") << "DType " << getName() + << " is recursive singleton, dependent upon " + << d_cardUAssume[t].size() + << " uninterpreted sorts: " << std::endl; + for (size_t i = 0; i < d_cardUAssume[t].size(); i++) + { + Trace("dt-card") << " " << d_cardUAssume[t][i] << std::endl; + } + Trace("dt-card") << std::endl; + } + } + else + { + d_cardRecSingleton[t] = -1; + } + } + else + { + d_cardRecSingleton[t] = -1; + } + return d_cardRecSingleton[t] == 1; +} + +bool DType::isRecursiveSingleton() const +{ + Assert(!isParametric()); + return isRecursiveSingleton(d_self); +} + +unsigned DType::getNumRecursiveSingletonArgTypes(TypeNode t) const +{ + Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end()); + Assert(isRecursiveSingleton(t)); + return d_cardUAssume[t].size(); +} + +unsigned DType::getNumRecursiveSingletonArgTypes() const +{ + Assert(!isParametric()); + return getNumRecursiveSingletonArgTypes(d_self); +} + +TypeNode DType::getRecursiveSingletonArgType(TypeNode t, size_t i) const +{ + Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end()); + Assert(isRecursiveSingleton(t)); + return d_cardUAssume[t][i]; +} + +TypeNode DType::getRecursiveSingletonArgType(size_t i) const +{ + Assert(!isParametric()); + return getRecursiveSingletonArgType(d_self, i); +} + +bool DType::computeCardinalityRecSingleton( + TypeNode t, + std::vector& processing, + std::vector& u_assume) const +{ + Trace("datatypes-init") << "DType::computeCardinalityRecSingleton " + << std::endl; + if (std::find(processing.begin(), processing.end(), d_self) + != processing.end()) + { + return true; + } + if (d_cardRecSingleton[t] == 0) + { + // if not yet computed + if (d_constructors.size() != 1) + { + return false; + } + bool success = false; + processing.push_back(d_self); + for (size_t i = 0, nargs = d_constructors[0]->getNumArgs(); i < nargs; i++) + { + TypeNode tc = d_constructors[0]->getArgType(i); + // if it is an uninterpreted sort, then we depend on it having cardinality + // one + if (tc.isSort()) + { + if (std::find(u_assume.begin(), u_assume.end(), tc) == u_assume.end()) + { + u_assume.push_back(tc); + } + // if it is a datatype, recurse + } + else if (tc.isDatatype()) + { + const DType& dt = tc.getDType(); + if (!dt.computeCardinalityRecSingleton(t, processing, u_assume)) + { + return false; + } + else + { + success = true; + } + // if it is a builtin type, it must have cardinality one + } + else if (!tc.getCardinality().isOne()) + { + return false; + } + } + processing.pop_back(); + return success; + } + else if (d_cardRecSingleton[t] == -1) + { + return false; + } + for (size_t i = 0, csize = d_cardUAssume[t].size(); i < csize; i++) + { + if (std::find(u_assume.begin(), u_assume.end(), d_cardUAssume[t][i]) + == u_assume.end()) + { + u_assume.push_back(d_cardUAssume[t][i]); + } + } + return true; +} + +bool DType::isFinite(TypeNode t) const +{ + Trace("datatypes-init") << "DType::isFinite " << std::endl; + Assert(isResolved()); + Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); + + // is this already in the cache ? + if (d_self.getAttribute(DTypeFiniteComputedAttr())) + { + return d_self.getAttribute(DTypeFiniteAttr()); + } + for (std::shared_ptr ctor : d_constructors) + { + if (!ctor->isFinite(t)) + { + d_self.setAttribute(DTypeFiniteComputedAttr(), true); + d_self.setAttribute(DTypeFiniteAttr(), false); + return false; + } + } + d_self.setAttribute(DTypeFiniteComputedAttr(), true); + d_self.setAttribute(DTypeFiniteAttr(), true); + return true; +} +bool DType::isFinite() const +{ + Assert(isResolved() && !isParametric()); + return isFinite(d_self); +} + +bool DType::isInterpretedFinite(TypeNode t) const +{ + Trace("datatypes-init") << "DType::isInterpretedFinite " << std::endl; + Assert(isResolved()); + Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); + // is this already in the cache ? + if (d_self.getAttribute(DTypeUFiniteComputedAttr())) + { + return d_self.getAttribute(DTypeUFiniteAttr()); + } + // start by assuming it is not + d_self.setAttribute(DTypeUFiniteComputedAttr(), true); + d_self.setAttribute(DTypeUFiniteAttr(), false); + for (std::shared_ptr ctor : d_constructors) + { + if (!ctor->isInterpretedFinite(t)) + { + return false; + } + } + d_self.setAttribute(DTypeUFiniteComputedAttr(), true); + d_self.setAttribute(DTypeUFiniteAttr(), true); + return true; +} +bool DType::isInterpretedFinite() const +{ + Assert(isResolved() && !isParametric()); + return isInterpretedFinite(d_self); +} + +bool DType::isWellFounded() const +{ + Trace("datatypes-init") << "DType::isWellFounded " << std::endl; + Assert(isResolved()); + if (d_wellFounded == 0) + { + std::vector processing; + if (computeWellFounded(processing)) + { + d_wellFounded = 1; + } + else + { + d_wellFounded = -1; + } + } + return d_wellFounded == 1; +} + +bool DType::computeWellFounded(std::vector& processing) const +{ + Trace("datatypes-init") << "DType::computeWellFounded " << std::endl; + Assert(isResolved()); + if (std::find(processing.begin(), processing.end(), d_self) + != processing.end()) + { + return d_isCo; + } + processing.push_back(d_self); + for (std::shared_ptr ctor : d_constructors) + { + if (ctor->computeWellFounded(processing)) + { + processing.pop_back(); + return true; + } + else + { + Trace("dt-wf") << "Constructor " << ctor->getName() + << " is not well-founded." << std::endl; + } + } + processing.pop_back(); + Trace("dt-wf") << "DType " << getName() << " is not well-founded." + << std::endl; + return false; +} + +Node DType::mkGroundTerm(TypeNode t) const +{ + Assert(isResolved()); + return mkGroundTermInternal(t, false); +} + +Node DType::mkGroundValue(TypeNode t) const +{ + Assert(isResolved()); + return mkGroundTermInternal(t, true); +} + +Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const +{ + Trace("datatypes-init") << "DType::mkGroundTerm of type " << t + << ", isValue = " << isValue << std::endl; + // is this already in the cache ? + std::map& cache = isValue ? d_groundValue : d_groundTerm; + std::map::iterator it = cache.find(t); + if (it != cache.end()) + { + Trace("datatypes-init") + << "\nin cache: " << d_self << " => " << it->second << std::endl; + return it->second; + } + std::vector processing; + Node groundTerm = computeGroundTerm(t, processing, isValue); + if (!groundTerm.isNull()) + { + // we found a ground-term-constructing constructor! + cache[t] = groundTerm; + Trace("datatypes-init") + << "constructed: " << getName() << " => " << groundTerm << std::endl; + } + // if ground term is null, we are not well-founded + Trace("datatypes-init") << "DType::mkGroundTerm for " << t << " returns " + << groundTerm << std::endl; + return groundTerm; +} + +Node getSubtermWithType(Node e, TypeNode t, bool isTop) +{ + if (!isTop && e.getType() == t) + { + return e; + } + for (const Node& ei : e) + { + Node se = getSubtermWithType(ei, t, false); + if (!se.isNull()) + { + return se; + } + } + return Node(); +} + +Node DType::computeGroundTerm(TypeNode t, + std::vector& processing, + bool isValue) const +{ + if (std::find(processing.begin(), processing.end(), t) != processing.end()) + { + Debug("datatypes-gt") << "...already processing " << t << " " << d_self + << std::endl; + return Node(); + } + processing.push_back(t); + for (unsigned r = 0; r < 2; r++) + { + for (std::shared_ptr ctor : d_constructors) + { + // do nullary constructors first + if ((ctor->getNumArgs() == 0) != (r == 0)) + { + continue; + } + Trace("datatypes-init") + << "Try constructing for " << ctor->getName() + << ", processing = " << processing.size() << std::endl; + Node e = ctor->computeGroundTerm(t, processing, d_groundTerm, isValue); + if (!e.isNull()) + { + // must check subterms for the same type to avoid infinite loops in + // type enumeration + Node se = getSubtermWithType(e, t, true); + if (!se.isNull()) + { + Trace("datatypes-init") << "Take subterm " << se << std::endl; + e = se; + } + processing.pop_back(); + return e; + } + else + { + Trace("datatypes-init") << "...failed." << std::endl; + } + } + } + processing.pop_back(); + return Node(); +} + +TypeNode DType::getTypeNode() const +{ + Assert(isResolved()); + Assert(!d_self.isNull()); + return d_self; +} + +TypeNode DType::getTypeNode(const std::vector& params) const +{ + Assert(isResolved()); + Assert(!d_self.isNull() && d_self.isParametricDatatype()); + return d_self.instantiateParametricDatatype(params); +} + +const DTypeConstructor& DType::operator[](size_t index) const +{ + Assert(index < getNumConstructors()); + return *d_constructors[index]; +} + +Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const +{ + Assert(isResolved()); + std::map > >::iterator + itd = d_sharedSel.find(dtt); + if (itd != d_sharedSel.end()) + { + std::map >::iterator its = + itd->second.find(t); + if (its != itd->second.end()) + { + std::map::iterator it = its->second.find(index); + if (it != its->second.end()) + { + return it->second; + } + } + } + // make the shared selector + Node s; + NodeManager* nm = NodeManager::currentNM(); + std::stringstream ss; + ss << "sel_" << index; + s = nm->mkSkolem(ss.str(), + nm->mkSelectorType(dtt, t), + "is a shared selector", + NodeManager::SKOLEM_NO_NOTIFY); + d_sharedSel[dtt][t][index] = s; + Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t + << std::endl; + return s; +} + +TypeNode DType::getSygusType() const { return d_sygusType; } + +Node DType::getSygusVarList() const { return d_sygusBvl; } + +bool DType::getSygusAllowConst() const { return d_sygusAllowConst; } + +bool DType::getSygusAllowAll() const { return d_sygusAllowAll; } + +bool DType::involvesExternalType() const { return d_involvesExt; } + +bool DType::involvesUninterpretedType() const { return d_involvesUt; } + +const std::vector >& DType::getConstructors() + const +{ + return d_constructors; +} + +std::ostream& operator<<(std::ostream& os, const DType& dt) +{ + // can only output datatypes in the CVC4 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + dt.toStream(os); + return os; +} + +void DType::toStream(std::ostream& out) const +{ + out << "DATATYPE " << getName(); + if (isParametric()) + { + out << '['; + for (size_t i = 0, nparams = getNumParameters(); i < nparams; ++i) + { + if (i > 0) + { + out << ','; + } + out << getParameter(i); + } + out << ']'; + } + out << " = " << std::endl; + bool firstTime = true; + for (std::shared_ptr ctor : d_constructors) + { + if (!firstTime) + { + out << " | "; + } + firstTime = false; + out << *ctor; + } + out << " END;" << std::endl; +} + +DTypeIndexConstant::DTypeIndexConstant(size_t index) : d_index(index) {} +std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic) +{ + return out << "index_" << dic.getIndex(); +} + +} // namespace CVC4 diff --git a/src/expr/dtype.h b/src/expr/dtype.h new file mode 100644 index 000000000..b2399472a --- /dev/null +++ b/src/expr/dtype.h @@ -0,0 +1,615 @@ +/********************* */ +/*! \file dtype.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype definition + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__DTYPE_H +#define CVC4__EXPR__DTYPE_H + +#include +#include +#include +#include "expr/dtype_cons.h" +#include "expr/dtype_selector.h" +#include "expr/node.h" +#include "expr/node_manager_attributes.h" +#include "expr/type_node.h" + +namespace CVC4 { + +// ----------------------- datatype attributes +/** + * Attribute for the index of an expression within a datatype, which is either: + * (1) If the expression is a constructor, then its index refers to its + * placement in the constructor list of the datatype that owns it, (2) If the + * expression is a selector, then its index refers to its placement in the + * argument list of the constructor that owns it. + */ +struct DTypeIndexTag +{ +}; +typedef expr::Attribute DTypeIndexAttr; +/** + * Attribute for the constructor index of a selector. This indicates the index + * (DTypeIndexAttr) of the constructor that owns this selector. + */ +struct DTypeConsIndexTag +{ +}; +typedef expr::Attribute DTypeConsIndexAttr; +/** Attribute true for datatype types that are finite. */ +struct DTypeFiniteTag +{ +}; +typedef expr::Attribute DTypeFiniteAttr; +/** Attribute true when we have computed whether a datatype type is finite */ +struct DTypeFiniteComputedTag +{ +}; +typedef expr::Attribute DTypeFiniteComputedAttr; +/** + * Attribute true for datatype types that are interpreted as finite (see + * TypeNode::isInterpretedFinite). + */ +struct DTypeUFiniteTag +{ +}; +typedef expr::Attribute DTypeUFiniteAttr; +/** + * Attribute true when we have computed whether a datatype type is interpreted + * as finite. + */ +struct DTypeUFiniteComputedTag +{ +}; +typedef expr::Attribute DTypeUFiniteComputedAttr; +// ----------------------- end datatype attributes + +class NodeManager; + +class Datatype; + +/** + * The Node-level representation of an inductive datatype, which currently + * resides within the Expr-level Datatype class (expr/datatype.h). + * + * Notice that this class is a specification for a datatype, and is not + * itself a type. The type that this specification corresponds to can be + * retrieved (after resolution as described in the following) via getTypeNode. + * + * This is far more complicated than it first seems. Consider this + * datatype definition: + * + * DATATYPE nat = + * succ(pred: nat) + * | zero + * END; + * + * You cannot define "nat" until you have a Type for it, but you + * cannot have a Type for it until you fill in the type of the "pred" + * selector, which needs the Type. So we have a chicken-and-egg + * problem. It's even more complicated when we have mutual recursion + * between datatypes, since the CVC presentation language does not + * require forward-declarations. Here, we define trees of lists that + * contain trees of lists (etc): + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(list), + * list = cons(car: tree, cdr: list) | nil + * END; + * + * We build DType objects to describe "tree" and "list", and their constructors + * and constructor arguments, but leave any unknown types (including + * self-references) in an "unresolved" state. After parsing the whole DATATYPE + * block, we create a TypeNode through ExprManager::mkMutualDatatypeTypes(). + * The ExprManager creates a Type for each, but before "releasing" this type + * into the wild, it does a round of in-place "resolution" on each DType by + * calling DType::resolve() with a map of string -> TypeNode to + * allow the datatype to construct the necessary testers and selectors. + * + * An additional point to make is that we want to ease the burden on + * both the parser AND the users of the CVC4 API, so this class takes + * on the task of generating its own selectors and testers, for + * instance. That means that, after reifying the DType with the + * NodeManager, the parser needs to go through the (now-resolved) + * DType and request the constructor, selector, and tester terms. + * See src/parser/parser.cpp for how this is done. For API usage + * ideas, see test/unit/util/datatype_black.h. + * + * DTypes may also be defined parametrically, such as this example: + * + * DATATYPE + * list[T] = cons(car : T, cdr : list[T]) | null, + * tree = node(children : list[tree]) | leaf + * END; + * + * Here, the definition of the parametric datatype list, where T is a type + * variable. In other words, this defines a family of types list[C] where C is + * any concrete type. DTypes can be parameterized over multiple type variables + * using the syntax sym[ T1, ..., Tn ] = ..., + * + */ +class DType +{ + friend class Datatype; + friend class DTypeConstructor; + friend class NodeManager; // for access to resolve() + + public: + /** + * Get the datatype of a constructor, selector, or tester operator. + */ + static const DType& datatypeOf(Node item); + + /** + * Get the index of a constructor or tester in its datatype, or the + * index of a selector in its constructor. (Zero is always the + * first index.) + */ + static size_t indexOf(Node item); + + /** + * Get the index of constructor corresponding to selector. (Zero is + * always the first index.) + */ + static size_t cindexOf(Node item); + + /** + * Same as above, but without checks. These methods should be used by + * internal (Node-level) code. + */ + static size_t indexOfInternal(Node item); + static size_t cindexOfInternal(Node item); + + /** Create a new DType of the given name. */ + DType(std::string name, bool isCo = false); + + /** + * Create a new DType of the given name, with the given + * parameterization. + */ + DType(std::string name, + const std::vector& params, + bool isCo = false); + + ~DType(); + + /** Add a constructor to this DType. + * + * Notice that constructor names need not + * be unique; they are for convenience and pretty-printing only. + */ + void addConstructor(std::shared_ptr c); + + /** set sygus + * + * This marks this datatype as a sygus datatype. + * A sygus datatype is one that represents terms of type st + * via a deep embedding described in Section 4 of + * Reynolds et al. CAV 2015. We say that this sygus datatype + * "encodes" its sygus type st in the following. + * + * st : the type this datatype encodes (this can be Int, Bool, etc.), + * bvl : the list of arguments for the synth-fun + * allow_const : whether all constants are (implicitly) allowed by the + * datatype + * allow_all : whether all terms are (implicitly) allowed by the datatype + * + * Notice that allow_const/allow_all do not reflect the constructors + * for this datatype, and instead are used solely for relaxing constraints + * when doing solution reconstruction (Figure 5 of Reynolds et al. + * CAV 2015). + */ + void setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll); + + /** set that this datatype is a tuple */ + void setTuple(); + + /** Get the name of this DType. */ + std::string getName() const; + + /** Get the number of constructors (so far) for this DType. */ + size_t getNumConstructors() const; + + /** Is this datatype parametric? */ + bool isParametric() const; + + /** Get the number of type parameters */ + size_t getNumParameters() const; + + /** Get parameter */ + TypeNode getParameter(size_t i) const; + + /** Get parameters */ + std::vector getParameters() const; + + /** is this a co-datatype? */ + bool isCodatatype() const; + + /** is this a sygus datatype? */ + bool isSygus() const; + + /** is this a tuple datatype? */ + bool isTuple() const; + + /** get the record representation for this datatype */ + Record* getRecord() const; + + /** + * Return the cardinality of this datatype. + * The DType must be resolved. + * + * The version of this method that takes type t is required + * for parametric datatypes, where t is an instantiated + * parametric datatype type whose datatype is this class. + */ + Cardinality getCardinality(TypeNode t) const; + Cardinality getCardinality() const; + + /** + * Return true iff this DType has finite cardinality. If the + * datatype is not well-founded, this method returns false. The + * DType must be resolved or an assertion is violated. + * + * The version of this method that takes type t is required + * for parametric datatypes, where t is an instantiated + * parametric datatype type whose datatype is this class. + */ + bool isFinite(TypeNode t) const; + bool isFinite() const; + + /** + * Return true iff this DType is finite (all constructors are + * finite, i.e., there are finitely many ground terms) under the + * assumption that unintepreted sorts are finite. If the + * datatype is not well-founded, this method returns false. The + * DType must be resolved or an assertion is violated. + * + * The versions of these methods that takes type t is required + * for parametric datatypes, where t is an instantiated + * parametric datatype type whose datatype is this class. + */ + bool isInterpretedFinite(TypeNode t) const; + bool isInterpretedFinite() const; + + /** is well-founded + * + * Return true iff this datatype is well-founded (there exist finite + * values of this type). This datatype must be resolved or an assertion is + * violated. + */ + bool isWellFounded() const; + + /** is recursive singleton + * + * Return true iff this datatype is a recursive singleton + * (a recursive singleton is a recursive datatype with only + * one infinite value). For details, see Reynolds et al. CADE 2015. + * + * The versions of these methods that takes type t is required + * for parametric datatypes, where t is an instantiated + * parametric datatype type whose datatype is this class. + */ + bool isRecursiveSingleton(TypeNode t) const; + bool isRecursiveSingleton() const; + + /** recursive single arguments + * + * Get recursive singleton argument types (uninterpreted sorts that the + * cardinality of this datatype is dependent upon). For example, for : + * stream := cons( head1 : U1, head2 : U2, tail : stream ) + * Then, the recursive singleton argument types of stream are { U1, U2 }, + * since if U1 and U2 have cardinality one, then stream has cardinality + * one as well. + * + * The versions of these methods that takes Type t is required + * for parametric datatypes, where t is an instantiated + * parametric datatype type whose datatype is this class. + */ + unsigned getNumRecursiveSingletonArgTypes(TypeNode t) const; + TypeNode getRecursiveSingletonArgType(TypeNode t, size_t i) const; + unsigned getNumRecursiveSingletonArgTypes() const; + TypeNode getRecursiveSingletonArgType(size_t i) const; + + /** + * Construct and return a ground term of this DType. The + * DType must be both resolved and well-founded, or else an + * exception is thrown. + * + * This method takes a type t, which is a datatype type whose + * datatype is this class, which may be an instantiated datatype + * type if this datatype is parametric. + */ + Node mkGroundTerm(TypeNode t) const; + /** Make ground value + * + * Same as above, but constructs a constant value instead of a ground term. + * These two notions typically coincide. However, for uninterpreted sorts, + * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns + * an uninterpreted constant. The motivation for mkGroundTerm is that + * unintepreted constants should never appear in lemmas. The motivation for + * mkGroundValue is for things like type enumeration and model construction. + */ + Node mkGroundValue(TypeNode t) const; + + /** + * Get the TypeNode associated to this DType. Can only be + * called post-resolution. + */ + TypeNode getTypeNode() const; + + /** + * Get the TypeNode associated to this (parameterized) DType. Can only be + * called post-resolution. + */ + TypeNode getTypeNode(const std::vector& params) const; + + /** Return true iff this DType has already been resolved. */ + bool isResolved() const; + + /** Get the ith DTypeConstructor. */ + const DTypeConstructor& operator[](size_t index) const; + + /** get sygus type + * This gets the built-in type associated with + * this sygus datatype, i.e. the type of the + * term that this sygus datatype encodes. + */ + TypeNode getSygusType() const; + + /** get sygus var list + * This gets the variable list of the function + * to synthesize using this sygus datatype. + * For example, if we are synthesizing a binary + * function f where solutions are of the form: + * f = (lambda (xy) t[x,y]) + * In this case, this method returns the + * bound variable list containing x and y. + */ + Node getSygusVarList() const; + /** get sygus allow constants + * + * Does this sygus datatype allow constants? + * Notice that this is not a property of the + * constructors of this datatype. Instead, it is + * an auxiliary flag (provided in the call + * to setSygus). + */ + bool getSygusAllowConst() const; + /** get sygus allow all + * + * Does this sygus datatype allow all terms? + * Notice that this is not a property of the + * constructors of this datatype. Instead, it is + * an auxiliary flag (provided in the call + * to setSygus). + */ + bool getSygusAllowAll() const; + + /** involves external type + * Get whether this datatype has a subfield + * in any constructor that is not a datatype type. + */ + bool involvesExternalType() const; + /** involves uninterpreted type + * Get whether this datatype has a subfield + * in any constructor that is an uninterpreted type. + */ + bool involvesUninterpretedType() const; + + /** + * Get the list of constructors. + */ + const std::vector >& getConstructors() + const; + + /** prints this datatype to stream */ + void toStream(std::ostream& out) const; + + private: + /** + * DTypes refer to themselves, recursively, and we have a + * chicken-and-egg problem. The TypeNode around the DType + * cannot exist until the DType is finalized, and the DType + * cannot refer to the TypeNode representing itself until it + * exists. resolve() is called by the NodeManager when a type is + * ultimately requested of the DType specification (that is, when + * NodeManager::mkTypeNode() or NodeManager::mkMutualTypeNodes() + * is called). Has the effect of freezing the object, too; that is, + * addConstructor() will fail after a call to resolve(). + * + * The basic goal of resolution is to assign constructors, selectors, + * and testers. To do this, any UnresolvedType/SelfType references + * must be cleared up. This is the purpose of the "resolutions" map; + * it includes any mutually-recursive datatypes that are currently + * under resolution. The four vectors come in two pairs (so, really + * they are two maps). placeholders->replacements give type variables + * that should be resolved in the case of parametric datatypes. + * + * @param em the NodeManager at play + * @param resolutions a map of strings to TypeNodes currently under + * resolution + * @param placeholders the types in these DTypes under resolution that must + * be replaced + * @param replacements the corresponding replacements + * @param paramTypes the sort constructors in these DTypes under resolution + * that must be replaced + * @param paramReplacements the corresponding (parametric) TypeNodes + */ + bool resolve(const std::map& resolutions, + const std::vector& placeholders, + const std::vector& replacements, + const std::vector& paramTypes, + const std::vector& paramReplacements); + + /** compute the cardinality of this datatype */ + Cardinality computeCardinality(TypeNode t, + std::vector& processing) const; + /** compute whether this datatype is a recursive singleton */ + bool computeCardinalityRecSingleton(TypeNode t, + std::vector& processing, + std::vector& u_assume) const; + /** compute whether this datatype is well-founded */ + bool computeWellFounded(std::vector& processing) const; + /** compute ground term + * + * This method checks if there is a term of this datatype whose type is t + * that is finitely constructable. As needed, it traverses its subfield types. + * + * The argument processing is the set of datatype types we are currently + * traversing. + * + * The argument isValue is whether we are constructing a constant value. If + * this flag is false, we are constructing a canonical ground term that is + * not necessarily constant. + */ + Node computeGroundTerm(TypeNode t, + std::vector& processing, + bool isValue) const; + /** Get the shared selector + * + * This returns the index^th (constructor-agnostic) + * selector for type t. The type dtt is the datatype + * type whose datatype is this class, where this may + * be an instantiated parametric datatype. + * + * In the terminology of "DTypes with Shared Selectors", + * this returns the term sel_{dtt}^{t,index}. + */ + Node getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const; + /** + * Helper for mkGroundTerm and mkGroundValue above. + */ + Node mkGroundTermInternal(TypeNode t, bool isValue) const; + /** name of this datatype */ + std::string d_name; + /** the type parameters of this datatype (if this is a parametric datatype) + */ + std::vector d_params; + /** whether the datatype is a codatatype. */ + bool d_isCo; + /** whether the datatype is a tuple */ + bool d_isTuple; + /** the constructors of this datatype */ + std::vector > d_constructors; + /** whether this datatype has been resolved */ + bool d_resolved; + /** self type */ + mutable TypeNode d_self; + /** cache for involves external type */ + bool d_involvesExt; + /** cache for involves uninterpreted type */ + bool d_involvesUt; + /** the builtin type that this sygus type encodes */ + TypeNode d_sygusType; + /** the variable list for the sygus function to synthesize */ + Node d_sygusBvl; + /** whether all constants are allowed as solutions */ + bool d_sygusAllowConst; + /** whether all terms are allowed as solutions */ + bool d_sygusAllowAll; + + /** the cardinality of this datatype + * "mutable" because computing the cardinality can be expensive, + * and so it's computed just once, on demand---this is the cache + */ + mutable Cardinality d_card; + + /** is this type a recursive singleton type? + * The range of this map stores + * 0 if the field has not been computed, + * 1 if this datatype is a recursive singleton type, + * -1 if this datatype is not a recursive singleton type. + * For definition of (co)recursive singleton, see + * Section 2 of Reynolds et al. CADE 2015. + */ + mutable std::map d_cardRecSingleton; + /** if d_cardRecSingleton is true, + * This datatype has infinite cardinality if at least one of the + * following uninterpreted sorts having cardinality > 1. + */ + mutable std::map > d_cardUAssume; + /** + * Cache of whether this datatype is well-founded, where 0 means we have + * not computed this information, 1 means it is well-founded, -1 means it is + * not. + */ + mutable int d_wellFounded; + /** cache of ground term for this datatype */ + mutable std::map d_groundTerm; + /** cache of ground values for this datatype */ + mutable std::map d_groundValue; + /** cache of shared selectors for this datatype */ + mutable std::map > > + d_sharedSel; +}; /* class DType */ + +/** + * A hash function for DTypes. Needed to store them in hash sets + * and hash maps. + */ +struct DTypeHashFunction +{ + size_t operator()(const DType& dt) const + { + return std::hash()(dt.getName()); + } + size_t operator()(const DType* dt) const + { + return std::hash()(dt->getName()); + } +}; /* struct DTypeHashFunction */ + +/* stores an index to DType residing in NodeManager */ +class DTypeIndexConstant +{ + public: + DTypeIndexConstant(size_t index); + + size_t getIndex() const { return d_index; } + bool operator==(const DTypeIndexConstant& uc) const + { + return d_index == uc.d_index; + } + bool operator!=(const DTypeIndexConstant& uc) const { return !(*this == uc); } + bool operator<(const DTypeIndexConstant& uc) const + { + return d_index < uc.d_index; + } + bool operator<=(const DTypeIndexConstant& uc) const + { + return d_index <= uc.d_index; + } + bool operator>(const DTypeIndexConstant& uc) const { return !(*this <= uc); } + bool operator>=(const DTypeIndexConstant& uc) const { return !(*this < uc); } + + private: + const size_t d_index; +}; /* class DTypeIndexConstant */ + +std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic); + +struct DTypeIndexConstantHashFunction +{ + size_t operator()(const DTypeIndexConstant& dic) const + { + return IntegerHashFunction()(dic.getIndex()); + } +}; /* struct DTypeIndexConstantHashFunction */ + +std::ostream& operator<<(std::ostream& os, const DType& dt); + +} // namespace CVC4 + +#endif diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp new file mode 100644 index 000000000..428097d54 --- /dev/null +++ b/src/expr/dtype_cons.cpp @@ -0,0 +1,649 @@ +/********************* */ +/*! \file dtype_cons.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype definition + **/ +#include "expr/dtype_cons.h" + +#include "expr/dtype.h" +#include "expr/node_manager.h" +#include "expr/type_matcher.h" +#include "options/datatypes_options.h" + +using namespace CVC4::kind; +using namespace CVC4::theory; + +namespace CVC4 { + +DTypeConstructor::DTypeConstructor(std::string name, + unsigned weight) + : // 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 + // the tester name away inside the constructor name until + // resolution. + d_name(name), + d_tester(), + d_args(), + d_weight(weight) +{ + Assert(name != ""); +} + +void DTypeConstructor::addArg(std::string selectorName, TypeNode 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 + // the selector type away inside a var until resolution (when we can + // create the proper selector type) + Assert(!isResolved()); + Assert(!selectorType.isNull()); + + Node type = NodeManager::currentNM()->mkSkolem( + "unresolved_" + selectorName, + selectorType, + "is an unresolved selector type placeholder", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + Trace("datatypes") << type << std::endl; + std::shared_ptr a = + std::make_shared(selectorName, type); + addArg(a); +} + +void DTypeConstructor::addArg(std::shared_ptr a) +{ + d_args.push_back(a); +} + +std::string DTypeConstructor::getName() const { return d_name; } + +Node DTypeConstructor::getConstructor() const +{ + Assert(isResolved()); + return d_constructor; +} + +Node DTypeConstructor::getTester() const +{ + Assert(isResolved()); + return d_tester; +} + +void DTypeConstructor::setSygus(Node op) +{ + Assert(!isResolved()); + d_sygusOp = op; +} + +Node DTypeConstructor::getSygusOp() const +{ + Assert(isResolved()); + return d_sygusOp; +} + +bool DTypeConstructor::isSygusIdFunc() const +{ + Assert(isResolved()); + return (d_sygusOp.getKind() == LAMBDA && d_sygusOp[0].getNumChildren() == 1 + && d_sygusOp[0][0] == d_sygusOp[1]); +} + +unsigned DTypeConstructor::getWeight() const +{ + Assert(isResolved()); + return d_weight; +} + +size_t DTypeConstructor::getNumArgs() const { return d_args.size(); } + +TypeNode DTypeConstructor::getSpecializedConstructorType( + TypeNode returnType) const +{ + Assert(isResolved()); + Assert(returnType.isDatatype()); + const DType& dt = DType::datatypeOf(d_constructor); + Assert(dt.isParametric()); + TypeNode dtt = dt.getTypeNode(); + TypeMatcher m(dtt); + m.doMatching(dtt, returnType); + std::vector subst; + m.getMatches(subst); + std::vector params = dt.getParameters(); + return d_constructor.getType().substitute( + params.begin(), params.end(), subst.begin(), subst.end()); +} + +const std::vector >& DTypeConstructor::getArgs() + const +{ + return d_args; +} + +Cardinality DTypeConstructor::getCardinality(TypeNode t) const +{ + Assert(isResolved()); + + Cardinality c = 1; + + for (size_t i = 0, nargs = d_args.size(); i < nargs; i++) + { + c *= getArgType(i).getCardinality(); + } + + return c; +} + +bool DTypeConstructor::isFinite(TypeNode t) const +{ + Assert(isResolved()); + + TNode self = d_constructor; + // is this already in the cache ? + if (self.getAttribute(DTypeFiniteComputedAttr())) + { + return self.getAttribute(DTypeFiniteAttr()); + } + std::vector instTypes; + std::vector paramTypes; + bool isParam = t.isParametricDatatype(); + if (isParam) + { + paramTypes = t.getDType().getParameters(); + instTypes = TypeNode(t).getParamTypes(); + } + for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) + { + TypeNode tc = getArgType(i); + if (isParam) + { + tc = tc.substitute(paramTypes.begin(), + paramTypes.end(), + instTypes.begin(), + instTypes.end()); + } + if (!tc.isFinite()) + { + self.setAttribute(DTypeFiniteComputedAttr(), true); + self.setAttribute(DTypeFiniteAttr(), false); + return false; + } + } + self.setAttribute(DTypeFiniteComputedAttr(), true); + self.setAttribute(DTypeFiniteAttr(), true); + return true; +} + +bool DTypeConstructor::isInterpretedFinite(TypeNode t) const +{ + Assert(isResolved()); + TNode self = d_constructor; + // is this already in the cache ? + if (self.getAttribute(DTypeUFiniteComputedAttr())) + { + return self.getAttribute(DTypeUFiniteAttr()); + } + std::vector instTypes; + std::vector paramTypes; + bool isParam = t.isParametricDatatype(); + if (isParam) + { + paramTypes = t.getDType().getParameters(); + instTypes = TypeNode(t).getParamTypes(); + } + for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++) + { + TypeNode tc = getArgType(i); + if (isParam) + { + tc = tc.substitute(paramTypes.begin(), + paramTypes.end(), + instTypes.begin(), + instTypes.end()); + } + if (!tc.isInterpretedFinite()) + { + self.setAttribute(DTypeUFiniteComputedAttr(), true); + self.setAttribute(DTypeUFiniteAttr(), false); + return false; + } + } + self.setAttribute(DTypeUFiniteComputedAttr(), true); + self.setAttribute(DTypeUFiniteAttr(), true); + return true; +} + +bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); } + +const DTypeSelector& DTypeConstructor::operator[](size_t index) const +{ + Assert(index < getNumArgs()); + return *d_args[index]; +} + +TypeNode DTypeConstructor::getArgType(size_t index) const +{ + Assert(index < getNumArgs()); + return (*this)[index].getType().getSelectorRangeType(); +} + +Node DTypeConstructor::getSelectorInternal(TypeNode domainType, + size_t index) const +{ + Assert(isResolved()); + Assert(index < getNumArgs()); + if (options::dtSharedSelectors()) + { + computeSharedSelectors(domainType); + Assert(d_sharedSelectors[domainType].size() == getNumArgs()); + return d_sharedSelectors[domainType][index]; + } + else + { + return d_args[index]->getSelector(); + } +} + +int DTypeConstructor::getSelectorIndexInternal(Node sel) const +{ + Assert(isResolved()); + if (options::dtSharedSelectors()) + { + Assert(sel.getType().isSelector()); + TypeNode domainType = sel.getType().getSelectorDomainType(); + computeSharedSelectors(domainType); + std::map::iterator its = + d_sharedSelectorIndex[domainType].find(sel); + if (its != d_sharedSelectorIndex[domainType].end()) + { + return (int)its->second; + } + } + else + { + unsigned sindex = DType::indexOf(sel); + if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel) + { + return static_cast(sindex); + } + } + return -1; +} + +bool DTypeConstructor::involvesExternalType() const +{ + for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) + { + if (!getArgType(i).isDatatype()) + { + return true; + } + } + return false; +} + +bool DTypeConstructor::involvesUninterpretedType() const +{ + for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) + { + if (!getArgType(i).isSort()) + { + return true; + } + } + return false; +} + +Cardinality DTypeConstructor::computeCardinality( + TypeNode t, std::vector& processing) const +{ + Cardinality c = 1; + std::vector instTypes; + std::vector paramTypes; + bool isParam = t.isParametricDatatype(); + if (isParam) + { + paramTypes = t.getDType().getParameters(); + instTypes = t.getParamTypes(); + } + for (size_t i = 0, nargs = d_args.size(); i < nargs; i++) + { + TypeNode tc = getArgType(i); + if (isParam) + { + tc = tc.substitute(paramTypes.begin(), + paramTypes.end(), + instTypes.begin(), + instTypes.end()); + } + if (tc.isDatatype()) + { + const DType& dt = tc.getDType(); + c *= dt.computeCardinality(t, processing); + } + else + { + c *= tc.getCardinality(); + } + } + return c; +} + +bool DTypeConstructor::computeWellFounded( + std::vector& processing) const +{ + for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) + { + TypeNode t = getArgType(i); + if (t.isDatatype()) + { + const DType& dt = t.getDType(); + if (!dt.computeWellFounded(processing)) + { + return false; + } + } + } + return true; +} + +Node DTypeConstructor::computeGroundTerm(TypeNode t, + std::vector& processing, + std::map& gt, + bool isValue) const +{ + NodeManager* nm = NodeManager::currentNM(); + std::vector groundTerms; + groundTerms.push_back(getConstructor()); + + // for each selector, get a ground term + std::vector instTypes; + std::vector paramTypes; + bool isParam = t.isParametricDatatype(); + if (isParam) + { + paramTypes = t.getDType().getParameters(); + instTypes = TypeNode(t).getParamTypes(); + } + for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) + { + TypeNode selType = getArgType(i); + if (isParam) + { + selType = selType.substitute(paramTypes.begin(), + paramTypes.end(), + instTypes.begin(), + instTypes.end()); + } + Node arg; + if (selType.isDatatype()) + { + std::map::iterator itgt = gt.find(selType); + if (itgt != gt.end()) + { + arg = itgt->second; + } + else + { + const DType& dt = selType.getDType(); + arg = dt.computeGroundTerm(selType, processing, isValue); + } + } + else + { + // call mkGroundValue or mkGroundTerm based on isValue + arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm(); + } + if (arg.isNull()) + { + Trace("datatypes") << "...unable to construct arg of " + << d_args[i]->getName() << std::endl; + return Node(); + } + else + { + Trace("datatypes") << "...constructed arg " << arg.getType() << std::endl; + groundTerms.push_back(arg); + } + } + + Node groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms); + if (isParam) + { + Assert(DType::datatypeOf(d_constructor).isParametric()); + // type is parametric, must apply type ascription + Debug("datatypes-gt") << "ambiguous type for " << groundTerm + << ", ascribe to " << t << std::endl; + groundTerms[0] = nm->mkNode( + APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(getSpecializedConstructorType(t).toType())), + groundTerms[0]); + groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms); + } + return groundTerm; +} + +void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const +{ + if (d_sharedSelectors[domainType].size() < getNumArgs()) + { + TypeNode ctype; + if (domainType.isParametricDatatype()) + { + ctype = getSpecializedConstructorType(domainType); + } + else + { + ctype = d_constructor.getType(); + } + Assert(ctype.isConstructor()); + Assert(ctype.getNumChildren() - 1 == getNumArgs()); + // compute the shared selectors + const DType& dt = DType::datatypeOf(d_constructor); + std::map counter; + for (size_t j = 0, jend = ctype.getNumChildren() - 1; j < jend; j++) + { + TypeNode t = ctype[j]; + Node ss = dt.getSharedSelector(domainType, t, counter[t]); + d_sharedSelectors[domainType].push_back(ss); + Assert(d_sharedSelectorIndex[domainType].find(ss) + == d_sharedSelectorIndex[domainType].end()); + d_sharedSelectorIndex[domainType][ss] = j; + counter[t]++; + } + } +} + +bool DTypeConstructor::resolve( + TypeNode self, + const std::map& resolutions, + const std::vector& placeholders, + const std::vector& replacements, + const std::vector& paramTypes, + const std::vector& paramReplacements, + size_t cindex) +{ + if (isResolved()) + { + // already resolved, fail + return false; + } + Trace("datatypes") << "DTypeConstructor::resolve, self type is " << self + << std::endl; + + NodeManager* nm = NodeManager::currentNM(); + size_t index = 0; + std::vector argTypes; + for (std::shared_ptr arg : d_args) + { + std::string argName = arg->d_name; + TypeNode range; + if (arg->d_selector.isNull()) + { + // the unresolved type wasn't created here; do name resolution + std::string typeName = argName.substr(argName.find('\0') + 1); + argName.resize(argName.find('\0')); + if (typeName == "") + { + range = self; + arg->d_selector = nm->mkSkolem( + argName, + nm->mkSelectorType(self, self), + "is a selector", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + } + else + { + std::map::const_iterator j = + resolutions.find(typeName); + if (j == resolutions.end()) + { + // failed to resolve selector + return false; + } + else + { + range = (*j).second; + arg->d_selector = nm->mkSkolem( + argName, + nm->mkSelectorType(self, range), + "is a selector", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + } + } + } + else + { + // the type for the selector already exists; may need + // complex-type substitution + range = arg->d_selector.getType(); + if (!placeholders.empty()) + { + range = range.substitute(placeholders.begin(), + placeholders.end(), + replacements.begin(), + replacements.end()); + } + if (!paramTypes.empty()) + { + range = doParametricSubstitution(range, paramTypes, paramReplacements); + } + arg->d_selector = nm->mkSkolem( + argName, + nm->mkSelectorType(self, range), + "is a selector", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + } + arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex); + arg->d_selector.setAttribute(DTypeIndexAttr(), index++); + arg->d_resolved = true; + argTypes.push_back(range); + } + + Assert(index == getNumArgs()); + + // Set constructor/tester last, since DTypeConstructor::isResolved() + // returns true when d_tester is not the null Node. If something + // fails above, we want Constuctor::isResolved() to remain "false". + // Further, mkConstructorType() iterates over the selectors, so + // should get the results of any resolutions we did above. + // The name of the tester variable does not matter, it is only used + // internally. + std::string testerName("is_" + d_name); + d_tester = nm->mkSkolem( + testerName, + nm->mkTesterType(self), + "is a tester", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + d_constructor = nm->mkSkolem( + getName(), + nm->mkConstructorType(argTypes, self), + "is a constructor", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + Assert(d_constructor.getType().isConstructor()); + // associate constructor with all selectors + for (std::shared_ptr sel : d_args) + { + sel->d_constructor = d_constructor; + } + Assert(isResolved()); + return true; +} + +TypeNode DTypeConstructor::doParametricSubstitution( + TypeNode range, + const std::vector& paramTypes, + const std::vector& paramReplacements) +{ + if (range.getNumChildren() == 0) + { + return range; + } + std::vector origChildren; + std::vector children; + for (TypeNode::const_iterator i = range.begin(), iend = range.end(); + i != iend; + ++i) + { + origChildren.push_back((*i)); + children.push_back( + doParametricSubstitution((*i), paramTypes, paramReplacements)); + } + for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i) + { + if (paramTypes[i].getNumChildren() + 1 == origChildren.size()) + { + TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren); + if (range == tn) + { + TypeNode tret = + paramReplacements[i].instantiateParametricDatatype(children); + return tret; + } + } + } + NodeBuilder<> nb(range.getKind()); + for (size_t i = 0, csize = children.size(); i < csize; ++i) + { + nb << children[i]; + } + TypeNode tn = nb.constructTypeNode(); + return tn; +} + +void DTypeConstructor::toStream(std::ostream& out) const +{ + out << getName(); + + unsigned nargs = getNumArgs(); + if (nargs == 0) + { + return; + } + out << "("; + for (unsigned i = 0; i < nargs; i++) + { + out << *d_args[i]; + if (i + 1 < nargs) + { + out << ", "; + } + } + out << ")"; +} + +std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor) +{ + // can only output datatypes in the CVC4 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + ctor.toStream(os); + return os; +} + +} // namespace CVC4 diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h new file mode 100644 index 000000000..d5d0013de --- /dev/null +++ b/src/expr/dtype_cons.h @@ -0,0 +1,335 @@ +/********************* */ +/*! \file dtype_cons.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype definition + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__DTYPE_CONS_H +#define CVC4__EXPR__DTYPE_CONS_H + +#include +#include +#include +#include "expr/dtype_selector.h" +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class DatatypeConstructor; + +/** + * The Node-level representation of a constructor for a datatype, which + * currently resides in the Expr-level DatatypeConstructor class + * (expr/datatype.h). + */ +class DTypeConstructor +{ + friend class DatatypeConstructor; + friend class DType; + + public: + /** + * Create a new datatype constructor with the given name for the + * constructor and the same name (prefixed with "is_") for the + * tester. The actual constructor and tester (meaning, the Nodes + * representing operators for these entities) aren't created until + * resolution time. + * + * weight is the value that this constructor carries when computing size + * for SyGuS. For example, if A, B, C have weights 0, 1, and 3 respectively, + * then C( B( A() ), B( A() ) ) has size 5. + */ + DTypeConstructor(std::string name, unsigned weight = 1); + + ~DTypeConstructor() {} + /** + * Add an argument (i.e., a data field) of the given name and type + * to this constructor. Selector names need not be unique; + * they are for convenience and pretty-printing only. + */ + void addArg(std::string selectorName, TypeNode selectorType); + /** + * Add an argument, given a pointer to a selector object. + */ + void addArg(std::shared_ptr a); + + /** Get the name of this constructor. */ + std::string getName() const; + + /** + * Get the constructor operator of this constructor. The + * DType must be resolved. + */ + Node getConstructor() const; + + /** + * Get the tester operator of this constructor. The + * DType must be resolved. + */ + Node getTester() const; + //-------------------------------------- sygus + /** set sygus + * + * Set that this constructor is a sygus datatype constructor that encodes + * operator op. + */ + void setSygus(Node op); + /** get sygus op + * + * This method returns the operator or + * term that this constructor represents + * in the sygus encoding. This may be a + * builtin operator, defined function, variable, + * or constant that this constructor encodes in this + * deep embedding. + */ + Node getSygusOp() const; + /** is this a sygus identity function? + * + * This returns true if the sygus operator of this datatype constructor is + * of the form (lambda (x) x). + */ + bool isSygusIdFunc() const; + /** get weight + * + * Get the weight of this constructor. This value is used when computing the + * size of datatype terms that involve this constructor. + */ + unsigned getWeight() const; + //-------------------------------------- end sygus + + /** + * Get the number of arguments (so far) of this DType constructor. + */ + size_t getNumArgs() const; + /** + * Get the list of arguments to this constructor. + */ + const std::vector >& getArgs() const; + /** + * Get the specialized constructor type for a parametric + * constructor; this call is only permitted after resolution. + * Given a (concrete) returnType, the constructor's concrete + * type in this parametric datatype is returned. + * + * For instance, if the datatype is list[T], with constructor + * "cons[T]" of type "T -> list[T] -> list[T]", then calling + * this function with "list[int]" will return the concrete + * "cons" constructor type for lists of int---namely, + * "int -> list[int] -> list[int]". + */ + TypeNode getSpecializedConstructorType(TypeNode returnType) const; + + /** + * Return the cardinality of this constructor (the product of the + * cardinalities of its arguments). + */ + Cardinality getCardinality(TypeNode t) const; + + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite). This function can + * only be called for resolved constructors. + */ + bool isFinite(TypeNode t) const; + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite) under assumption + * uninterpreted sorts are finite. This function can + * only be called for resolved constructors. + */ + bool isInterpretedFinite(TypeNode t) const; + + /** + * Returns true iff this constructor has already been + * resolved. + */ + bool isResolved() const; + + /** Get the ith DTypeConstructor arg. */ + const DTypeSelector& operator[](size_t index) const; + + /** + * Get argument type. Returns the return type of the i^th selector of this + * constructor. + */ + TypeNode getArgType(size_t i) const; + + /** get selector internal + * + * This gets the selector for the index^th argument + * of this constructor. The type dtt is the datatype + * type whose datatype is the owner of this constructor, + * where this type may be an instantiated parametric datatype. + * + * If shared selectors are enabled, + * this returns a shared (constructor-agnotic) selector, which + * in the terminology of "DTypes with Shared Selectors", is: + * sel_{dtt}^{T,atos(T,C,index)} + * where C is this constructor, and T is the type + * of the index^th field of this constructor. + * The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of + * type T of constructor term t if one exists, or is + * unconstrained otherwise. + */ + Node getSelectorInternal(TypeNode dtt, size_t index) const; + + /** get selector index internal + * + * This gets the argument number of this constructor + * that the selector sel accesses. It returns -1 if the + * selector sel is not a selector for this constructor. + * + * In the terminology of "DTypes with Shared Selectors", + * if sel is sel_{dtt}^{T,index} for some (T, index), where + * dtt is the datatype type whose datatype is the owner + * of this constructor, then this method returns + * stoa(T,C,index) + */ + int getSelectorIndexInternal(Node sel) const; + + /** involves external type + * + * Get whether this constructor has a subfield + * in any constructor that is not a datatype type. + */ + bool involvesExternalType() const; + /** involves uninterpreted type + * + * Get whether this constructor has a subfield + * in any constructor that is an uninterpreted type. + */ + bool involvesUninterpretedType() const; + /** prints this datatype constructor to stream */ + void toStream(std::ostream& out) const; + + private: + /** resolve + * + * This resolves (initializes) the constructor. For details + * on how datatypes and their constructors are resolved, see + * documentation for DType::resolve. + */ + bool resolve(TypeNode self, + const std::map& resolutions, + const std::vector& placeholders, + const std::vector& replacements, + const std::vector& paramTypes, + const std::vector& paramReplacements, + size_t cindex); + + /** Helper function for resolving parametric datatypes. + * + * This replaces instances of the TypeNode produced for unresolved + * parametric datatypes, with the corresponding resolved TypeNode. For + * example, take the parametric definition of a list, + * list[T] = cons(car : T, cdr : list[T]) | null. + * If "range" is the unresolved parametric datatype: + * DATATYPE list = + * cons(car: SORT_TAG_1, + * cdr: SORT_TAG_2(SORT_TAG_1)) | null END;, + * this function will return the resolved type: + * DATATYPE list = + * cons(car: SORT_TAG_1, + * cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END; + */ + TypeNode doParametricSubstitution( + TypeNode range, + const std::vector& paramTypes, + const std::vector& paramReplacements); + + /** compute the cardinality of this datatype */ + Cardinality computeCardinality(TypeNode t, + std::vector& processing) const; + /** compute whether this datatype is well-founded */ + bool computeWellFounded(std::vector& processing) const; + /** compute ground term + * + * This method is used for constructing a term that is an application + * of this constructor whose type is t. + * + * The argument processing is the set of datatype types we are currently + * traversing. This is used to avoid infinite loops. + * + * The argument gt caches the ground terms we have computed so far. + * + * The argument isValue is whether we are constructing a constant value. If + * this flag is false, we are constructing a canonical ground term that is + * not necessarily constant. + */ + Node computeGroundTerm(TypeNode t, + std::vector& processing, + std::map& gt, + bool isValue) const; + /** compute shared selectors + * This computes the maps d_sharedSelectors and d_sharedSelectorIndex. + */ + void computeSharedSelectors(TypeNode domainType) const; + /** the name of the constructor */ + std::string d_name; + /** the name of the tester */ + std::string d_testerName; + /** the constructor expression */ + Node d_constructor; + /** the tester for this constructor */ + Node d_tester; + /** the arguments of this constructor */ + std::vector > d_args; + /** sygus operator */ + Node d_sygusOp; + /** weight */ + unsigned d_weight; + /** shared selectors for each type + * + * This stores the shared (constructor-agnotic) + * selectors that access the fields of this datatype. + * In the terminology of "DTypes with Shared Selectors", + * this stores: + * sel_{dtt}^{T1,atos(T1,C,1)}, ..., + * sel_{dtt}^{Tn,atos(Tn,C,n)} + * where C is this constructor, which has type + * T1 x ... x Tn -> dtt above. + * We store this information for (possibly multiple) + * datatype types dtt, since this constructor may be + * for a parametric datatype, where dtt is an instantiated + * parametric datatype. + */ + mutable std::map > d_sharedSelectors; + /** for each type, a cache mapping from shared selectors to + * its argument index for this constructor. + */ + mutable std::map > d_sharedSelectorIndex; +}; /* class DTypeConstructor */ + +/** + * A hash function for DTypeConstructors. Needed to store them in hash sets + * and hash maps. + */ +struct DTypeConstructorHashFunction +{ + size_t operator()(const DTypeConstructor& dtc) const + { + return std::hash()(dtc.getName()); + } + size_t operator()(const DTypeConstructor* dtc) const + { + return std::hash()(dtc->getName()); + } +}; /* struct DTypeConstructorHashFunction */ + +std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor); + +} // namespace CVC4 + +#endif diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp new file mode 100644 index 000000000..960bbeb4d --- /dev/null +++ b/src/expr/dtype_selector.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file dtype_selector.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype selector. + **/ + +#include "expr/dtype_selector.h" + +#include "options/set_language.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +DTypeSelector::DTypeSelector(std::string name, Node selector) + : d_name(name), d_selector(selector), d_resolved(false) +{ + Assert(name != ""); +} + +std::string DTypeSelector::getName() const { return d_name; } + +Node DTypeSelector::getSelector() const +{ + Assert(d_resolved); + return d_selector; +} + +Node DTypeSelector::getConstructor() const +{ + Assert(d_resolved); + return d_constructor; +} + +TypeNode DTypeSelector::getType() const { return d_selector.getType(); } + +TypeNode DTypeSelector::getRangeType() const +{ + return getType().getRangeType(); +} + +bool DTypeSelector::isResolved() const { return d_resolved; } + +void DTypeSelector::toStream(std::ostream& out) const +{ + out << getName() << ": "; + TypeNode t; + if (d_resolved) + { + t = getRangeType(); + } + else if (d_selector.isNull()) + { + std::string typeName = d_name.substr(d_name.find('\0') + 1); + out << ((typeName == "") ? "[self]" : typeName); + return; + } + else + { + out << "unresolved"; + return; + } + out << t; +} + +std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg) +{ + // can only output datatypes in the CVC4 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + arg.toStream(os); + return os; +} + +} // namespace CVC4 diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h new file mode 100644 index 000000000..71b035d8c --- /dev/null +++ b/src/expr/dtype_selector.h @@ -0,0 +1,95 @@ +/********************* */ +/*! \file dtype_selector.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class representing a datatype selector. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__DTYPE_SELECTOR_H +#define CVC4__EXPR__DTYPE_SELECTOR_H + +#include +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class DatatypeConstructorArg; +class DType; +class DTypeConstructor; + +/** + * A datatype selector for a constructor argument (i.e., a datatype field). + */ +class DTypeSelector +{ + friend class DatatypeConstructorArg; + friend class DTypeConstructor; + friend class DType; + + public: + /** constructor */ + DTypeSelector(std::string name, Node selector); + + /** Get the name of this constructor argument. */ + std::string getName() const; + + /** + * Get the selector for this constructor argument; this call is + * only permitted after resolution. + */ + Node getSelector() const; + + /** + * Get the associated constructor for this constructor argument; + * this call is only permitted after resolution. + */ + Node getConstructor() const; + + /** + * Get the type of the selector for this constructor argument. + */ + TypeNode getType() const; + + /** + * Get the range type of this argument. + */ + TypeNode getRangeType() const; + + /** + * Returns true iff this constructor argument has been resolved. + */ + bool isResolved() const; + + /** prints this datatype constructor argument to stream */ + void toStream(std::ostream& out) const; + + private: + /** the name of this selector */ + std::string d_name; + /** the selector expression */ + Node d_selector; + /** + * The constructor associated with this selector. This field is initialized + * by the constructor of this selector during a call to + * DTypeConstructor::resolve. + */ + Node d_constructor; + /** whether this class has been resolved */ + bool d_resolved; +}; + +std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg); + +} // namespace CVC4 + +#endif diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5223fd02c..201e428de 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -24,6 +24,7 @@ #include "base/check.h" #include "base/listener.h" #include "expr/attribute.h" +#include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "expr/node_manager_listeners.h" #include "expr/type_checker.h" @@ -186,6 +187,7 @@ NodeManager::~NodeManager() { d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; + // TODO: switch to DType for (std::vector::iterator datatype_iter = d_ownedDatatypes.begin(), datatype_end = d_ownedDatatypes.end(); @@ -253,10 +255,22 @@ unsigned NodeManager::registerDatatype(Datatype* dt) { } const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ + // when the Node-level API is in place, this function will be deleted. Assert(index < d_ownedDatatypes.size()); return *d_ownedDatatypes[index]; } +const DType& NodeManager::getDTypeForIndex(unsigned index) const +{ + // when the Node-level API is in place, this function will be replaced by a + // direct lookup into a d_ownedDTypes vector, similar to d_ownedDatatypes + // above. + Unreachable() << "NodeManager::getDTypeForIndex: DType is not available in " + "the current implementation."; + const Datatype& d = getDatatypeForIndex(index); + return *d.d_internal; +} + void NodeManager::reclaimZombies() { // FIXME multithreading Assert(!d_attrManager->inGarbageCollection()); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f47795c15..61ef1d39d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -43,6 +43,8 @@ namespace CVC4 { class StatisticsRegistry; class ResourceManager; +class DType; + namespace expr { namespace attr { class AttributeUniqueId; @@ -429,6 +431,7 @@ public: unsigned registerDatatype(Datatype* dt); /** get datatype for index */ const Datatype & getDatatypeForIndex( unsigned index ) const; + const DType& getDTypeForIndex(unsigned index) const; /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 1ef5030ce..8cc10b5b2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -647,4 +647,15 @@ std::string TypeNode::toString() const { return ss.str(); } +const DType& TypeNode::getDType() const +{ + if (getKind() == kind::DATATYPE_TYPE) + { + DatatypeIndexConstant dic = getConst(); + return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex()); + } + Assert(getKind() == kind::PARAMETRIC_DATATYPE); + return (*this)[0].getDType(); +} + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 472d29f5f..b1c4da026 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -37,6 +37,7 @@ namespace CVC4 { class NodeManager; +class DType; namespace expr { class NodeValue; @@ -661,6 +662,9 @@ public: /** Get the Datatype specification from a datatype type */ const Datatype& getDatatype() const; + /** Get the internal Datatype specification from a datatype type */ + const DType& getDType() const; + /** Get the exponent size of this floating-point type */ unsigned getFloatingPointExponentSize() const;