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 std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
  24   using namespace CVC4::kind;
  25
  26   switch(k) {
  27
  28   /* special cases */
  29   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
  30   case NULL_EXPR: out << "NULL"; break;
  31 ${kind_printers}
  32   case LAST_KIND: out << "LAST_KIND"; break;
  33   default: out << "UNKNOWNKIND!" << int(k); break;
  34   }
  35
  36   return out;
  37 }
  38
  39 /** Returns true if the given kind is associative. This is used by ExprManager to
  40  * decide whether it's safe to modify big expressions by changing the grouping of
  41  * the arguments. */
  42 /* TODO: This could be generated. */
  43 bool isAssociative(::CVC4::Kind k) {
  44   switch(k) {
  45   case kind::AND:
  46   case kind::OR:
  47   case kind::MULT:
  48   case kind::PLUS:
  49     return true;
  50
  51   default:
  52     return false;
  53   }
  54 }
  55
  56 std::string kindToString(::CVC4::Kind k) {
  57   std::stringstream ss;
  58   ss << k;
  59   return ss.str();
  60 }
  61
  62 }/* CVC4::kind namespace */
  63
  64 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
  65   switch(typeConstant) {
  66 ${type_constant_descriptions}
  67 #line 68 "${template}"
  68   default:
  69     out << "UNKNOWN_TYPE_CONSTANT";
  70     break;
  71   }
  72   return out;
  73 }
  74
  75 namespace theory {
  76
  77 TheoryId kindToTheoryId(::CVC4::Kind k) {
  78   switch(k) {
  79   case kind::UNDEFINED_KIND:
  80   case kind::NULL_EXPR:
  81     break;
  82 ${kind_to_theory_id}
  83 #line 84 "${template}"
  84   case kind::LAST_KIND:
  85     break;
  86   }
  87   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
  88 }
  89
  90 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
  91 {
  92   switch (typeConstant)
  93   {
  94 ${type_constant_to_theory_id}
  95 #line 96 "${template}"
  96     case LAST_TYPE: break;
  97   }
  98   throw IllegalArgumentException(
  99       "", "k", __PRETTY_FUNCTION__, "bad type constant");
 100 }
 101
 102 }/* CVC4::theory namespace */
 103 }/* CVC4 namespace */