GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/theory/type_enumerator.cpp Lines: 31 37 83.8 %
Date: 2021-03-23 Branches: 42 104 40.4 %

Line Exec Source
1
/*********************                                                        */
2
/** type_enumerator.cpp
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This header file automatically generated by:
8
 **
9
 **     ../../../src/theory/mktheorytraits /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/type_enumerator_template.cpp /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/quantifiers/kinds
10
 **
11
 ** for the CVC4 project.
12
 **/
13
14
/*********************                                                        */
15
/*! \file type_enumerator_template.cpp
16
 ** \verbatim
17
 ** Top contributors (to current version):
18
 **   Morgan Deters, Mathias Preiner, Tim King
19
 ** This file is part of the CVC4 project.
20
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
21
 ** in the top-level source directory and their institutional affiliations.
22
 ** All rights reserved.  See the file COPYING in the top-level source
23
 ** directory for licensing information.\endverbatim
24
 **
25
 ** \brief Enumerators for types
26
 **
27
 ** Enumerators for types.
28
 **/
29
30
#include <sstream>
31
32
#include "base/check.h"
33
#include "expr/kind.h"
34
#include "theory/type_enumerator.h"
35
36
37
38
#include "theory/builtin/type_enumerator.h"
39
#include "theory/builtin/type_enumerator.h"
40
#include "theory/booleans/type_enumerator.h"
41
#include "theory/arith/type_enumerator.h"
42
#include "theory/arith/type_enumerator.h"
43
#include "theory/bv/type_enumerator.h"
44
#include "theory/fp/type_enumerator.h"
45
#include "theory/fp/type_enumerator.h"
46
#include "theory/arrays/type_enumerator.h"
47
#include "theory/datatypes/type_enumerator.h"
48
#include "theory/datatypes/type_enumerator.h"
49
#include "theory/sets/theory_sets_type_enumerator.h"
50
#include "theory/bags/theory_bags_type_enumerator.h"
51
#include "theory/strings/type_enumerator.h"
52
#include "theory/strings/type_enumerator.h"
53
54
using namespace std;
55
56
namespace CVC4 {
57
namespace theory {
58
59
180556
TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
60
    TypeNode type, TypeEnumeratorProperties* tep)
61
{
62
180556
  switch (type.getKind())
63
  {
64
8183
    case kind::TYPE_CONSTANT:
65
8183
      switch (type.getConst<TypeConstant>())
66
      {
67
68
1879
    case BOOLEAN_TYPE:
69
1879
      return new ::CVC4::theory::booleans::BooleanEnumerator(type, tep);
70
71
228
    case REAL_TYPE:
72
228
      return new ::CVC4::theory::arith::RationalEnumerator(type, tep);
73
74
5370
    case INTEGER_TYPE:
75
5370
      return new ::CVC4::theory::arith::IntegerEnumerator(type, tep);
76
77
1
    case ROUNDINGMODE_TYPE:
78
1
      return new ::CVC4::theory::fp::RoundingModeEnumerator(type, tep);
79
80
705
    case STRING_TYPE:
81
705
      return new ::CVC4::theory::strings::StringEnumerator(type, tep);
82
83
        default: Unhandled() << "No type enumerator for type `" << type << "'";
84
      }
85
      Unreachable();
86
87
3330
  case kind::SORT_TYPE:
88
3330
    return new ::CVC4::theory::builtin::UninterpretedSortEnumerator(type, tep);
89
90
  case kind::FUNCTION_TYPE:
91
    return new ::CVC4::theory::builtin::FunctionEnumerator(type, tep);
92
93
8036
  case kind::BITVECTOR_TYPE:
94
8036
    return new ::CVC4::theory::bv::BitVectorEnumerator(type, tep);
95
96
14
  case kind::FLOATINGPOINT_TYPE:
97
14
    return new ::CVC4::theory::fp::FloatingPointEnumerator(type, tep);
98
99
103
  case kind::ARRAY_TYPE:
100
103
    return new ::CVC4::theory::arrays::ArrayEnumerator(type, tep);
101
102
160761
  case kind::DATATYPE_TYPE:
103
160761
    return new ::CVC4::theory::datatypes::DatatypesEnumerator(type, tep);
104
105
95
  case kind::PARAMETRIC_DATATYPE:
106
95
    return new ::CVC4::theory::datatypes::DatatypesEnumerator(type, tep);
107
108
33
  case kind::SET_TYPE:
109
33
    return new ::CVC4::theory::sets::SetEnumerator(type, tep);
110
111
  case kind::BAG_TYPE:
112
    return new ::CVC4::theory::bags::BagEnumerator(type, tep);
113
114
1
  case kind::SEQUENCE_TYPE:
115
1
    return new ::CVC4::theory::strings::SequenceEnumerator(type, tep);
116
117
    default: Unhandled() << "No type enumerator for type `" << type << "'";
118
  }
119
  Unreachable();
120
}
121
122
}/* CVC4::theory namespace */
123
26691
}/* CVC4 namespace */