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.
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
#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"
typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> 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<Type>& 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;
}
// 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(),
// 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(),
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");
}
class CVC4_PUBLIC DatatypeSelfType {
};/* class DatatypeSelfType */
+class DTypeSelector;
+
/**
* An unresolved type (used in calls to
* DatatypeConstructor::addArg()) to allow a Datatype to refer to
void toStream(std::ostream& out) const;
private:
+ /** The internal representation */
+ std::shared_ptr<DTypeSelector> d_internal;
/** the name of this selector */
std::string d_name;
/** the selector expression */
Expr e) const = 0;
};
+class DTypeConstructor;
+
/**
* A constructor for a Datatype.
*/
void toStream(std::ostream& out) const;
private:
+ /** The internal representation */
+ std::shared_ptr<DTypeConstructor> d_internal;
/** the name of the constructor */
std::string d_name;
/** the constructor expression */
void computeSharedSelectors(Type domainType) const;
};/* class DatatypeConstructor */
+class DType;
+
/**
* The representation of an inductive datatype.
*
*/
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.
*/
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<Type>& params, bool isCo = false);
+ Datatype(std::string name,
+ const std::vector<Type>& params,
+ bool isCo = false);
~Datatype();
void toStream(std::ostream& out) const;
private:
+ /** The internal representation */
+ std::shared_ptr<DType> d_internal;
/** name of this datatype */
std::string d_name;
/** the type parameters of this datatype (if this is a parametric datatype)
}
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<Type>& 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
--- /dev/null
+/********************* */
+/*! \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<TypeNode>& 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<TypeNode> 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<std::string, TypeNode>& resolutions,
+ const std::vector<TypeNode>& placeholders,
+ const std::vector<TypeNode>& replacements,
+ const std::vector<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& 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<DTypeConstructor> 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<DTypeConstructor> 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<Node, NodeHashFunction> 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<Node, NodeHashFunction> 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<DTypeConstructor> 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<TypeNode> processing;
+ computeCardinality(t, processing);
+ return d_card;
+}
+
+Cardinality DType::getCardinality() const
+{
+ Assert(!isParametric());
+ return getCardinality(d_self);
+}
+
+Cardinality DType::computeCardinality(TypeNode t,
+ std::vector<TypeNode>& 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<DTypeConstructor> 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<TypeNode> 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<TypeNode>& processing,
+ std::vector<TypeNode>& 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<DTypeConstructor> 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<DTypeConstructor> 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<TypeNode> processing;
+ if (computeWellFounded(processing))
+ {
+ d_wellFounded = 1;
+ }
+ else
+ {
+ d_wellFounded = -1;
+ }
+ }
+ return d_wellFounded == 1;
+}
+
+bool DType::computeWellFounded(std::vector<TypeNode>& 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<DTypeConstructor> 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<TypeNode, Node>& cache = isValue ? d_groundValue : d_groundTerm;
+ std::map<TypeNode, Node>::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<TypeNode> 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<TypeNode>& 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<DTypeConstructor> 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<TypeNode>& 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<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >::iterator
+ itd = d_sharedSel.find(dtt);
+ if (itd != d_sharedSel.end())
+ {
+ std::map<TypeNode, std::map<unsigned, Node> >::iterator its =
+ itd->second.find(t);
+ if (its != itd->second.end())
+ {
+ std::map<unsigned, Node>::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<std::shared_ptr<DTypeConstructor> >& 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<DTypeConstructor> 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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <string>
+#include <vector>
+#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<DTypeIndexTag, size_t> 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<DTypeConsIndexTag, size_t> DTypeConsIndexAttr;
+/** Attribute true for datatype types that are finite. */
+struct DTypeFiniteTag
+{
+};
+typedef expr::Attribute<DTypeFiniteTag, bool> DTypeFiniteAttr;
+/** Attribute true when we have computed whether a datatype type is finite */
+struct DTypeFiniteComputedTag
+{
+};
+typedef expr::Attribute<DTypeFiniteComputedTag, bool> DTypeFiniteComputedAttr;
+/**
+ * Attribute true for datatype types that are interpreted as finite (see
+ * TypeNode::isInterpretedFinite).
+ */
+struct DTypeUFiniteTag
+{
+};
+typedef expr::Attribute<DTypeUFiniteTag, bool> DTypeUFiniteAttr;
+/**
+ * Attribute true when we have computed whether a datatype type is interpreted
+ * as finite.
+ */
+struct DTypeUFiniteComputedTag
+{
+};
+typedef expr::Attribute<DTypeUFiniteComputedTag, bool> 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<TypeNode>& 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<DTypeConstructor> 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<TypeNode> 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<TypeNode>& 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<std::shared_ptr<DTypeConstructor> >& 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<std::string, TypeNode>& resolutions,
+ const std::vector<TypeNode>& placeholders,
+ const std::vector<TypeNode>& replacements,
+ const std::vector<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& paramReplacements);
+
+ /** compute the cardinality of this datatype */
+ Cardinality computeCardinality(TypeNode t,
+ std::vector<TypeNode>& processing) const;
+ /** compute whether this datatype is a recursive singleton */
+ bool computeCardinalityRecSingleton(TypeNode t,
+ std::vector<TypeNode>& processing,
+ std::vector<TypeNode>& u_assume) const;
+ /** compute whether this datatype is well-founded */
+ bool computeWellFounded(std::vector<TypeNode>& 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<TypeNode>& 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<TypeNode> 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<std::shared_ptr<DTypeConstructor> > 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<TypeNode, int> 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<TypeNode, std::vector<TypeNode> > 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<TypeNode, Node> d_groundTerm;
+ /** cache of ground values for this datatype */
+ mutable std::map<TypeNode, Node> d_groundValue;
+ /** cache of shared selectors for this datatype */
+ mutable std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >
+ 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<std::string>()(dt.getName());
+ }
+ size_t operator()(const DType* dt) const
+ {
+ return std::hash<std::string>()(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
--- /dev/null
+/********************* */
+/*! \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<DTypeSelector> a =
+ std::make_shared<DTypeSelector>(selectorName, type);
+ addArg(a);
+}
+
+void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> 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<TypeNode> subst;
+ m.getMatches(subst);
+ std::vector<TypeNode> params = dt.getParameters();
+ return d_constructor.getType().substitute(
+ params.begin(), params.end(), subst.begin(), subst.end());
+}
+
+const std::vector<std::shared_ptr<DTypeSelector> >& 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<TypeNode> instTypes;
+ std::vector<TypeNode> 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<TypeNode> instTypes;
+ std::vector<TypeNode> 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<Node, unsigned>::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<int>(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<TypeNode>& processing) const
+{
+ Cardinality c = 1;
+ std::vector<TypeNode> instTypes;
+ std::vector<TypeNode> 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<TypeNode>& 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<TypeNode>& processing,
+ std::map<TypeNode, Node>& gt,
+ bool isValue) const
+{
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> groundTerms;
+ groundTerms.push_back(getConstructor());
+
+ // for each selector, get a ground term
+ std::vector<TypeNode> instTypes;
+ std::vector<TypeNode> 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<TypeNode, Node>::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<TypeNode, unsigned> 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<std::string, TypeNode>& resolutions,
+ const std::vector<TypeNode>& placeholders,
+ const std::vector<TypeNode>& replacements,
+ const std::vector<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& 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<TypeNode> argTypes;
+ for (std::shared_ptr<DTypeSelector> 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<std::string, TypeNode>::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<DTypeSelector> sel : d_args)
+ {
+ sel->d_constructor = d_constructor;
+ }
+ Assert(isResolved());
+ return true;
+}
+
+TypeNode DTypeConstructor::doParametricSubstitution(
+ TypeNode range,
+ const std::vector<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& paramReplacements)
+{
+ if (range.getNumChildren() == 0)
+ {
+ return range;
+ }
+ std::vector<TypeNode> origChildren;
+ std::vector<TypeNode> 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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <string>
+#include <vector>
+#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<DTypeSelector> 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<std::shared_ptr<DTypeSelector> >& 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<std::string, TypeNode>& resolutions,
+ const std::vector<TypeNode>& placeholders,
+ const std::vector<TypeNode>& replacements,
+ const std::vector<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& 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<TypeNode>& paramTypes,
+ const std::vector<TypeNode>& paramReplacements);
+
+ /** compute the cardinality of this datatype */
+ Cardinality computeCardinality(TypeNode t,
+ std::vector<TypeNode>& processing) const;
+ /** compute whether this datatype is well-founded */
+ bool computeWellFounded(std::vector<TypeNode>& 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<TypeNode>& processing,
+ std::map<TypeNode, Node>& 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<std::shared_ptr<DTypeSelector> > 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<TypeNode, std::vector<Node> > d_sharedSelectors;
+ /** for each type, a cache mapping from shared selectors to
+ * its argument index for this constructor.
+ */
+ mutable std::map<TypeNode, std::map<Node, unsigned> > 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<std::string>()(dtc.getName());
+ }
+ size_t operator()(const DTypeConstructor* dtc) const
+ {
+ return std::hash<std::string>()(dtc->getName());
+ }
+}; /* struct DTypeConstructorHashFunction */
+
+std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor);
+
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <string>
+#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
#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"
d_rt_cache.d_children.clear();
d_rt_cache.d_data = dummy;
+ // TODO: switch to DType
for (std::vector<Datatype*>::iterator
datatype_iter = d_ownedDatatypes.begin(),
datatype_end = d_ownedDatatypes.end();
}
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());
class StatisticsRegistry;
class ResourceManager;
+class DType;
+
namespace expr {
namespace attr {
class AttributeUniqueId;
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);
return ss.str();
}
+const DType& TypeNode::getDType() const
+{
+ if (getKind() == kind::DATATYPE_TYPE)
+ {
+ DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+ return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex());
+ }
+ Assert(getKind() == kind::PARAMETRIC_DATATYPE);
+ return (*this)[0].getDType();
+}
+
}/* CVC4 namespace */
namespace CVC4 {
class NodeManager;
+class DType;
namespace expr {
class NodeValue;
/** 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;
projects / cvc5.git / commitdiff