src/theory/type_enumerator_template.cpp

   1 /*********************                                                        */
   2 /*! \file type_enumerator_template.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Mathias Preiner, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Enumerators for types
  13  **
  14  ** Enumerators for types.
  15  **/
  16
  17 #include <sstream>
  18
  19 #include "base/check.h"
  20 #include "expr/kind.h"
  21 #include "theory/type_enumerator.h"
  22
  23
  24 ${type_enumerator_includes}
  25
  26 using namespace std;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30
  31 TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
  32     TypeNode type, TypeEnumeratorProperties* tep)
  33 {
  34   switch (type.getKind())
  35   {
  36     case kind::TYPE_CONSTANT:
  37       switch (type.getConst<TypeConstant>())
  38       {
  39         ${mk_type_enumerator_type_constant_cases}
  40         default: Unhandled() << "No type enumerator for type `" << type << "'";
  41       }
  42       Unreachable();
  43       ${mk_type_enumerator_cases}
  44     default: Unhandled() << "No type enumerator for type `" << type << "'";
  45   }
  46   Unreachable();
  47 }
  48
  49 }/* CVC4::theory namespace */
  50 }/* CVC4 namespace */