They previously were TYPE_CONSTANTs hashed by the index of their DType in the NodeManager. Now they are variables having an attribute that is their index.
This makes datatypes more analogous to uninterpreted sorts, and eliminates the need for an auxiliary DatatypeIndexConstant class.
type_matcher.h
type_node.cpp
type_node.h
- datatype_index.h
- datatype_index.cpp
dtype.h
dtype.cpp
dtype_cons.h
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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.
- * ****************************************************************************
- *
- * A class representing an index to a datatype living in NodeManager.
- */
-#include "expr/datatype_index.h"
-
-#include <sstream>
-#include <string>
-#include "util/hash.h"
-#include "util/integer.h"
-
-using namespace std;
-
-namespace cvc5::internal {
-
-DatatypeIndexConstant::DatatypeIndexConstant(uint32_t index) : d_index(index) {}
-std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic)
-{
- return out << "index_" << dic.getIndex();
-}
-
-size_t DatatypeIndexConstantHashFunction::operator()(
- const DatatypeIndexConstant& dic) const
-{
- return IntegerHashFunction()(dic.getIndex());
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Tim King, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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.
- * ****************************************************************************
- *
- * A class representing an index to a datatype living in NodeManager.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__DATATYPE_INDEX_H
-#define CVC5__DATATYPE_INDEX_H
-
-#include <iosfwd>
-
-namespace cvc5::internal {
-
-/* stores an index to Datatype residing in NodeManager */
-class DatatypeIndexConstant
-{
- public:
- DatatypeIndexConstant(unsigned index);
-
- unsigned getIndex() const { return d_index; }
- bool operator==(const DatatypeIndexConstant& uc) const
- {
- return d_index == uc.d_index;
- }
- bool operator!=(const DatatypeIndexConstant& uc) const
- {
- return !(*this == uc);
- }
- bool operator<(const DatatypeIndexConstant& uc) const
- {
- return d_index < uc.d_index;
- }
- bool operator<=(const DatatypeIndexConstant& uc) const
- {
- return d_index <= uc.d_index;
- }
- bool operator>(const DatatypeIndexConstant& uc) const
- {
- return !(*this <= uc);
- }
- bool operator>=(const DatatypeIndexConstant& uc) const
- {
- return !(*this < uc);
- }
-
- private:
- const unsigned d_index;
-}; /* class DatatypeIndexConstant */
-
-std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic);
-
-struct DatatypeIndexConstantHashFunction
-{
- size_t operator()(const DatatypeIndexConstant& dic) const;
-}; /* struct DatatypeIndexConstantHashFunction */
-
-} // namespace cvc5::internal
-
-#endif /* CVC5__DATATYPE_H */
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 cvc5::internal
}
}; /* 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 cvc5::internal
struct TupleDatatypeTag
{
};
+ struct DatatypeIndexTag
+ {
+ };
} // namespace attr
typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
using TupleDatatypeAttr =
expr::Attribute<expr::attr::TupleDatatypeTag, TypeNode>;
+/** Mapping datatype types to the index of their datatype in node manager */
+using DatatypeIndexAttr = Attribute<attr::DatatypeIndexTag, uint64_t>;
+
} // namespace expr
} // namespace cvc5::internal
#include "base/listener.h"
#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
-#include "expr/datatype_index.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/metakind.h"
Kind k = tn.getKind();
if (k == kind::DATATYPE_TYPE)
{
- DatatypeIndexConstant dic = tn.getConst<DatatypeIndexConstant>();
- return getDTypeForIndex(dic.getIndex());
+ size_t index = tn.getAttribute(DatatypeIndexAttr());
+ return getDTypeForIndex(index);
}
else if (k == kind::TUPLE_TYPE)
{
return getDTypeFor(tn[0]);
}
+const DType& NodeManager::getDTypeFor(Node n) const
+{
+ return getDTypeFor(TypeNode(n.d_nv));
+}
+
const DType& NodeManager::getDTypeForIndex(size_t index) const
{
// if this assertion fails, it is likely due to not managing datatypes
// simple self- and mutual-recursion, for example in the definition
// "nat = succ(pred:nat) | zero", a named resolution can handle the
// pred selector.
+ DatatypeIndexAttr dia;
for (const DType& dt : datatypes)
{
uint32_t index = d_dtypes.size();
d_dtypes.push_back(std::unique_ptr<DType>(new DType(dt)));
DType* dtp = d_dtypes.back().get();
- TypeNode typeNode;
+
+ NodeBuilder dtnb(this, kind::DATATYPE_TYPE);
+ TypeNode typeNode = dtnb.constructTypeNode();
+ typeNode.setAttribute(dia, index);
if (dtp->getNumParameters() == 0)
{
- typeNode = mkTypeConst(DatatypeIndexConstant(index));
// if the datatype is a tuple, the type will be (TUPLE_TYPE ...)
if (dt.isTuple())
{
}
else
{
- TypeNode cons = mkTypeConst(DatatypeIndexConstant(index));
+ TypeNode cons = typeNode;
std::vector<TypeNode> params;
params.push_back(cons);
for (uint32_t ip = 0; ip < dtp->getNumParameters(); ++ip)
{
params.push_back(dtp->getParameter(ip));
}
-
typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
}
if (nameResolutions.find(dtp->getName()) != nameResolutions.end())
/**
* Return the datatype at the given index owned by this class. Type nodes are
- * associated with datatypes through the DatatypeIndexConstant class. The
+ * associated with datatypes through the DatatypeIndexAttr attribute. The
* argument index is intended to be a value taken from that class.
*
* Type nodes must access their DTypes through a level of indirection to
* prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
- * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
- * which is used as an index to retrieve the DType via this call.
+ * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexAttr
+ * attribute which is used as an index to retrieve the DType via this call.
*/
const DType& getDTypeForIndex(size_t index) const;
/**
* this method on it.
*/
const DType& getDTypeFor(TypeNode tn) const;
+ /** Same as above, for node */
+ const DType& getDTypeFor(Node n) const;
/** get the canonical bound variable list for function type tn */
Node getBoundVarListForFunctionType(TypeNode tn);
#include <vector>
-#include "expr/datatype_index.h"
#include "expr/dtype_cons.h"
#include "expr/node_manager_attributes.h"
#include "expr/type_properties.h"
if (k == kind::PARAMETRIC_DATATYPE)
{
Assert(params.size() == getNumChildren() - 1);
- TypeNode cons =
- nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>());
+ TypeNode cons = (*this)[0];
std::vector<TypeNode> paramsNodes;
paramsNodes.push_back(cons);
for (const TypeNode& t : params)
#include "expr/array_store_all.h"
#include "expr/ascription_type.h"
#include "expr/cardinality_constraint.h"
-#include "expr/datatype_index.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/emptybag.h"
break;
}
- case kind::DATATYPE_TYPE:
- {
- const DType& dt = (NodeManager::currentNM()->getDTypeForIndex(
- n.getConst<DatatypeIndexConstant>().getIndex()));
- if (dt.isTuple())
- {
- unsigned int nargs = dt[0].getNumArgs();
- if (nargs == 0)
- {
- out << "Tuple";
- }
- else
- {
- out << "(Tuple";
- for (unsigned int i = 0; i < nargs; i++)
- {
- out << " ";
- toStreamType(out, dt[0][i].getRangeType());
- }
- out << ")";
- }
- }
- else
- {
- out << cvc5::internal::quoteSymbol(dt.getName());
- }
- break;
- }
-
case kind::UNINTERPRETED_SORT_VALUE:
{
const UninterpretedSortValue& av = n.getConst<UninterpretedSortValue>();
return;
}
- if(n.getKind() == kind::SORT_TYPE) {
+ Kind k = n.getKind();
+ if (k == kind::SORT_TYPE)
+ {
string name;
if(n.getNumChildren() != 0) {
out << '(';
}
return;
}
+ else if (k == kind::DATATYPE_TYPE)
+ {
+ const DType& dt = NodeManager::currentNM()->getDTypeFor(n);
+ if (dt.isTuple())
+ {
+ unsigned int nargs = dt[0].getNumArgs();
+ if (nargs == 0)
+ {
+ out << "Tuple";
+ }
+ else
+ {
+ out << "(Tuple";
+ for (unsigned int i = 0; i < nargs; i++)
+ {
+ out << " ";
+ toStreamType(out, dt[0][i].getRangeType());
+ }
+ out << ")";
+ }
+ }
+ else
+ {
+ out << cvc5::internal::quoteSymbol(dt.getName());
+ }
+ return;
+ }
// determine if we are printing out a type ascription, store the argument of
// the type ascription into type_asc_arg.
- Kind k = n.getKind();
Node type_asc_arg;
TypeNode force_nt;
if (k == kind::APPLY_TYPE_ASCRIPTION)
parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with"
-constant DATATYPE_TYPE \
- class \
- DatatypeIndexConstant \
- "::cvc5::internal::DatatypeIndexConstantHashFunction" \
- "expr/datatype_index.h" \
- "a datatype type index"
+variable DATATYPE_TYPE
cardinality DATATYPE_TYPE \
"%TYPE%.getDType().getCardinality(%TYPE%)" \
"expr/dtype.h"
projects / cvc5.git / commitdiff