src/expr/kind_template.cpp

   1 /*********************                                                        */
   2 /*! \file kind_template.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Morgan Deters, 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "expr/kind.h"
  19
  20 namespace CVC4 {
  21 namespace kind {
  22
  23 const char* toString(CVC4::Kind k)
  24 {
  25   using namespace CVC4::kind;
  26
  27   switch (k)
  28   {
  29     /* special cases */
  30     case UNDEFINED_KIND: return "UNDEFINED_KIND";
  31     case NULL_EXPR: return "NULL";
  32     ${kind_printers}
  33     case LAST_KIND: return "LAST_KIND";
  34     default: return "?";
  35   }
  36 }
  37
  38 std::ostream& operator<<(std::ostream& out, CVC4::Kind k)
  39 {
  40   out << toString(k);
  41   return out;
  42 }
  43
  44 /** Returns true if the given kind is associative. This is used by ExprManager to
  45  * decide whether it's safe to modify big expressions by changing the grouping of
  46  * the arguments. */
  47 /* TODO: This could be generated. */
  48 bool isAssociative(::CVC4::Kind k) {
  49   switch(k) {
  50   case kind::AND:
  51   case kind::OR:
  52   case kind::MULT:
  53   case kind::PLUS:
  54     return true;
  55
  56   default:
  57     return false;
  58   }
  59 }
  60
  61 std::string kindToString(::CVC4::Kind k) {
  62   std::stringstream ss;
  63   ss << k;
  64   return ss.str();
  65 }
  66
  67 }/* CVC4::kind namespace */
  68
  69 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
  70   switch(typeConstant) {
  71 ${type_constant_descriptions}
  72 #line 73 "${template}"
  73   default:
  74     out << "UNKNOWN_TYPE_CONSTANT";
  75     break;
  76   }
  77   return out;
  78 }
  79
  80 namespace theory {
  81
  82 TheoryId kindToTheoryId(::CVC4::Kind k) {
  83   switch(k) {
  84   case kind::UNDEFINED_KIND:
  85   case kind::NULL_EXPR:
  86     break;
  87 ${kind_to_theory_id}
  88 #line 89 "${template}"
  89   case kind::LAST_KIND:
  90     break;
  91   }
  92   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
  93 }
  94
  95 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
  96 {
  97   switch (typeConstant)
  98   {
  99 ${type_constant_to_theory_id}
 100 #line 101 "${template}"
 101     case LAST_TYPE: break;
 102   }
 103   throw IllegalArgumentException(
 104       "", "k", __PRETTY_FUNCTION__, "bad type constant");
 105 }
 106
 107 }/* CVC4::theory namespace */
 108 }/* CVC4 namespace */