From: Andrew Reynolds Date: Tue, 3 May 2022 03:03:51 +0000 (-0500) Subject: Simplify representation of datatypes at the TypeNode level (#8702) X-Git-Tag: cvc5-1.0.1~184 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f2b2170adbf22f1541ed5be0eebd3fde7b80ba3;p=cvc5.git Simplify representation of datatypes at the TypeNode level (#8702) 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. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 32da6002e..f48536537 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -86,8 +86,6 @@ libcvc5_add_sources( type_matcher.h type_node.cpp type_node.h - datatype_index.h - datatype_index.cpp dtype.h dtype.cpp dtype_cons.h diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp deleted file mode 100644 index 36a11c347..000000000 --- a/src/expr/datatype_index.cpp +++ /dev/null @@ -1,38 +0,0 @@ -/****************************************************************************** - * 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 -#include -#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 diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h deleted file mode 100644 index 773378627..000000000 --- a/src/expr/datatype_index.h +++ /dev/null @@ -1,70 +0,0 @@ -/****************************************************************************** - * 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 - -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 */ diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index b913ec51c..17920ae46 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -991,10 +991,4 @@ void DType::toStream(std::ostream& out) const 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 diff --git a/src/expr/dtype.h b/src/expr/dtype.h index edc6f0f83..f0f644b94 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -650,43 +650,6 @@ struct DTypeHashFunction } }; /* 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 diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index eb284b304..25043f146 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -36,6 +36,9 @@ namespace attr { struct TupleDatatypeTag { }; + struct DatatypeIndexTag + { + }; } // namespace attr typedef Attribute VarNameAttr; @@ -51,5 +54,8 @@ using UnresolvedDatatypeAttr = using TupleDatatypeAttr = expr::Attribute; +/** Mapping datatype types to the index of their datatype in node manager */ +using DatatypeIndexAttr = Attribute; + } // namespace expr } // namespace cvc5::internal diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index dad48ba1f..0a7ef904a 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -21,7 +21,6 @@ #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" @@ -307,8 +306,8 @@ const DType& NodeManager::getDTypeFor(TypeNode tn) const Kind k = tn.getKind(); if (k == kind::DATATYPE_TYPE) { - DatatypeIndexConstant dic = tn.getConst(); - return getDTypeForIndex(dic.getIndex()); + size_t index = tn.getAttribute(DatatypeIndexAttr()); + return getDTypeForIndex(index); } else if (k == kind::TUPLE_TYPE) { @@ -321,6 +320,11 @@ const DType& NodeManager::getDTypeFor(TypeNode tn) const 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 @@ -609,15 +613,18 @@ std::vector NodeManager::mkMutualDatatypeTypesInternal( // 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(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()) { @@ -637,14 +644,13 @@ std::vector NodeManager::mkMutualDatatypeTypesInternal( } else { - TypeNode cons = mkTypeConst(DatatypeIndexConstant(index)); + TypeNode cons = typeNode; std::vector 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()) diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index e10f448b4..0ad5005ec 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -122,13 +122,13 @@ class NodeManager /** * 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; /** @@ -139,6 +139,8 @@ class NodeManager * 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); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index d0801126c..748677e64 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -16,7 +16,6 @@ #include -#include "expr/datatype_index.h" #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" #include "expr/type_properties.h" @@ -443,8 +442,7 @@ TypeNode TypeNode::instantiate(const std::vector& params) const if (k == kind::PARAMETRIC_DATATYPE) { Assert(params.size() == getNumChildren() - 1); - TypeNode cons = - nm->mkTypeConst((*this)[0].getConst()); + TypeNode cons = (*this)[0]; std::vector paramsNodes; paramsNodes.push_back(cons); for (const TypeNode& t : params) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cb2c1d083..19c67f672 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -25,7 +25,6 @@ #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" @@ -308,35 +307,6 @@ void Smt2Printer::toStream(std::ostream& out, break; } - case kind::DATATYPE_TYPE: - { - const DType& dt = (NodeManager::currentNM()->getDTypeForIndex( - n.getConst().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(); @@ -468,7 +438,9 @@ void Smt2Printer::toStream(std::ostream& out, return; } - if(n.getKind() == kind::SORT_TYPE) { + Kind k = n.getKind(); + if (k == kind::SORT_TYPE) + { string name; if(n.getNumChildren() != 0) { out << '('; @@ -485,10 +457,36 @@ void Smt2Printer::toStream(std::ostream& 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) diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 2d7a30918..dee4fe4be 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -46,12 +46,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is 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"