src/theory/type_enumerator_template.cpp

   1 /*********************                                                        */
   2 /*! \file type_enumerator_template.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Enumerators for types
  13  **
  14  ** Enumerators for types.
  15  **/
  16
  17 #include <sstream>
  18
  19 #include "theory/type_enumerator.h"
  20
  21 #include "expr/kind.h"
  22 #include "util/cvc4_assert.h"
  23
  24 ${type_enumerator_includes}
  25 #line 26 "${template}"
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30 namespace theory {
  31
  32 TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type) throw(AssertionException) {
  33   switch(type.getKind()) {
  34   case kind::TYPE_CONSTANT:
  35     switch(type.getConst<TypeConstant>()) {
  36 ${mk_type_enumerator_type_constant_cases}
  37     default:
  38       {
  39         stringstream ss;
  40         ss << "No type enumerator for type `" << type << "'";
  41         Unhandled(ss.str());
  42       }
  43     }
  44     Unreachable();
  45 ${mk_type_enumerator_cases}
  46 #line 47 "${template}"
  47   default:
  48     {
  49       stringstream ss;
  50       ss << "No type enumerator for type `" << type << "'";
  51       Unhandled(ss.str());
  52     }
  53   }
  54   Unreachable();
  55 }
  56
  57 }/* CVC4::theory namespace */
  58 }/* CVC4 namespace */