src/expr/metakind_template.h

   1 /*********************                                                        */
   2 /*! \file metakind_template.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andres Noetzli, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Template for the metakind header.
  13  **
  14  ** Template for the metakind header.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__KIND__METAKIND_H
  20 #define CVC4__KIND__METAKIND_H
  21
  22 #include <iosfwd>
  23
  24 #include "base/check.h"
  25 #include "expr/kind.h"
  26
  27 namespace CVC4 {
  28
  29 namespace expr {
  30   class NodeValue;
  31 }/* CVC4::expr namespace */
  32
  33 namespace kind {
  34 namespace metakind {
  35
  36 /**
  37  * Static, compile-time information about types T representing CVC4
  38  * constants:
  39  *
  40  *   typename ConstantMap<T>::OwningTheory
  41  *
  42  *     The theory in charge of constructing T when constructing Nodes
  43  *     with NodeManager::mkConst(T).
  44  *
  45  *   typename ConstantMap<T>::kind
  46  *
  47  *     The kind to use when constructing Nodes with
  48  *     NodeManager::mkConst(T).
  49  */
  50 template <class T>
  51 struct ConstantMap;
  52
  53 /**
  54  * Static, compile-time information about kinds k and what type their
  55  * corresponding CVC4 constants are:
  56  *
  57  *   typename ConstantMapReverse<k>::T
  58  *
  59  *     Constant type for kind k.
  60  */
  61 template <Kind k>
  62 struct ConstantMapReverse;
  63
  64 /**
  65  * Static, compile-time mapping from CONSTANT kinds to comparison
  66  * functors on NodeValue*.  The single element of this structure is:
  67  *
  68  *   static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
  69  *
  70  *     Compares x and y, given that they are both K-kinded (and the
  71  *     meta-kind of K is CONSTANT).  If pool == true, one of x and y
  72  *     (but not both) may be a "non-inlined" NodeValue.  If pool ==
  73  *     false, neither x nor y may be a "non-inlined" NodeValue.
  74  */
  75 template <Kind k, bool pool>
  76 struct NodeValueConstCompare {
  77   inline static bool compare(const ::CVC4::expr::NodeValue* x,
  78                              const ::CVC4::expr::NodeValue* y);
  79   inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
  80 };/* NodeValueConstCompare<k, pool> */
  81
  82 struct NodeValueCompare {
  83   template <bool pool>
  84   static bool compare(const ::CVC4::expr::NodeValue* nv1,
  85                       const ::CVC4::expr::NodeValue* nv2);
  86   static size_t constHash(const ::CVC4::expr::NodeValue* nv);
  87 };/* struct NodeValueCompare */
  88
  89 /**
  90  * "metakinds" represent the "kinds" of kinds at the meta-level.
  91  * "metakind" is an ugly name but it's not used by client code, just
  92  * by the expr package, and the intent here is to keep it from
  93  * polluting the kind namespace.  For more documentation on what these
  94  * mean, see src/theory/builtin/kinds.
  95  */
  96 enum MetaKind_t {
  97   INVALID = -1, /**< special node non-kinds like NULL_EXPR or LAST_KIND */
  98   VARIABLE, /**< special node kinds: no operator */
  99   OPERATOR, /**< operators that get "inlined" */
 100   PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */
 101   CONSTANT, /**< constants */
 102   NULLARY_OPERATOR /**< nullary operator */
 103 };/* enum MetaKind_t */
 104
 105 }/* CVC4::kind::metakind namespace */
 106
 107 // import MetaKind into the "CVC4::kind" namespace but keep the
 108 // individual MetaKind constants under kind::metakind::
 109 typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
 110
 111 /**
 112  * Get the metakind for a particular kind.
 113  */
 114 MetaKind metaKindOf(Kind k);
 115 }/* CVC4::kind namespace */
 116
 117 namespace expr {
 118
 119 // Comparison predicate
 120 struct NodeValuePoolEq {
 121   inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
 122     return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
 123   }
 124 };
 125
 126 }/* CVC4::expr namespace */
 127 }/* CVC4 namespace */
 128
 129 #include "expr/node_value.h"
 130
 131 #endif /* CVC4__KIND__METAKIND_H */
 132
 133 ${metakind_includes}
 134
 135 #ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 136
 137 namespace CVC4 {
 138
 139 namespace expr {
 140 ${metakind_getConst_decls}
 141 }/* CVC4::expr namespace */
 142
 143 namespace kind {
 144 namespace metakind {
 145
 146 template <Kind k, bool pool>
 147 inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x,
 148                                                     const ::CVC4::expr::NodeValue* y) {
 149   typedef typename ConstantMapReverse<k>::T T;
 150   if(pool) {
 151     if(x->d_nchildren == 1) {
 152       Assert(y->d_nchildren == 0);
 153       return compare(y, x);
 154     } else if(y->d_nchildren == 1) {
 155       Assert(x->d_nchildren == 0);
 156       return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
 157     }
 158   }
 159
 160   Assert(x->d_nchildren == 0);
 161   Assert(y->d_nchildren == 0);
 162   return x->getConst<T>() == y->getConst<T>();
 163 }
 164
 165 template <Kind k, bool pool>
 166 inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) {
 167   typedef typename ConstantMapReverse<k>::T T;
 168   return nv->getConst<T>().hash();
 169 }
 170
 171 ${metakind_constantMaps_decls}
 172
 173 struct NodeValueConstPrinter {
 174   static void toStream(std::ostream& out,
 175                               const ::CVC4::expr::NodeValue* nv);
 176   static void toStream(std::ostream& out, TNode n);
 177 };
 178
 179 /**
 180  * Cleanup to be performed when a NodeValue zombie is collected, and
 181  * it has CONSTANT metakind.  This calls the destructor for the underlying
 182  * C++ type representing the constant value.  See
 183  * NodeManager::reclaimZombies() for more information.
 184  *
 185  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
 186  * kind of cleanup.
 187  */
 188 void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
 189
 190 unsigned getLowerBoundForKind(::CVC4::Kind k);
 191 unsigned getUpperBoundForKind(::CVC4::Kind k);
 192
 193 }/* CVC4::kind::metakind namespace */
 194
 195 /**
 196  * Map a kind of the operator to the kind of the enclosing expression. For
 197  * example, since the kind of functions is just VARIABLE, it should map
 198  * VARIABLE to APPLY_UF.
 199  */
 200 Kind operatorToKind(::CVC4::expr::NodeValue* nv);
 201
 202 }/* CVC4::kind namespace */
 203
 204 #line 205 "${template}"
 205
 206 }/* CVC4 namespace */
 207
 208 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */