src/expr/kind_middle.h

   1 /*********************                                                        */
   2 /** kind_middle.h
   3  ** Original author: mdeters
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Middle section of the Node kind header.  This file finishes off the
  14  ** Kind enum and starts the pretty-printing function definition.
  15  **/
  16
  17   LAST_KIND
  18
  19 };/* enum Kind */
  20
  21 inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
  22 inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
  23   using namespace CVC4;
  24
  25   switch(k) {
  26
  27   /* special cases */
  28   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
  29   case NULL_EXPR: out << "NULL"; break;
  30
  31   case EQUAL: out << "EQUAL"; break;
  32   case ITE: out << "ITE"; break;
  33   case SKOLEM: out << "SKOLEM"; break;
  34   case VARIABLE: out << "VARIABLE"; break;