Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/dtype_cons.h	Lines:	2	2	100.0 %
Date:	2021-09-05	Branches:	8	16	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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 a datatype definition.
 */

#include "cvc5_private.h"

#ifndef CVC5__EXPR__DTYPE_CONS_H
#define CVC5__EXPR__DTYPE_CONS_H

#include <map>
#include <string>
#include <vector>
#include "expr/dtype_selector.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "util/cardinality_class.h"

namespace cvc5 {

/**
 * 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 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);
  /**
   * Add a self-referential (i.e., a data field) of the given name
   * to this Datatype constructor that refers to the enclosing
   * Datatype.  For example, using the familiar "nat" Datatype, to
   * create the "pred" field for "succ" constructor, one uses
   * succ::addArgSelf("pred")---the actual Type
   * cannot be passed because the Datatype is still under
   * construction.  Selector names need not be unique; they are for
   * convenience and pretty-printing only.
   *
   * This is a special case of
   * DTypeConstructor::addArg(std::string).
   */
  void addArgSelf(std::string selectorName);

  /** Get the name of this constructor. */
  const 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 the cardinality class, which indicates if the type has cardinality
   * one, is finite or infinite, possibly dependent on uninterpreted sorts being
   * finite.
   *
   * Note that the cardinality of a constructor is equivalent to asking how
   * many applications of this constructor exist.
   */
  CardinalityClass getCardinalityClass(TypeNode t) const;

