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