src/expr/kind_template.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andres Noetzli, Morgan Deters, Aina Niemetz
   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  * Template for the Node kind header.
  14  */
  15
  16 #include "cvc5_public.h"
  17
  18 #ifndef CVC5__KIND_H
  19 #define CVC5__KIND_H
  20
  21 #include <iosfwd>
  22
  23 #include "base/exception.h"
  24 #include "theory/theory_id.h"
  25
  26 namespace cvc5 {
  27 namespace kind {
  28
  29 enum Kind_t
  30 {
  31   UNDEFINED_KIND = -1, /**< undefined */
  32   NULL_EXPR,           /**< Null kind */
  33   // clang-format off
  34   ${kind_decls} LAST_KIND /**< marks the upper-bound of this enumeration */
  35   // clang-format on
  36
  37 }; /* enum Kind_t */
  38
  39 }  // namespace kind
  40
  41 // import Kind into the "cvc5" namespace but keep the individual kind
  42 // constants under kind::
  43 typedef ::cvc5::kind::Kind_t Kind;
  44
  45 namespace kind {
  46
  47 /**
  48  * Converts an kind to a string. Note: This function is also used in
  49  * `safe_print()`. Changing this functions name or signature will result in
  50  * `safe_print()` printing "<unsupported>" instead of the proper strings for
  51  * the enum values.
  52  *
  53  * @param k The kind
  54  * @return The name of the kind
  55  */
  56 const char* toString(cvc5::Kind k);
  57
  58 /**
  59  * Writes a kind name to a stream.
  60  *
  61  * @param out The stream to write to
  62  * @param k The kind to write to the stream
  63  * @return The stream
  64  */
  65 std::ostream& operator<<(std::ostream&, cvc5::Kind);
  66
  67 /** Returns true if the given kind is associative. This is used by ExprManager to
  68  * decide whether it's safe to modify big expressions by changing the grouping of
  69  * the arguments. */
  70 /* TODO: This could be generated. */
  71 bool isAssociative(::cvc5::Kind k);
  72 std::string kindToString(::cvc5::Kind k);
  73
  74 struct KindHashFunction
  75 {
  76   inline size_t operator()(::cvc5::Kind k) const { return k; }
  77 }; /* struct KindHashFunction */
  78
  79 }  // namespace kind
  80
  81 /**
  82  * The enumeration for the built-in atomic types.
  83  */
  84 enum TypeConstant
  85 {
  86   // clang-format off
  87   ${type_constant_list} LAST_TYPE
  88   // clang-format on
  89 }; /* enum TypeConstant */
  90
  91 /**
  92  * We hash the constants with their values.
  93  */
  94 struct TypeConstantHashFunction
  95 {
  96   inline size_t operator()(TypeConstant tc) const { return tc; }
  97 }; /* struct TypeConstantHashFunction */
  98
  99 const char* toString(TypeConstant tc);
 100 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 101
 102 namespace theory {
 103
 104 ::cvc5::theory::TheoryId kindToTheoryId(::cvc5::Kind k);
 105 ::cvc5::theory::TheoryId typeConstantToTheoryId(
 106     ::cvc5::TypeConstant typeConstant);
 107
 108 }  // namespace theory
 109 }  // namespace cvc5
 110
 111 #endif /* CVC5__KIND_H */