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-05-22/src/theory/type_enumerator_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/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/builtin/type_enumerator.h" |
42 |
|
#include "theory/booleans/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/type_enumerator.h" |
55 |
|
// clang-format on |
56 |
|
|
57 |
|
using namespace std; |
58 |
|
|
59 |
|
namespace cvc5 { |
60 |
|
namespace theory { |
61 |
|
|
62 |
113591 |
TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator( |
63 |
|
TypeNode type, TypeEnumeratorProperties* tep) |
64 |
|
{ |
65 |
113591 |
switch (type.getKind()) |
66 |
|
{ |
67 |
6414 |
case kind::TYPE_CONSTANT: |
68 |
6414 |
switch (type.getConst<TypeConstant>()) |
69 |
|
{ |
70 |
|
// clang-format off |
71 |
|
|
72 |
545 |
case BOOLEAN_TYPE: |
73 |
545 |
return new ::cvc5::theory::booleans::BooleanEnumerator(type, tep); |
74 |
|
|
75 |
214 |
case REAL_TYPE: |
76 |
214 |
return new ::cvc5::theory::arith::RationalEnumerator(type, tep); |
77 |
|
|
78 |
5242 |
case INTEGER_TYPE: |
79 |
5242 |
return new ::cvc5::theory::arith::IntegerEnumerator(type, tep); |
80 |
|
|
81 |
1 |
case ROUNDINGMODE_TYPE: |
82 |
1 |
return new ::cvc5::theory::fp::RoundingModeEnumerator(type, tep); |
83 |
|
|
84 |
412 |
case STRING_TYPE: |
85 |
412 |
return new ::cvc5::theory::strings::StringEnumerator(type, tep); |
86 |
|
|
87 |
|
// clang-format on |
88 |
|
default: Unhandled() << "No type enumerator for type `" << type << "'"; |
89 |
|
} |
90 |
|
Unreachable(); |
91 |
|
// clang-format off |
92 |
|
|
93 |
3315 |
case kind::SORT_TYPE: |
94 |
3315 |
return new ::cvc5::theory::builtin::UninterpretedSortEnumerator(type, tep); |
95 |
|
|
96 |
|
case kind::FUNCTION_TYPE: |
97 |
|
return new ::cvc5::theory::builtin::FunctionEnumerator(type, tep); |
98 |
|
|
99 |
7838 |
case kind::BITVECTOR_TYPE: |
100 |
7838 |
return new ::cvc5::theory::bv::BitVectorEnumerator(type, tep); |
101 |
|
|
102 |
14 |
case kind::FLOATINGPOINT_TYPE: |
103 |
14 |
return new ::cvc5::theory::fp::FloatingPointEnumerator(type, tep); |
104 |
|
|
105 |
100 |
case kind::ARRAY_TYPE: |
106 |
100 |
return new ::cvc5::theory::arrays::ArrayEnumerator(type, tep); |
107 |
|
|
108 |
95780 |
case kind::DATATYPE_TYPE: |
109 |
95780 |
return new ::cvc5::theory::datatypes::DatatypesEnumerator(type, tep); |
110 |
|
|
111 |
97 |
case kind::PARAMETRIC_DATATYPE: |
112 |
97 |
return new ::cvc5::theory::datatypes::DatatypesEnumerator(type, tep); |
113 |
|
|
114 |
32 |
case kind::SET_TYPE: |
115 |
32 |
return new ::cvc5::theory::sets::SetEnumerator(type, tep); |
116 |
|
|
117 |
|
case kind::BAG_TYPE: |
118 |
|
return new ::cvc5::theory::bags::BagEnumerator(type, tep); |
119 |
|
|
120 |
1 |
case kind::SEQUENCE_TYPE: |
121 |
1 |
return new ::cvc5::theory::strings::SequenceEnumerator(type, tep); |
122 |
|
|
123 |
|
// clang-format on |
124 |
|
default: Unhandled() << "No type enumerator for type `" << type << "'"; |
125 |
|
} |
126 |
|
Unreachable(); |
127 |
|
} |
128 |
|
|
129 |
|
} // namespace theory |
130 |
28194 |
} // namespace cvc5 |