src/expr/kind_template.h

   1 /*********************                                                        */
   2 /*! \file kind_template.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Template for the Node kind header.
  15  **
  16  ** Template for the Node kind header.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__KIND_H
  22 #define __CVC4__KIND_H
  23
  24 #include <iostream>
  25 #include <sstream>
  26
  27 #include "util/Assert.h"
  28
  29 namespace CVC4 {
  30 namespace kind {
  31
  32 enum Kind_t {
  33   UNDEFINED_KIND = -1, /**< undefined */
  34   NULL_EXPR, /**< Null kind */
  35 ${kind_decls}
  36   LAST_KIND /**< marks the upper-bound of this enumeration */
  37
  38 };/* enum Kind_t */
  39
  40 }/* CVC4::kind namespace */
  41
  42 // import Kind into the "CVC4" namespace but keep the individual kind
  43 // constants under kind::
  44 typedef ::CVC4::kind::Kind_t Kind;
  45
  46 namespace kind {
  47
  48 inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
  49 inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
  50   using namespace CVC4::kind;
  51
  52   switch(k) {
  53
  54   /* special cases */
  55   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
  56   case NULL_EXPR: out << "NULL"; break;
  57 ${kind_printers}
  58   case LAST_KIND: out << "LAST_KIND"; break;
  59   default: out << "UNKNOWNKIND!" << int(k); break;
  60   }
  61
  62   return out;
  63 }
  64
  65 /** Returns true if the given kind is associative. This is used by ExprManager to
  66  * decide whether it's safe to modify big expressions by changing the grouping of
  67  * the arguments. */
  68 /* TODO: This could be generated. */
  69 inline bool isAssociative(::CVC4::Kind k) {
  70   switch(k) {
  71   case kind::AND:
  72   case kind::OR:
  73   case kind::MULT:
  74   case kind::PLUS:
  75     return true;
  76
  77   default:
  78     return false;
  79   }
  80 }
  81
  82 inline std::string kindToString(::CVC4::Kind k) {
  83   std::stringstream ss;
  84   ss << k;
  85   return ss.str();
  86 }
  87
  88 struct KindHashStrategy {
  89   static inline size_t hash(::CVC4::Kind k) { return k; }
  90 };/* struct KindHashStrategy */
  91
  92 }/* CVC4::kind namespace */
  93
  94 /**
  95  * The enumeration for the built-in atomic types.
  96  */
  97 enum TypeConstant {
  98   ${type_constant_list}
  99   LAST_TYPE
 100 };/* enum TypeConstant */
 101
 102 /**
 103  * We hash the constants with their values.
 104  */
 105 struct TypeConstantHashStrategy {
 106   static inline size_t hash(TypeConstant tc) {
 107     return tc;
 108   }
 109 };/* struct BoolHashStrategy */
 110
 111 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
 112   switch(typeConstant) {
 113   ${type_constant_descriptions}
 114   default:
 115     out << "UNKNOWN_TYPE_CONSTANT";
 116     break;
 117   }
 118   return out;
 119 }
 120
 121 namespace theory {
 122
 123 enum TheoryId {
 124   ${theory_enum}
 125   THEORY_LAST
 126 };
 127
 128 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
 129   switch(theoryId) {
 130   ${theory_descriptions}
 131   default:
 132     out << "UNKNOWN_THEORY";
 133     break;
 134   }
 135   return out;
 136 }
 137
 138 inline TheoryId kindToTheoryId(::CVC4::Kind k) {
 139   switch (k) {
 140     ${kind_to_theory_id}
 141   default:
 142     Unreachable();
 143   }
 144 }
 145
 146 inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
 147   switch (typeConstant) {
 148     ${type_constant_to_theory_id}
 149   default:
 150     Unreachable();
 151   }
 152 }
 153
 154 }/* theory namespace */
 155
 156
 157 }/* CVC4 namespace */
 158
 159 #endif /* __CVC4__KIND_H */