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-09-29/src/theory/theory_traits_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/quantifiers/kinds |
13 |
|
* |
14 |
|
* for the cvc5 project. |
15 |
|
*/ |
16 |
|
|
17 |
|
/****************************************************************************** |
18 |
|
* Top contributors (to current version): |
19 |
|
* Morgan Deters, Dejan Jovanovic, Mathias Preiner |
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 |
|
* A template for the theory_traits.h header, defining various |
30 |
|
* (static) aspects of theories |
31 |
|
* |
32 |
|
* This file is a template for the theory_traits.h header, defining |
33 |
|
* various (static) aspects of theories, combined with the theory |
34 |
|
* kinds files to produce the final header. |
35 |
|
*/ |
36 |
|
|
37 |
|
#include "cvc5_private.h" |
38 |
|
|
39 |
|
#pragma once |
40 |
|
|
41 |
|
#include "options/theory_options.h" |
42 |
|
#include "theory/theory.h" |
43 |
|
|
44 |
|
// clang-format off |
45 |
|
#include "theory/builtin/theory_builtin.h" |
46 |
|
#include "theory/builtin/theory_builtin_rewriter.h" |
47 |
|
#include "theory/booleans/theory_bool.h" |
48 |
|
#include "theory/booleans/theory_bool_rewriter.h" |
49 |
|
#include "theory/uf/theory_uf.h" |
50 |
|
#include "theory/uf/theory_uf_rewriter.h" |
51 |
|
#include "theory/arith/theory_arith.h" |
52 |
|
#include "theory/arith/arith_rewriter.h" |
53 |
|
#include "theory/bv/theory_bv.h" |
54 |
|
#include "theory/bv/theory_bv_rewriter.h" |
55 |
|
#include "theory/fp/theory_fp.h" |
56 |
|
#include "theory/fp/theory_fp_rewriter.h" |
57 |
|
#include "theory/arrays/theory_arrays.h" |
58 |
|
#include "theory/arrays/theory_arrays_rewriter.h" |
59 |
|
#include "theory/datatypes/theory_datatypes.h" |
60 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
61 |
|
#include "theory/sep/theory_sep.h" |
62 |
|
#include "theory/sep/theory_sep_rewriter.h" |
63 |
|
#include "theory/sets/theory_sets.h" |
64 |
|
#include "theory/sets/theory_sets_rewriter.h" |
65 |
|
#include "theory/bags/theory_bags.h" |
66 |
|
#include "theory/bags/bags_rewriter.h" |
67 |
|
#include "theory/strings/theory_strings.h" |
68 |
|
#include "theory/strings/sequences_rewriter.h" |
69 |
|
#include "theory/quantifiers/theory_quantifiers.h" |
70 |
|
#include "theory/quantifiers/quantifiers_rewriter.h" |
71 |
|
|
72 |
|
// clang-format on |
73 |
|
|
74 |
|
namespace cvc5 { |
75 |
|
namespace theory { |
76 |
|
|
77 |
|
template <TheoryId theoryId> |
78 |
|
struct TheoryTraits; |
79 |
|
|
80 |
|
// clang-format off |
81 |
|
|
82 |
|
template<> |
83 |
|
struct TheoryTraits<THEORY_BUILTIN> { |
84 |
|
// typedef ::cvc5::theory::builtin::TheoryBuiltin theory_class; |
85 |
|
typedef ::cvc5::theory::builtin::TheoryBuiltinRewriter rewriter_class; |
86 |
|
|
87 |
|
static const bool isStableInfinite = true; |
88 |
|
static const bool isFinite = false; |
89 |
|
static const bool isPolite = false; |
90 |
|
static const bool isParametric = false; |
91 |
|
|
92 |
|
static const bool hasCheck = false; |
93 |
|
static const bool hasPropagate = false; |
94 |
|
static const bool hasPpStaticLearn = false; |
95 |
|
static const bool hasNotifyRestart = false; |
96 |
|
static const bool hasPresolve = false; |
97 |
|
static const bool hasPostsolve = false; |
98 |
|
};/* struct TheoryTraits<THEORY_BUILTIN> */ |
99 |
|
|
100 |
|
template<> |
101 |
|
struct TheoryTraits<THEORY_BOOL> { |
102 |
|
// typedef ::cvc5::theory::booleans::TheoryBool theory_class; |
103 |
|
typedef ::cvc5::theory::booleans::TheoryBoolRewriter rewriter_class; |
104 |
|
|
105 |
|
static const bool isStableInfinite = false; |
106 |
|
static const bool isFinite = true; |
107 |
|
static const bool isPolite = false; |
108 |
|
static const bool isParametric = false; |
109 |
|
|
110 |
|
static const bool hasCheck = false; |
111 |
|
static const bool hasPropagate = false; |
112 |
|
static const bool hasPpStaticLearn = false; |
113 |
|
static const bool hasNotifyRestart = false; |
114 |
|
static const bool hasPresolve = false; |
115 |
|
static const bool hasPostsolve = false; |
116 |
|
};/* struct TheoryTraits<THEORY_BOOL> */ |
117 |
|
|
118 |
|
template<> |
119 |
|
struct TheoryTraits<THEORY_UF> { |
120 |
|
// typedef ::cvc5::theory::uf::TheoryUF theory_class; |
121 |
|
typedef ::cvc5::theory::uf::TheoryUfRewriter rewriter_class; |
122 |
|
|
123 |
|
static const bool isStableInfinite = true; |
124 |
|
static const bool isFinite = false; |
125 |
|
static const bool isPolite = false; |
126 |
|
static const bool isParametric = true; |
127 |
|
|
128 |
|
static const bool hasCheck = true; |
129 |
|
static const bool hasPropagate = false; |
130 |
|
static const bool hasPpStaticLearn = true; |
131 |
|
static const bool hasNotifyRestart = false; |
132 |
|
static const bool hasPresolve = true; |
133 |
|
static const bool hasPostsolve = false; |
134 |
|
};/* struct TheoryTraits<THEORY_UF> */ |
135 |
|
|
136 |
|
template<> |
137 |
|
struct TheoryTraits<THEORY_ARITH> { |
138 |
|
// typedef ::cvc5::theory::arith::TheoryArith theory_class; |
139 |
|
typedef ::cvc5::theory::arith::ArithRewriter rewriter_class; |
140 |
|
|
141 |
|
static const bool isStableInfinite = true; |
142 |
|
static const bool isFinite = false; |
143 |
|
static const bool isPolite = false; |
144 |
|
static const bool isParametric = false; |
145 |
|
|
146 |
|
static const bool hasCheck = true; |
147 |
|
static const bool hasPropagate = true; |
148 |
|
static const bool hasPpStaticLearn = true; |
149 |
|
static const bool hasNotifyRestart = true; |
150 |
|
static const bool hasPresolve = true; |
151 |
|
static const bool hasPostsolve = false; |
152 |
|
};/* struct TheoryTraits<THEORY_ARITH> */ |
153 |
|
|
154 |
|
template<> |
155 |
|
struct TheoryTraits<THEORY_BV> { |
156 |
|
// typedef ::cvc5::theory::bv::TheoryBV theory_class; |
157 |
|
typedef ::cvc5::theory::bv::TheoryBVRewriter rewriter_class; |
158 |
|
|
159 |
|
static const bool isStableInfinite = false; |
160 |
|
static const bool isFinite = true; |
161 |
|
static const bool isPolite = false; |
162 |
|
static const bool isParametric = false; |
163 |
|
|
164 |
|
static const bool hasCheck = true; |
165 |
|
static const bool hasPropagate = true; |
166 |
|
static const bool hasPpStaticLearn = true; |
167 |
|
static const bool hasNotifyRestart = false; |
168 |
|
static const bool hasPresolve = true; |
169 |
|
static const bool hasPostsolve = false; |
170 |
|
};/* struct TheoryTraits<THEORY_BV> */ |
171 |
|
|
172 |
|
template<> |
173 |
|
struct TheoryTraits<THEORY_FP> { |
174 |
|
// typedef ::cvc5::theory::fp::TheoryFp theory_class; |
175 |
|
typedef ::cvc5::theory::fp::TheoryFpRewriter rewriter_class; |
176 |
|
|
177 |
|
static const bool isStableInfinite = false; |
178 |
|
static const bool isFinite = false; |
179 |
|
static const bool isPolite = false; |
180 |
|
static const bool isParametric = false; |
181 |
|
|
182 |
|
static const bool hasCheck = true; |
183 |
|
static const bool hasPropagate = false; |
184 |
|
static const bool hasPpStaticLearn = false; |
185 |
|
static const bool hasNotifyRestart = false; |
186 |
|
static const bool hasPresolve = false; |
187 |
|
static const bool hasPostsolve = false; |
188 |
|
};/* struct TheoryTraits<THEORY_FP> */ |
189 |
|
|
190 |
|
template<> |
191 |
|
struct TheoryTraits<THEORY_ARRAYS> { |
192 |
|
// typedef ::cvc5::theory::arrays::TheoryArrays theory_class; |
193 |
|
typedef ::cvc5::theory::arrays::TheoryArraysRewriter rewriter_class; |
194 |
|
|
195 |
|
static const bool isStableInfinite = true; |
196 |
|
static const bool isFinite = false; |
197 |
|
static const bool isPolite = true; |
198 |
|
static const bool isParametric = true; |
199 |
|
|
200 |
|
static const bool hasCheck = true; |
201 |
|
static const bool hasPropagate = false; |
202 |
|
static const bool hasPpStaticLearn = false; |
203 |
|
static const bool hasNotifyRestart = false; |
204 |
|
static const bool hasPresolve = true; |
205 |
|
static const bool hasPostsolve = false; |
206 |
|
};/* struct TheoryTraits<THEORY_ARRAYS> */ |
207 |
|
|
208 |
|
template<> |
209 |
|
struct TheoryTraits<THEORY_DATATYPES> { |
210 |
|
// typedef ::cvc5::theory::datatypes::TheoryDatatypes theory_class; |
211 |
|
typedef ::cvc5::theory::datatypes::DatatypesRewriter rewriter_class; |
212 |
|
|
213 |
|
static const bool isStableInfinite = false; |
214 |
|
static const bool isFinite = false; |
215 |
|
static const bool isPolite = false; |
216 |
|
static const bool isParametric = true; |
217 |
|
|
218 |
|
static const bool hasCheck = true; |
219 |
|
static const bool hasPropagate = false; |
220 |
|
static const bool hasPpStaticLearn = false; |
221 |
|
static const bool hasNotifyRestart = false; |
222 |
|
static const bool hasPresolve = false; |
223 |
|
static const bool hasPostsolve = false; |
224 |
|
};/* struct TheoryTraits<THEORY_DATATYPES> */ |
225 |
|
|
226 |
|
template<> |
227 |
|
struct TheoryTraits<THEORY_SEP> { |
228 |
|
// typedef ::cvc5::theory::sep::TheorySep theory_class; |
229 |
|
typedef ::cvc5::theory::sep::TheorySepRewriter rewriter_class; |
230 |
|
|
231 |
|
static const bool isStableInfinite = true; |
232 |
|
static const bool isFinite = false; |
233 |
|
static const bool isPolite = true; |
234 |
|
static const bool isParametric = true; |
235 |
|
|
236 |
|
static const bool hasCheck = true; |
237 |
|
static const bool hasPropagate = false; |
238 |
|
static const bool hasPpStaticLearn = false; |
239 |
|
static const bool hasNotifyRestart = false; |
240 |
|
static const bool hasPresolve = true; |
241 |
|
static const bool hasPostsolve = false; |
242 |
|
};/* struct TheoryTraits<THEORY_SEP> */ |
243 |
|
|
244 |
|
template<> |
245 |
|
struct TheoryTraits<THEORY_SETS> { |
246 |
|
// typedef ::cvc5::theory::sets::TheorySets theory_class; |
247 |
|
typedef ::cvc5::theory::sets::TheorySetsRewriter rewriter_class; |
248 |
|
|
249 |
|
static const bool isStableInfinite = false; |
250 |
|
static const bool isFinite = false; |
251 |
|
static const bool isPolite = false; |
252 |
|
static const bool isParametric = true; |
253 |
|
|
254 |
|
static const bool hasCheck = true; |
255 |
|
static const bool hasPropagate = false; |
256 |
|
static const bool hasPpStaticLearn = false; |
257 |
|
static const bool hasNotifyRestart = false; |
258 |
|
static const bool hasPresolve = true; |
259 |
|
static const bool hasPostsolve = false; |
260 |
|
};/* struct TheoryTraits<THEORY_SETS> */ |
261 |
|
|
262 |
|
template<> |
263 |
|
struct TheoryTraits<THEORY_BAGS> { |
264 |
|
// typedef ::cvc5::theory::bags::TheoryBags theory_class; |
265 |
|
typedef ::cvc5::theory::bags::BagsRewriter rewriter_class; |
266 |
|
|
267 |
|
static const bool isStableInfinite = false; |
268 |
|
static const bool isFinite = false; |
269 |
|
static const bool isPolite = false; |
270 |
|
static const bool isParametric = true; |
271 |
|
|
272 |
|
static const bool hasCheck = true; |
273 |
|
static const bool hasPropagate = false; |
274 |
|
static const bool hasPpStaticLearn = false; |
275 |
|
static const bool hasNotifyRestart = false; |
276 |
|
static const bool hasPresolve = true; |
277 |
|
static const bool hasPostsolve = false; |
278 |
|
};/* struct TheoryTraits<THEORY_BAGS> */ |
279 |
|
|
280 |
|
template<> |
281 |
|
struct TheoryTraits<THEORY_STRINGS> { |
282 |
|
// typedef ::cvc5::theory::strings::TheoryStrings theory_class; |
283 |
|
typedef ::cvc5::theory::strings::SequencesRewriter rewriter_class; |
284 |
|
|
285 |
|
static const bool isStableInfinite = false; |
286 |
|
static const bool isFinite = false; |
287 |
|
static const bool isPolite = false; |
288 |
|
static const bool isParametric = true; |
289 |
|
|
290 |
|
static const bool hasCheck = true; |
291 |
|
static const bool hasPropagate = false; |
292 |
|
static const bool hasPpStaticLearn = false; |
293 |
|
static const bool hasNotifyRestart = false; |
294 |
|
static const bool hasPresolve = true; |
295 |
|
static const bool hasPostsolve = false; |
296 |
|
};/* struct TheoryTraits<THEORY_STRINGS> */ |
297 |
|
|
298 |
|
template<> |
299 |
|
struct TheoryTraits<THEORY_QUANTIFIERS> { |
300 |
|
// typedef ::cvc5::theory::quantifiers::TheoryQuantifiers theory_class; |
301 |
|
typedef ::cvc5::theory::quantifiers::QuantifiersRewriter rewriter_class; |
302 |
|
|
303 |
|
static const bool isStableInfinite = false; |
304 |
|
static const bool isFinite = false; |
305 |
|
static const bool isPolite = false; |
306 |
|
static const bool isParametric = false; |
307 |
|
|
308 |
|
static const bool hasCheck = true; |
309 |
|
static const bool hasPropagate = false; |
310 |
|
static const bool hasPpStaticLearn = false; |
311 |
|
static const bool hasNotifyRestart = false; |
312 |
|
static const bool hasPresolve = true; |
313 |
|
static const bool hasPostsolve = false; |
314 |
|
};/* struct TheoryTraits<THEORY_QUANTIFIERS> */ |
315 |
|
|
316 |
|
// clang-format on |
317 |
|
|
318 |
|
struct TheoryConstructor |
319 |
|
{ |
320 |
81523 |
static void addTheory(TheoryEngine* engine, TheoryId id) |
321 |
|
{ |
322 |
81523 |
switch (id) |
323 |
|
{ |
324 |
|
// clang-format off |
325 |
|
|
326 |
6271 |
case THEORY_BUILTIN: |
327 |
|
|
328 |
6271 |
engine->addTheory< ::cvc5::theory::builtin::TheoryBuiltin >(THEORY_BUILTIN); |
329 |
6271 |
return; |
330 |
|
|
331 |
6271 |
case THEORY_BOOL: |
332 |
|
|
333 |
6271 |
engine->addTheory< ::cvc5::theory::booleans::TheoryBool >(THEORY_BOOL); |
334 |
6271 |
return; |
335 |
|
|
336 |
6271 |
case THEORY_UF: |
337 |
|
|
338 |
6271 |
engine->addTheory< ::cvc5::theory::uf::TheoryUF >(THEORY_UF); |
339 |
6271 |
return; |
340 |
|
|
341 |
6271 |
case THEORY_ARITH: |
342 |
|
|
343 |
6271 |
engine->addTheory< ::cvc5::theory::arith::TheoryArith >(THEORY_ARITH); |
344 |
6271 |
return; |
345 |
|
|
346 |
6271 |
case THEORY_BV: |
347 |
|
|
348 |
6271 |
engine->addTheory< ::cvc5::theory::bv::TheoryBV >(THEORY_BV); |
349 |
6271 |
return; |
350 |
|
|
351 |
6271 |
case THEORY_FP: |
352 |
|
|
353 |
6271 |
engine->addTheory< ::cvc5::theory::fp::TheoryFp >(THEORY_FP); |
354 |
6271 |
return; |
355 |
|
|
356 |
6271 |
case THEORY_ARRAYS: |
357 |
|
|
358 |
6271 |
engine->addTheory< ::cvc5::theory::arrays::TheoryArrays >(THEORY_ARRAYS); |
359 |
6271 |
return; |
360 |
|
|
361 |
6271 |
case THEORY_DATATYPES: |
362 |
|
|
363 |
6271 |
engine->addTheory< ::cvc5::theory::datatypes::TheoryDatatypes >(THEORY_DATATYPES); |
364 |
6271 |
return; |
365 |
|
|
366 |
6271 |
case THEORY_SEP: |
367 |
|
|
368 |
6271 |
engine->addTheory< ::cvc5::theory::sep::TheorySep >(THEORY_SEP); |
369 |
6271 |
return; |
370 |
|
|
371 |
6271 |
case THEORY_SETS: |
372 |
|
|
373 |
6271 |
engine->addTheory< ::cvc5::theory::sets::TheorySets >(THEORY_SETS); |
374 |
6271 |
return; |
375 |
|
|
376 |
6271 |
case THEORY_BAGS: |
377 |
|
|
378 |
6271 |
engine->addTheory< ::cvc5::theory::bags::TheoryBags >(THEORY_BAGS); |
379 |
6271 |
return; |
380 |
|
|
381 |
6271 |
case THEORY_STRINGS: |
382 |
|
|
383 |
6271 |
engine->addTheory< ::cvc5::theory::strings::TheoryStrings >(THEORY_STRINGS); |
384 |
6271 |
return; |
385 |
|
|
386 |
6271 |
case THEORY_QUANTIFIERS: |
387 |
|
|
388 |
6271 |
engine->addTheory< ::cvc5::theory::quantifiers::TheoryQuantifiers >(THEORY_QUANTIFIERS); |
389 |
6271 |
return; |
390 |
|
|
391 |
|
// clang-format on |
392 |
|
|
393 |
|
default: Unhandled() << id; |
394 |
|
} |
395 |
|
} |
396 |
|
}; /* struct cvc5::theory::TheoryConstructor */ |
397 |
|
|
398 |
|
} // namespace theory |
399 |
|
} // namespace cvc5 |