GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/theory/theory_traits.h Lines: 41 42 97.6 %
Date: 2021-03-22 Branches: 13 20 65.0 %

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