  /**
   * Has finite external argument type. This returns true if this constructor
   * has an argument type that is not a datatype and is interpreted as a
   * finite type. This function can only be called for resolved constructors.
   *
   */
  bool hasFiniteExternalArgType(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;
  /** get selector index for name
   *
   * Returns the index of selector with the given name, or -1 if it
   * does not exist.
   */
  int getSelectorIndexForName(const std::string& name) 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 cardinality info, returns a pair where its first component is
   * an identifier indicating the cardinality type of this constructor for
   * type t, and a Boolean indicating whether the constructor has any arguments
   * that have finite external type.
   */
  std::pair<CardinalityClass, bool> computeCardinalityInfo(TypeNode t) 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;
  /**  A cache for computeCardinalityInfo. */
  mutable std::map<TypeNode, std::pair<CardinalityClass, bool> > d_cardInfo;
}; /* 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 cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Tim King
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* A class representing a datatype definition.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__EXPR__DTYPE_CONS_H
19		#define CVC5__EXPR__DTYPE_CONS_H
20
21		#include <map>
22		#include <string>
23		#include <vector>
24		#include "expr/dtype_selector.h"
25		#include "expr/node.h"
26		#include "expr/type_node.h"
27		#include "util/cardinality_class.h"
28
29		namespace cvc5 {
30
31		/**
32		* The Node-level representation of a constructor for a datatype, which
33		* currently resides in the Expr-level DatatypeConstructor class
34		* (expr/datatype.h).
35		*/
36	6416	class DTypeConstructor
37		{
38		friend class DType;
39
40		public:
41		/**
42		* Create a new datatype constructor with the given name for the
43		* constructor and the same name (prefixed with "is_") for the
44		* tester. The actual constructor and tester (meaning, the Nodes
45		* representing operators for these entities) aren't created until
46		* resolution time.
47		*
48		* weight is the value that this constructor carries when computing size
49		* for SyGuS. For example, if A, B, C have weights 0, 1, and 3 respectively,
50		* then C( B( A() ), B( A() ) ) has size 5.
51		*/
52		DTypeConstructor(std::string name, unsigned weight = 1);
53
54	22018	~DTypeConstructor() {}
55		/**
56		* Add an argument (i.e., a data field) of the given name and type
57		* to this constructor. Selector names need not be unique;
58		* they are for convenience and pretty-printing only.
59		*/
60		void addArg(std::string selectorName, TypeNode selectorType);
61		/**
62		* Add an argument, given a pointer to a selector object.
63		*/
64		void addArg(std::shared_ptr<DTypeSelector> a);
65		/**
66		* Add a self-referential (i.e., a data field) of the given name
67		* to this Datatype constructor that refers to the enclosing
68		* Datatype. For example, using the familiar "nat" Datatype, to
69		* create the "pred" field for "succ" constructor, one uses
70		* succ::addArgSelf("pred")---the actual Type
71		* cannot be passed because the Datatype is still under
72		* construction. Selector names need not be unique; they are for
73		* convenience and pretty-printing only.
74		*
75		* This is a special case of
76		* DTypeConstructor::addArg(std::string).
77		*/
78		void addArgSelf(std::string selectorName);
79
80		/** Get the name of this constructor. */
81		const std::string& getName() const;
82
83		/**
84		* Get the constructor operator of this constructor. The
85		* DType must be resolved.
86		*/
87		Node getConstructor() const;
88
89		/**
90		* Get the tester operator of this constructor. The
91		* DType must be resolved.
92		*/
93		Node getTester() const;
94		//-------------------------------------- sygus
95		/** set sygus
96		*
97		* Set that this constructor is a sygus datatype constructor that encodes
98		* operator op.
99		*/
100		void setSygus(Node op);
101		/** get sygus op
102		*
103		* This method returns the operator or term that this constructor represents
104		* in the sygus encoding. This may be a builtin operator, defined function,
105		* variable, or constant that this constructor encodes in this deep embedding.
106		*/
107		Node getSygusOp() const;
108		/** is this a sygus identity function?
109		*
110		* This returns true if the sygus operator of this datatype constructor is
111		* of the form (lambda (x) x).
112		*/
113		bool isSygusIdFunc() const;
114		/** get weight
115		*
116		* Get the weight of this constructor. This value is used when computing the
117		* size of datatype terms that involve this constructor.
118		*/
119		unsigned getWeight() const;
120		//-------------------------------------- end sygus
121
122		/**
123		* Get the number of arguments (so far) of this DType constructor.
124		*/
125		size_t getNumArgs() const;
126		/**
127		* Get the list of arguments to this constructor.
128		*/
129		const std::vector<std::shared_ptr<DTypeSelector> >& getArgs() const;
130		/**
131		* Get the specialized constructor type for a parametric
132		* constructor; this call is only permitted after resolution.
133		* Given a (concrete) returnType, the constructor's concrete
134		* type in this parametric datatype is returned.
135		*
136		* For instance, if the datatype is list[T], with constructor
137		* "cons[T]" of type "T -> list[T] -> list[T]", then calling
138		* this function with "list[int]" will return the concrete
139		* "cons" constructor type for lists of int---namely,
140		* "int -> list[int] -> list[int]".
141		*/
142		TypeNode getSpecializedConstructorType(TypeNode returnType) const;
143
144		/**
145		* Return the cardinality of this constructor (the product of the
146		* cardinalities of its arguments).
147		*/
148		Cardinality getCardinality(TypeNode t) const;
149
150		/**
151		* Return the cardinality class, which indicates if the type has cardinality
152		* one, is finite or infinite, possibly dependent on uninterpreted sorts being
153		* finite.
154		*
155		* Note that the cardinality of a constructor is equivalent to asking how
156		* many applications of this constructor exist.
157		*/
158		CardinalityClass getCardinalityClass(TypeNode t) const;
159
160		/**
161		* Has finite external argument type. This returns true if this constructor
162		* has an argument type that is not a datatype and is interpreted as a
163		* finite type. This function can only be called for resolved constructors.
164		*
165		*/
166		bool hasFiniteExternalArgType(TypeNode t) const;
167
168		/**
169		* Returns true iff this constructor has already been
170		* resolved.
171		*/
172		bool isResolved() const;
173
174		/** Get the ith DTypeConstructor arg. */
175		const DTypeSelector& operator[](size_t index) const;
176
177		/**
178		* Get argument type. Returns the return type of the i^th selector of this
179		* constructor.
180		*/
181		TypeNode getArgType(size_t i) const;
182
183		/** get selector internal
184		*
185		* This gets the selector for the index^th argument
186		* of this constructor. The type dtt is the datatype
187		* type whose datatype is the owner of this constructor,
188		* where this type may be an instantiated parametric datatype.
189		*
190		* If shared selectors are enabled,
191		* this returns a shared (constructor-agnotic) selector, which
192		* in the terminology of "DTypes with Shared Selectors", is:
193		* sel_{dtt}^{T,atos(T,C,index)}
194		* where C is this constructor, and T is the type
195		* of the index^th field of this constructor.
196		* The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of
197		* type T of constructor term t if one exists, or is
198		* unconstrained otherwise.
199		*/
200		Node getSelectorInternal(TypeNode dtt, size_t index) const;
201
202		/** get selector index internal
203		*
204		* This gets the argument number of this constructor
205		* that the selector sel accesses. It returns -1 if the
206		* selector sel is not a selector for this constructor.
207		*
208		* In the terminology of "DTypes with Shared Selectors",
209		* if sel is sel_{dtt}^{T,index} for some (T, index), where
210		* dtt is the datatype type whose datatype is the owner
211		* of this constructor, then this method returns
212		* stoa(T,C,index)
213		*/
214		int getSelectorIndexInternal(Node sel) const;
215		/** get selector index for name
216		*
217		* Returns the index of selector with the given name, or -1 if it
218		* does not exist.
219		*/
220		int getSelectorIndexForName(const std::string& name) const;
221
222		/** involves external type
223		*
224		* Get whether this constructor has a subfield
225		* in any constructor that is not a datatype type.
226		*/
227		bool involvesExternalType() const;
228		/** involves uninterpreted type
229		*
230		* Get whether this constructor has a subfield
231		* in any constructor that is an uninterpreted type.
232		*/
233		bool involvesUninterpretedType() const;
234		/** prints this datatype constructor to stream */
235		void toStream(std::ostream& out) const;
236
237		private:
238		/** resolve
239		*
240		* This resolves (initializes) the constructor. For details
241		* on how datatypes and their constructors are resolved, see
242		* documentation for DType::resolve.
243		*/
244		bool resolve(TypeNode self,
245		const std::map<std::string, TypeNode>& resolutions,
246		const std::vector<TypeNode>& placeholders,
247		const std::vector<TypeNode>& replacements,
248		const std::vector<TypeNode>& paramTypes,
249		const std::vector<TypeNode>& paramReplacements,
250		size_t cindex);
251
252		/** Helper function for resolving parametric datatypes.
253		*
254		* This replaces instances of the TypeNode produced for unresolved
255		* parametric datatypes, with the corresponding resolved TypeNode. For
256		* example, take the parametric definition of a list,
257		* list[T] = cons(car : T, cdr : list[T]) \| null.
258		* If "range" is the unresolved parametric datatype:
259		* DATATYPE list =
260		* cons(car: SORT_TAG_1,
261		* cdr: SORT_TAG_2(SORT_TAG_1)) \| null END;,
262		* this function will return the resolved type:
263		* DATATYPE list =
264		* cons(car: SORT_TAG_1,
265		* cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) \| null END;
266		*/
267		TypeNode doParametricSubstitution(
268		TypeNode range,
269		const std::vector<TypeNode>& paramTypes,
270		const std::vector<TypeNode>& paramReplacements);
271
272		/** compute the cardinality of this datatype */
273		Cardinality computeCardinality(TypeNode t,
274		std::vector<TypeNode>& processing) const;
275		/** compute whether this datatype is well-founded */
276		bool computeWellFounded(std::vector<TypeNode>& processing) const;
277		/** compute ground term
278		*
279		* This method is used for constructing a term that is an application
280		* of this constructor whose type is t.
281		*
282		* The argument processing is the set of datatype types we are currently
283		* traversing. This is used to avoid infinite loops.
284		*
285		* The argument gt caches the ground terms we have computed so far.
286		*
287		* The argument isValue is whether we are constructing a constant value. If
288		* this flag is false, we are constructing a canonical ground term that is
289		* not necessarily constant.
290		*/
291		Node computeGroundTerm(TypeNode t,
292		std::vector<TypeNode>& processing,
293		std::map<TypeNode, Node>& gt,
294		bool isValue) const;
295		/**
296		* Compute cardinality info, returns a pair where its first component is
297		* an identifier indicating the cardinality type of this constructor for
298		* type t, and a Boolean indicating whether the constructor has any arguments
299		* that have finite external type.
300		*/
301		std::pair<CardinalityClass, bool> computeCardinalityInfo(TypeNode t) const;
302		/** compute shared selectors
303		* This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
304		*/
305		void computeSharedSelectors(TypeNode domainType) const;
306		/** the name of the constructor */
307		std::string d_name;
308		/** the name of the tester */
309		std::string d_testerName;
310		/** the constructor expression */
311		Node d_constructor;
312		/** the tester for this constructor */
313		Node d_tester;
314		/** the arguments of this constructor */
315		std::vector<std::shared_ptr<DTypeSelector> > d_args;
316		/** sygus operator */
317		Node d_sygusOp;
318		/** weight */
319		unsigned d_weight;
320		/** shared selectors for each type
321		*
322		* This stores the shared (constructor-agnotic)
323		* selectors that access the fields of this datatype.
324		* In the terminology of "DTypes with Shared Selectors",
325		* this stores:
326		* sel_{dtt}^{T1,atos(T1,C,1)}, ...,
327		* sel_{dtt}^{Tn,atos(Tn,C,n)}
328		* where C is this constructor, which has type
329		* T1 x ... x Tn -> dtt above.
330		* We store this information for (possibly multiple)
331		* datatype types dtt, since this constructor may be
332		* for a parametric datatype, where dtt is an instantiated
333		* parametric datatype.
334		*/
335		mutable std::map<TypeNode, std::vector<Node> > d_sharedSelectors;
336		/** for each type, a cache mapping from shared selectors to
337		* its argument index for this constructor.
338		*/
339		mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
340		/** A cache for computeCardinalityInfo. */
341		mutable std::map<TypeNode, std::pair<CardinalityClass, bool> > d_cardInfo;
342		}; /* class DTypeConstructor */
343
344		/**
345		* A hash function for DTypeConstructors. Needed to store them in hash sets
346		* and hash maps.
347		*/
348		struct DTypeConstructorHashFunction
349		{
350		size_t operator()(const DTypeConstructor& dtc) const
351		{
352		return std::hash<std::string>()(dtc.getName());
353		}
354		size_t operator()(const DTypeConstructor* dtc) const
355		{
356		return std::hash<std::string>()(dtc->getName());
357		}
358		}; /* struct DTypeConstructorHashFunction */
359
360		std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor);
361
362		} // namespace cvc5
363
364		#endif