GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/metakind.h Lines: 12 12 100.0 %
Date: 2021-03-23 Branches: 462 4600 10.0 %

Line Exec Source
1
/*********************                                                        */
2
/** metakind.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/expr/mkmetakind /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/metakind_template.h /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 metakind_template.h
16
 ** \verbatim
17
 ** Top contributors (to current version):
18
 **   Morgan Deters, Andres Noetzli, 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 Template for the metakind header.
26
 **
27
 ** Template for the metakind header.
28
 **/
29
30
#include "cvc4_private.h"
31
32
#ifndef CVC4__KIND__METAKIND_H
33
#define CVC4__KIND__METAKIND_H
34
35
#include <iosfwd>
36
37
#include "base/check.h"
38
#include "expr/kind.h"
39
40
namespace CVC4 {
41
42
namespace expr {
43
  class NodeValue;
44
}/* CVC4::expr namespace */
45
46
namespace kind {
47
namespace metakind {
48
49
/**
50
 * Static, compile-time information about types T representing CVC4
51
 * constants:
52
 *
53
 *   typename ConstantMap<T>::OwningTheory
54
 *
55
 *     The theory in charge of constructing T when constructing Nodes
56
 *     with NodeManager::mkConst(T).
57
 *
58
 *   typename ConstantMap<T>::kind
59
 *
60
 *     The kind to use when constructing Nodes with
61
 *     NodeManager::mkConst(T).
62
 */
63
template <class T>
64
struct ConstantMap;
65
66
/**
67
 * Static, compile-time information about kinds k and what type their
68
 * corresponding CVC4 constants are:
69
 *
70
 *   typename ConstantMapReverse<k>::T
71
 *
72
 *     Constant type for kind k.
73
 */
74
template <Kind k>
75
struct ConstantMapReverse;
76
77
/**
78
 * Static, compile-time mapping from CONSTANT kinds to comparison
79
 * functors on NodeValue*.  The single element of this structure is:
80
 *
81
 *   static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
82
 *
83
 *     Compares x and y, given that they are both K-kinded (and the
84
 *     meta-kind of K is CONSTANT).  If pool == true, one of x and y
85
 *     (but not both) may be a "non-inlined" NodeValue.  If pool ==
86
 *     false, neither x nor y may be a "non-inlined" NodeValue.
87
 */
88
template <Kind k, bool pool>
89
struct NodeValueConstCompare {
90
  inline static bool compare(const ::CVC4::expr::NodeValue* x,
91
                             const ::CVC4::expr::NodeValue* y);
92
  inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
93
};/* NodeValueConstCompare<k, pool> */
94
95
struct NodeValueCompare {
96
  template <bool pool>
97
  static bool compare(const ::CVC4::expr::NodeValue* nv1,
98
                      const ::CVC4::expr::NodeValue* nv2);
99
  static size_t constHash(const ::CVC4::expr::NodeValue* nv);
100
};/* struct NodeValueCompare */
101
102
/**
103
 * "metakinds" represent the "kinds" of kinds at the meta-level.
104
 * "metakind" is an ugly name but it's not used by client code, just
105
 * by the expr package, and the intent here is to keep it from
106
 * polluting the kind namespace.  For more documentation on what these
107
 * mean, see src/theory/builtin/kinds.
108
 */
109
enum MetaKind_t {
110
  INVALID = -1, /**< special node non-kinds like NULL_EXPR or LAST_KIND */
111
  VARIABLE, /**< special node kinds: no operator */
112
  OPERATOR, /**< operators that get "inlined" */
113
  PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */
114
  CONSTANT, /**< constants */
115
  NULLARY_OPERATOR /**< nullary operator */
116
};/* enum MetaKind_t */
117
118
}/* CVC4::kind::metakind namespace */
119
120
// import MetaKind into the "CVC4::kind" namespace but keep the
121
// individual MetaKind constants under kind::metakind::
122
typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
123
124
/**
125
 * Get the metakind for a particular kind.
126
 */
127
MetaKind metaKindOf(Kind k);
128
}/* CVC4::kind namespace */
129
130
namespace expr {
131
132
// Comparison predicate
133
struct NodeValuePoolEq {
134
673057496
  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
135
673057496
    return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
136
  }
137
};
138
139
}/* CVC4::expr namespace */
140
}/* CVC4 namespace */
141
142
#include "expr/node_value.h"
143
144
#endif /* CVC4__KIND__METAKIND_H */
145
146
147
// #include "theory/builtin/::CVC4::theory::builtin::TheoryBuiltin"
148
#include "expr/uninterpreted_constant.h"
149
#include "util/abstract_value.h"
150
#include "expr/kind.h"
151
// #include "theory/booleans/::CVC4::theory::booleans::TheoryBool"
152
#include "util/bool.h"
153
// #include "theory/uf/::CVC4::theory::uf::TheoryUF"
154
// #include "theory/arith/::CVC4::theory::arith::TheoryArith"
155
#include "util/divisible.h"
156
#include "util/rational.h"
157
#include "util/indexed_root_predicate.h"
158
#include "util/iand.h"
159
// #include "theory/bv/::CVC4::theory::bv::TheoryBV"
160
#include "util/bitvector.h"
161
// #include "theory/fp/::CVC4::theory::fp::TheoryFp"
162
#include "util/floatingpoint.h"
163
// #include "theory/arrays/::CVC4::theory::arrays::TheoryArrays"
164
#include "expr/array_store_all.h"
165
// #include "theory/datatypes/::CVC4::theory::datatypes::TheoryDatatypes"
166
#include "expr/datatype_index.h"
167
#include "expr/ascription_type.h"
168
#include "util/tuple.h"
169
#include "expr/record.h"
170
#include "theory/datatypes/tuple_project_op.h"
171
// #include "theory/sep/::CVC4::theory::sep::TheorySep"
172
// #include "theory/sets/::CVC4::theory::sets::TheorySets"
173
#include "expr/emptyset.h"
174
#include "theory/sets/singleton_op.h"
175
// #include "theory/bags/::CVC4::theory::bags::TheoryBags"
176
#include "expr/emptybag.h"
177
#include "theory/bags/make_bag_op.h"
178
// #include "theory/strings/::CVC4::theory::strings::TheoryStrings"
179
#include "util/string.h"
180
#include "expr/sequence.h"
181
#include "util/regexp.h"
182
// #include "theory/quantifiers/::CVC4::theory::quantifiers::TheoryQuantifiers"
183
184
#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
185
186
namespace CVC4 {
187
188
namespace expr {
189
190
template <>
191
::CVC4::UninterpretedConstant const& NodeValue::getConst< ::CVC4::UninterpretedConstant >() const;
192
193
template <>
194
::CVC4::AbstractValue const& NodeValue::getConst< ::CVC4::AbstractValue >() const;
195
196
template <>
197
::CVC4::Kind const& NodeValue::getConst< ::CVC4::Kind >() const;
198
199
template <>
200
::CVC4::TypeConstant const& NodeValue::getConst< ::CVC4::TypeConstant >() const;
201
202
template <>
203
bool const& NodeValue::getConst< bool >() const;
204
205
template <>
206
::CVC4::Divisible const& NodeValue::getConst< ::CVC4::Divisible >() const;
207
208
template <>
209
::CVC4::Rational const& NodeValue::getConst< ::CVC4::Rational >() const;
210
211
template <>
212
::CVC4::IndexedRootPredicate const& NodeValue::getConst< ::CVC4::IndexedRootPredicate >() const;
213
214
template <>
215
::CVC4::IntAnd const& NodeValue::getConst< ::CVC4::IntAnd >() const;
216
217
template <>
218
::CVC4::BitVectorSize const& NodeValue::getConst< ::CVC4::BitVectorSize >() const;
219
220
template <>
221
::CVC4::BitVector const& NodeValue::getConst< ::CVC4::BitVector >() const;
222
223
template <>
224
::CVC4::BitVectorBitOf const& NodeValue::getConst< ::CVC4::BitVectorBitOf >() const;
225
226
template <>
227
::CVC4::BitVectorExtract const& NodeValue::getConst< ::CVC4::BitVectorExtract >() const;
228
229
template <>
230
::CVC4::BitVectorRepeat const& NodeValue::getConst< ::CVC4::BitVectorRepeat >() const;
231
232
template <>
233
::CVC4::BitVectorRotateLeft const& NodeValue::getConst< ::CVC4::BitVectorRotateLeft >() const;
234
235
template <>
236
::CVC4::BitVectorRotateRight const& NodeValue::getConst< ::CVC4::BitVectorRotateRight >() const;
237
238
template <>
239
::CVC4::BitVectorSignExtend const& NodeValue::getConst< ::CVC4::BitVectorSignExtend >() const;
240
241
template <>
242
::CVC4::BitVectorZeroExtend const& NodeValue::getConst< ::CVC4::BitVectorZeroExtend >() const;
243
244
template <>
245
::CVC4::IntToBitVector const& NodeValue::getConst< ::CVC4::IntToBitVector >() const;
246
247
template <>
248
::CVC4::FloatingPoint const& NodeValue::getConst< ::CVC4::FloatingPoint >() const;
249
250
template <>
251
::CVC4::RoundingMode const& NodeValue::getConst< ::CVC4::RoundingMode >() const;
252
253
template <>
254
::CVC4::FloatingPointSize const& NodeValue::getConst< ::CVC4::FloatingPointSize >() const;
255
256
template <>
257
::CVC4::FloatingPointToFPIEEEBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPIEEEBitVector >() const;
258
259
template <>
260
::CVC4::FloatingPointToFPFloatingPoint const& NodeValue::getConst< ::CVC4::FloatingPointToFPFloatingPoint >() const;
261
262
template <>
263
::CVC4::FloatingPointToFPReal const& NodeValue::getConst< ::CVC4::FloatingPointToFPReal >() const;
264
265
template <>
266
::CVC4::FloatingPointToFPSignedBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPSignedBitVector >() const;
267
268
template <>
269
::CVC4::FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPUnsignedBitVector >() const;
270
271
template <>
272
::CVC4::FloatingPointToFPGeneric const& NodeValue::getConst< ::CVC4::FloatingPointToFPGeneric >() const;
273
274
template <>
275
::CVC4::FloatingPointToUBV const& NodeValue::getConst< ::CVC4::FloatingPointToUBV >() const;
276
277
template <>
278
::CVC4::FloatingPointToUBVTotal const& NodeValue::getConst< ::CVC4::FloatingPointToUBVTotal >() const;
279
280
template <>
281
::CVC4::FloatingPointToSBV const& NodeValue::getConst< ::CVC4::FloatingPointToSBV >() const;
282
283
template <>
284
::CVC4::FloatingPointToSBVTotal const& NodeValue::getConst< ::CVC4::FloatingPointToSBVTotal >() const;
285
286
template <>
287
::CVC4::ArrayStoreAll const& NodeValue::getConst< ::CVC4::ArrayStoreAll >() const;
288
289
template <>
290
::CVC4::DatatypeIndexConstant const& NodeValue::getConst< ::CVC4::DatatypeIndexConstant >() const;
291
292
template <>
293
::CVC4::AscriptionType const& NodeValue::getConst< ::CVC4::AscriptionType >() const;
294
295
template <>
296
::CVC4::TupleUpdate const& NodeValue::getConst< ::CVC4::TupleUpdate >() const;
297
298
template <>
299
::CVC4::RecordUpdate const& NodeValue::getConst< ::CVC4::RecordUpdate >() const;
300
301
template <>
302
::CVC4::TupleProjectOp const& NodeValue::getConst< ::CVC4::TupleProjectOp >() const;
303
304
template <>
305
::CVC4::EmptySet const& NodeValue::getConst< ::CVC4::EmptySet >() const;
306
307
template <>
308
::CVC4::SingletonOp const& NodeValue::getConst< ::CVC4::SingletonOp >() const;
309
310
template <>
311
::CVC4::EmptyBag const& NodeValue::getConst< ::CVC4::EmptyBag >() const;
312
313
template <>
314
::CVC4::MakeBagOp const& NodeValue::getConst< ::CVC4::MakeBagOp >() const;
315
316
template <>
317
::CVC4::String const& NodeValue::getConst< ::CVC4::String >() const;
318
319
template <>
320
::CVC4::Sequence const& NodeValue::getConst< ::CVC4::Sequence >() const;
321
322
template <>
323
::CVC4::RegExpRepeat const& NodeValue::getConst< ::CVC4::RegExpRepeat >() const;
324
325
template <>
326
::CVC4::RegExpLoop const& NodeValue::getConst< ::CVC4::RegExpLoop >() const;
327
328
}/* CVC4::expr namespace */
329
330
namespace kind {
331
namespace metakind {
332
333
template <Kind k, bool pool>
334
477087428
inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x,
335
                                                    const ::CVC4::expr::NodeValue* y) {
336
  typedef typename ConstantMapReverse<k>::T T;
337
  if(pool) {
338
477087428
    if(x->d_nchildren == 1) {
339
234477697
      Assert(y->d_nchildren == 0);
340
234477697
      return compare(y, x);
341
242609731
    } else if(y->d_nchildren == 1) {
342
234477697
      Assert(x->d_nchildren == 0);
343
234477697
      return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
344
    }
345
  }
346
347
8132034
  Assert(x->d_nchildren == 0);
348
8132034
  Assert(y->d_nchildren == 0);
349
8132034
  return x->getConst<T>() == y->getConst<T>();
350
}
351
352
template <Kind k, bool pool>
353
inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) {
354
  typedef typename ConstantMapReverse<k>::T T;
355
  return nv->getConst<T>().hash();
356
}
357
358
359
template <>
360
struct ConstantMap< ::CVC4::UninterpretedConstant > {
361
  // typedef THEORY_BUILTIN OwningTheory;
362
  enum { kind = ::CVC4::kind::UNINTERPRETED_CONSTANT };
363
};/* ConstantMap< ::CVC4::UninterpretedConstant > */
364
365
template <>
366
struct ConstantMapReverse< ::CVC4::kind::UNINTERPRETED_CONSTANT > {
367
  typedef ::CVC4::UninterpretedConstant T;
368
};/* ConstantMapReverse< ::CVC4::kind::UNINTERPRETED_CONSTANT > */
369
370
template <>
371
struct ConstantMap< ::CVC4::AbstractValue > {
372
  // typedef THEORY_BUILTIN OwningTheory;
373
  enum { kind = ::CVC4::kind::ABSTRACT_VALUE };
374
};/* ConstantMap< ::CVC4::AbstractValue > */
375
376
template <>
377
struct ConstantMapReverse< ::CVC4::kind::ABSTRACT_VALUE > {
378
  typedef ::CVC4::AbstractValue T;
379
};/* ConstantMapReverse< ::CVC4::kind::ABSTRACT_VALUE > */
380
381
template <>
382
struct ConstantMap< ::CVC4::Kind > {
383
  // typedef THEORY_BUILTIN OwningTheory;
384
  enum { kind = ::CVC4::kind::BUILTIN };
385
};/* ConstantMap< ::CVC4::Kind > */
386
387
template <>
388
struct ConstantMapReverse< ::CVC4::kind::BUILTIN > {
389
  typedef ::CVC4::Kind T;
390
};/* ConstantMapReverse< ::CVC4::kind::BUILTIN > */
391
392
template <>
393
struct ConstantMap< ::CVC4::TypeConstant > {
394
  // typedef THEORY_BUILTIN OwningTheory;
395
  enum { kind = ::CVC4::kind::TYPE_CONSTANT };
396
};/* ConstantMap< ::CVC4::TypeConstant > */
397
398
template <>
399
struct ConstantMapReverse< ::CVC4::kind::TYPE_CONSTANT > {
400
  typedef ::CVC4::TypeConstant T;
401
};/* ConstantMapReverse< ::CVC4::kind::TYPE_CONSTANT > */
402
403
template <>
404
struct ConstantMap< bool > {
405
  // typedef THEORY_BOOL OwningTheory;
406
  enum { kind = ::CVC4::kind::CONST_BOOLEAN };
407
};/* ConstantMap< bool > */
408
409
template <>
410
struct ConstantMapReverse< ::CVC4::kind::CONST_BOOLEAN > {
411
  typedef bool T;
412
};/* ConstantMapReverse< ::CVC4::kind::CONST_BOOLEAN > */
413
414
template <>
415
struct ConstantMap< ::CVC4::Divisible > {
416
  // typedef THEORY_ARITH OwningTheory;
417
  enum { kind = ::CVC4::kind::DIVISIBLE_OP };
418
};/* ConstantMap< ::CVC4::Divisible > */
419
420
template <>
421
struct ConstantMapReverse< ::CVC4::kind::DIVISIBLE_OP > {
422
  typedef ::CVC4::Divisible T;
423
};/* ConstantMapReverse< ::CVC4::kind::DIVISIBLE_OP > */
424
425
template <>
426
struct ConstantMap< ::CVC4::Rational > {
427
  // typedef THEORY_ARITH OwningTheory;
428
  enum { kind = ::CVC4::kind::CONST_RATIONAL };
429
};/* ConstantMap< ::CVC4::Rational > */
430
431
template <>
432
struct ConstantMapReverse< ::CVC4::kind::CONST_RATIONAL > {
433
  typedef ::CVC4::Rational T;
434
};/* ConstantMapReverse< ::CVC4::kind::CONST_RATIONAL > */
435
436
template <>
437
struct ConstantMap< ::CVC4::IndexedRootPredicate > {
438
  // typedef THEORY_ARITH OwningTheory;
439
  enum { kind = ::CVC4::kind::INDEXED_ROOT_PREDICATE_OP };
440
};/* ConstantMap< ::CVC4::IndexedRootPredicate > */
441
442
template <>
443
struct ConstantMapReverse< ::CVC4::kind::INDEXED_ROOT_PREDICATE_OP > {
444
  typedef ::CVC4::IndexedRootPredicate T;
445
};/* ConstantMapReverse< ::CVC4::kind::INDEXED_ROOT_PREDICATE_OP > */
446
447
template <>
448
struct ConstantMap< ::CVC4::IntAnd > {
449
  // typedef THEORY_ARITH OwningTheory;
450
  enum { kind = ::CVC4::kind::IAND_OP };
451
};/* ConstantMap< ::CVC4::IntAnd > */
452
453
template <>
454
struct ConstantMapReverse< ::CVC4::kind::IAND_OP > {
455
  typedef ::CVC4::IntAnd T;
456
};/* ConstantMapReverse< ::CVC4::kind::IAND_OP > */
457
458
template <>
459
struct ConstantMap< ::CVC4::BitVectorSize > {
460
  // typedef THEORY_BV OwningTheory;
461
  enum { kind = ::CVC4::kind::BITVECTOR_TYPE };
462
};/* ConstantMap< ::CVC4::BitVectorSize > */
463
464
template <>
465
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_TYPE > {
466
  typedef ::CVC4::BitVectorSize T;
467
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_TYPE > */
468
469
template <>
470
struct ConstantMap< ::CVC4::BitVector > {
471
  // typedef THEORY_BV OwningTheory;
472
  enum { kind = ::CVC4::kind::CONST_BITVECTOR };
473
};/* ConstantMap< ::CVC4::BitVector > */
474
475
template <>
476
struct ConstantMapReverse< ::CVC4::kind::CONST_BITVECTOR > {
477
  typedef ::CVC4::BitVector T;
478
};/* ConstantMapReverse< ::CVC4::kind::CONST_BITVECTOR > */
479
480
template <>
481
struct ConstantMap< ::CVC4::BitVectorBitOf > {
482
  // typedef THEORY_BV OwningTheory;
483
  enum { kind = ::CVC4::kind::BITVECTOR_BITOF_OP };
484
};/* ConstantMap< ::CVC4::BitVectorBitOf > */
485
486
template <>
487
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_BITOF_OP > {
488
  typedef ::CVC4::BitVectorBitOf T;
489
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_BITOF_OP > */
490
491
template <>
492
struct ConstantMap< ::CVC4::BitVectorExtract > {
493
  // typedef THEORY_BV OwningTheory;
494
  enum { kind = ::CVC4::kind::BITVECTOR_EXTRACT_OP };
495
};/* ConstantMap< ::CVC4::BitVectorExtract > */
496
497
template <>
498
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_EXTRACT_OP > {
499
  typedef ::CVC4::BitVectorExtract T;
500
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_EXTRACT_OP > */
501
502
template <>
503
struct ConstantMap< ::CVC4::BitVectorRepeat > {
504
  // typedef THEORY_BV OwningTheory;
505
  enum { kind = ::CVC4::kind::BITVECTOR_REPEAT_OP };
506
};/* ConstantMap< ::CVC4::BitVectorRepeat > */
507
508
template <>
509
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_REPEAT_OP > {
510
  typedef ::CVC4::BitVectorRepeat T;
511
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_REPEAT_OP > */
512
513
template <>
514
struct ConstantMap< ::CVC4::BitVectorRotateLeft > {
515
  // typedef THEORY_BV OwningTheory;
516
  enum { kind = ::CVC4::kind::BITVECTOR_ROTATE_LEFT_OP };
517
};/* ConstantMap< ::CVC4::BitVectorRotateLeft > */
518
519
template <>
520
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_ROTATE_LEFT_OP > {
521
  typedef ::CVC4::BitVectorRotateLeft T;
522
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_ROTATE_LEFT_OP > */
523
524
template <>
525
struct ConstantMap< ::CVC4::BitVectorRotateRight > {
526
  // typedef THEORY_BV OwningTheory;
527
  enum { kind = ::CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP };
528
};/* ConstantMap< ::CVC4::BitVectorRotateRight > */
529
530
template <>
531
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP > {
532
  typedef ::CVC4::BitVectorRotateRight T;
533
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP > */
534
535
template <>
536
struct ConstantMap< ::CVC4::BitVectorSignExtend > {
537
  // typedef THEORY_BV OwningTheory;
538
  enum { kind = ::CVC4::kind::BITVECTOR_SIGN_EXTEND_OP };
539
};/* ConstantMap< ::CVC4::BitVectorSignExtend > */
540
541
template <>
542
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_SIGN_EXTEND_OP > {
543
  typedef ::CVC4::BitVectorSignExtend T;
544
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_SIGN_EXTEND_OP > */
545
546
template <>
547
struct ConstantMap< ::CVC4::BitVectorZeroExtend > {
548
  // typedef THEORY_BV OwningTheory;
549
  enum { kind = ::CVC4::kind::BITVECTOR_ZERO_EXTEND_OP };
550
};/* ConstantMap< ::CVC4::BitVectorZeroExtend > */
551
552
template <>
553
struct ConstantMapReverse< ::CVC4::kind::BITVECTOR_ZERO_EXTEND_OP > {
554
  typedef ::CVC4::BitVectorZeroExtend T;
555
};/* ConstantMapReverse< ::CVC4::kind::BITVECTOR_ZERO_EXTEND_OP > */
556
557
template <>
558
struct ConstantMap< ::CVC4::IntToBitVector > {
559
  // typedef THEORY_BV OwningTheory;
560
  enum { kind = ::CVC4::kind::INT_TO_BITVECTOR_OP };
561
};/* ConstantMap< ::CVC4::IntToBitVector > */
562
563
template <>
564
struct ConstantMapReverse< ::CVC4::kind::INT_TO_BITVECTOR_OP > {
565
  typedef ::CVC4::IntToBitVector T;
566
};/* ConstantMapReverse< ::CVC4::kind::INT_TO_BITVECTOR_OP > */
567
568
template <>
569
struct ConstantMap< ::CVC4::FloatingPoint > {
570
  // typedef THEORY_FP OwningTheory;
571
  enum { kind = ::CVC4::kind::CONST_FLOATINGPOINT };
572
};/* ConstantMap< ::CVC4::FloatingPoint > */
573
574
template <>
575
struct ConstantMapReverse< ::CVC4::kind::CONST_FLOATINGPOINT > {
576
  typedef ::CVC4::FloatingPoint T;
577
};/* ConstantMapReverse< ::CVC4::kind::CONST_FLOATINGPOINT > */
578
579
template <>
580
struct ConstantMap< ::CVC4::RoundingMode > {
581
  // typedef THEORY_FP OwningTheory;
582
  enum { kind = ::CVC4::kind::CONST_ROUNDINGMODE };
583
};/* ConstantMap< ::CVC4::RoundingMode > */
584
585
template <>
586
struct ConstantMapReverse< ::CVC4::kind::CONST_ROUNDINGMODE > {
587
  typedef ::CVC4::RoundingMode T;
588
};/* ConstantMapReverse< ::CVC4::kind::CONST_ROUNDINGMODE > */
589
590
template <>
591
struct ConstantMap< ::CVC4::FloatingPointSize > {
592
  // typedef THEORY_FP OwningTheory;
593
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TYPE };
594
};/* ConstantMap< ::CVC4::FloatingPointSize > */
595
596
template <>
597
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TYPE > {
598
  typedef ::CVC4::FloatingPointSize T;
599
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TYPE > */
600
601
template <>
602
struct ConstantMap< ::CVC4::FloatingPointToFPIEEEBitVector > {
603
  // typedef THEORY_FP OwningTheory;
604
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP };
605
};/* ConstantMap< ::CVC4::FloatingPointToFPIEEEBitVector > */
606
607
template <>
608
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > {
609
  typedef ::CVC4::FloatingPointToFPIEEEBitVector T;
610
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > */
611
612
template <>
613
struct ConstantMap< ::CVC4::FloatingPointToFPFloatingPoint > {
614
  // typedef THEORY_FP OwningTheory;
615
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP };
616
};/* ConstantMap< ::CVC4::FloatingPointToFPFloatingPoint > */
617
618
template <>
619
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > {
620
  typedef ::CVC4::FloatingPointToFPFloatingPoint T;
621
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > */
622
623
template <>
624
struct ConstantMap< ::CVC4::FloatingPointToFPReal > {
625
  // typedef THEORY_FP OwningTheory;
626
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_REAL_OP };
627
};/* ConstantMap< ::CVC4::FloatingPointToFPReal > */
628
629
template <>
630
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_REAL_OP > {
631
  typedef ::CVC4::FloatingPointToFPReal T;
632
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_REAL_OP > */
633
634
template <>
635
struct ConstantMap< ::CVC4::FloatingPointToFPSignedBitVector > {
636
  // typedef THEORY_FP OwningTheory;
637
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP };
638
};/* ConstantMap< ::CVC4::FloatingPointToFPSignedBitVector > */
639
640
template <>
641
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > {
642
  typedef ::CVC4::FloatingPointToFPSignedBitVector T;
643
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > */
644
645
template <>
646
struct ConstantMap< ::CVC4::FloatingPointToFPUnsignedBitVector > {
647
  // typedef THEORY_FP OwningTheory;
648
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP };
649
};/* ConstantMap< ::CVC4::FloatingPointToFPUnsignedBitVector > */
650
651
template <>
652
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > {
653
  typedef ::CVC4::FloatingPointToFPUnsignedBitVector T;
654
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > */
655
656
template <>
657
struct ConstantMap< ::CVC4::FloatingPointToFPGeneric > {
658
  // typedef THEORY_FP OwningTheory;
659
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_FP_GENERIC_OP };
660
};/* ConstantMap< ::CVC4::FloatingPointToFPGeneric > */
661
662
template <>
663
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > {
664
  typedef ::CVC4::FloatingPointToFPGeneric T;
665
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > */
666
667
template <>
668
struct ConstantMap< ::CVC4::FloatingPointToUBV > {
669
  // typedef THEORY_FP OwningTheory;
670
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_UBV_OP };
671
};/* ConstantMap< ::CVC4::FloatingPointToUBV > */
672
673
template <>
674
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_UBV_OP > {
675
  typedef ::CVC4::FloatingPointToUBV T;
676
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_UBV_OP > */
677
678
template <>
679
struct ConstantMap< ::CVC4::FloatingPointToUBVTotal > {
680
  // typedef THEORY_FP OwningTheory;
681
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP };
682
};/* ConstantMap< ::CVC4::FloatingPointToUBVTotal > */
683
684
template <>
685
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > {
686
  typedef ::CVC4::FloatingPointToUBVTotal T;
687
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > */
688
689
template <>
690
struct ConstantMap< ::CVC4::FloatingPointToSBV > {
691
  // typedef THEORY_FP OwningTheory;
692
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_SBV_OP };
693
};/* ConstantMap< ::CVC4::FloatingPointToSBV > */
694
695
template <>
696
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_SBV_OP > {
697
  typedef ::CVC4::FloatingPointToSBV T;
698
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_SBV_OP > */
699
700
template <>
701
struct ConstantMap< ::CVC4::FloatingPointToSBVTotal > {
702
  // typedef THEORY_FP OwningTheory;
703
  enum { kind = ::CVC4::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP };
704
};/* ConstantMap< ::CVC4::FloatingPointToSBVTotal > */
705
706
template <>
707
struct ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > {
708
  typedef ::CVC4::FloatingPointToSBVTotal T;
709
};/* ConstantMapReverse< ::CVC4::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > */
710
711
template <>
712
struct ConstantMap< ::CVC4::ArrayStoreAll > {
713
  // typedef THEORY_ARRAYS OwningTheory;
714
  enum { kind = ::CVC4::kind::STORE_ALL };
715
};/* ConstantMap< ::CVC4::ArrayStoreAll > */
716
717
template <>
718
struct ConstantMapReverse< ::CVC4::kind::STORE_ALL > {
719
  typedef ::CVC4::ArrayStoreAll T;
720
};/* ConstantMapReverse< ::CVC4::kind::STORE_ALL > */
721
722
template <>
723
struct ConstantMap< ::CVC4::DatatypeIndexConstant > {
724
  // typedef THEORY_DATATYPES OwningTheory;
725
  enum { kind = ::CVC4::kind::DATATYPE_TYPE };
726
};/* ConstantMap< ::CVC4::DatatypeIndexConstant > */
727
728
template <>
729
struct ConstantMapReverse< ::CVC4::kind::DATATYPE_TYPE > {
730
  typedef ::CVC4::DatatypeIndexConstant T;
731
};/* ConstantMapReverse< ::CVC4::kind::DATATYPE_TYPE > */
732
733
template <>
734
struct ConstantMap< ::CVC4::AscriptionType > {
735
  // typedef THEORY_DATATYPES OwningTheory;
736
  enum { kind = ::CVC4::kind::ASCRIPTION_TYPE };
737
};/* ConstantMap< ::CVC4::AscriptionType > */
738
739
template <>
740
struct ConstantMapReverse< ::CVC4::kind::ASCRIPTION_TYPE > {
741
  typedef ::CVC4::AscriptionType T;
742
};/* ConstantMapReverse< ::CVC4::kind::ASCRIPTION_TYPE > */
743
744
template <>
745
struct ConstantMap< ::CVC4::TupleUpdate > {
746
  // typedef THEORY_DATATYPES OwningTheory;
747
  enum { kind = ::CVC4::kind::TUPLE_UPDATE_OP };
748
};/* ConstantMap< ::CVC4::TupleUpdate > */
749
750
template <>
751
struct ConstantMapReverse< ::CVC4::kind::TUPLE_UPDATE_OP > {
752
  typedef ::CVC4::TupleUpdate T;
753
};/* ConstantMapReverse< ::CVC4::kind::TUPLE_UPDATE_OP > */
754
755
template <>
756
struct ConstantMap< ::CVC4::RecordUpdate > {
757
  // typedef THEORY_DATATYPES OwningTheory;
758
  enum { kind = ::CVC4::kind::RECORD_UPDATE_OP };
759
};/* ConstantMap< ::CVC4::RecordUpdate > */
760
761
template <>
762
struct ConstantMapReverse< ::CVC4::kind::RECORD_UPDATE_OP > {
763
  typedef ::CVC4::RecordUpdate T;
764
};/* ConstantMapReverse< ::CVC4::kind::RECORD_UPDATE_OP > */
765
766
template <>
767
struct ConstantMap< ::CVC4::TupleProjectOp > {
768
  // typedef THEORY_DATATYPES OwningTheory;
769
  enum { kind = ::CVC4::kind::TUPLE_PROJECT_OP };
770
};/* ConstantMap< ::CVC4::TupleProjectOp > */
771
772
template <>
773
struct ConstantMapReverse< ::CVC4::kind::TUPLE_PROJECT_OP > {
774
  typedef ::CVC4::TupleProjectOp T;
775
};/* ConstantMapReverse< ::CVC4::kind::TUPLE_PROJECT_OP > */
776
777
template <>
778
struct ConstantMap< ::CVC4::EmptySet > {
779
  // typedef THEORY_SETS OwningTheory;
780
  enum { kind = ::CVC4::kind::EMPTYSET };
781
};/* ConstantMap< ::CVC4::EmptySet > */
782
783
template <>
784
struct ConstantMapReverse< ::CVC4::kind::EMPTYSET > {
785
  typedef ::CVC4::EmptySet T;
786
};/* ConstantMapReverse< ::CVC4::kind::EMPTYSET > */
787
788
template <>
789
struct ConstantMap< ::CVC4::SingletonOp > {
790
  // typedef THEORY_SETS OwningTheory;
791
  enum { kind = ::CVC4::kind::SINGLETON_OP };
792
};/* ConstantMap< ::CVC4::SingletonOp > */
793
794
template <>
795
struct ConstantMapReverse< ::CVC4::kind::SINGLETON_OP > {
796
  typedef ::CVC4::SingletonOp T;
797
};/* ConstantMapReverse< ::CVC4::kind::SINGLETON_OP > */
798
799
template <>
800
struct ConstantMap< ::CVC4::EmptyBag > {
801
  // typedef THEORY_BAGS OwningTheory;
802
  enum { kind = ::CVC4::kind::EMPTYBAG };
803
};/* ConstantMap< ::CVC4::EmptyBag > */
804
805
template <>
806
struct ConstantMapReverse< ::CVC4::kind::EMPTYBAG > {
807
  typedef ::CVC4::EmptyBag T;
808
};/* ConstantMapReverse< ::CVC4::kind::EMPTYBAG > */
809
810
template <>
811
struct ConstantMap< ::CVC4::MakeBagOp > {
812
  // typedef THEORY_BAGS OwningTheory;
813
  enum { kind = ::CVC4::kind::MK_BAG_OP };
814
};/* ConstantMap< ::CVC4::MakeBagOp > */
815
816
template <>
817
struct ConstantMapReverse< ::CVC4::kind::MK_BAG_OP > {
818
  typedef ::CVC4::MakeBagOp T;
819
};/* ConstantMapReverse< ::CVC4::kind::MK_BAG_OP > */
820
821
template <>
822
struct ConstantMap< ::CVC4::String > {
823
  // typedef THEORY_STRINGS OwningTheory;
824
  enum { kind = ::CVC4::kind::CONST_STRING };
825
};/* ConstantMap< ::CVC4::String > */
826
827
template <>
828
struct ConstantMapReverse< ::CVC4::kind::CONST_STRING > {
829
  typedef ::CVC4::String T;
830
};/* ConstantMapReverse< ::CVC4::kind::CONST_STRING > */
831
832
template <>
833
struct ConstantMap< ::CVC4::Sequence > {
834
  // typedef THEORY_STRINGS OwningTheory;
835
  enum { kind = ::CVC4::kind::CONST_SEQUENCE };
836
};/* ConstantMap< ::CVC4::Sequence > */
837
838
template <>
839
struct ConstantMapReverse< ::CVC4::kind::CONST_SEQUENCE > {
840
  typedef ::CVC4::Sequence T;
841
};/* ConstantMapReverse< ::CVC4::kind::CONST_SEQUENCE > */
842
843
template <>
844
struct ConstantMap< ::CVC4::RegExpRepeat > {
845
  // typedef THEORY_STRINGS OwningTheory;
846
  enum { kind = ::CVC4::kind::REGEXP_REPEAT_OP };
847
};/* ConstantMap< ::CVC4::RegExpRepeat > */
848
849
template <>
850
struct ConstantMapReverse< ::CVC4::kind::REGEXP_REPEAT_OP > {
851
  typedef ::CVC4::RegExpRepeat T;
852
};/* ConstantMapReverse< ::CVC4::kind::REGEXP_REPEAT_OP > */
853
854
template <>
855
struct ConstantMap< ::CVC4::RegExpLoop > {
856
  // typedef THEORY_STRINGS OwningTheory;
857
  enum { kind = ::CVC4::kind::REGEXP_LOOP_OP };
858
};/* ConstantMap< ::CVC4::RegExpLoop > */
859
860
template <>
861
struct ConstantMapReverse< ::CVC4::kind::REGEXP_LOOP_OP > {
862
  typedef ::CVC4::RegExpLoop T;
863
};/* ConstantMapReverse< ::CVC4::kind::REGEXP_LOOP_OP > */
864
865
866
struct NodeValueConstPrinter {
867
  static void toStream(std::ostream& out,
868
                              const ::CVC4::expr::NodeValue* nv);
869
  static void toStream(std::ostream& out, TNode n);
870
};
871
872
/**
873
 * Cleanup to be performed when a NodeValue zombie is collected, and
874
 * it has CONSTANT metakind.  This calls the destructor for the underlying
875
 * C++ type representing the constant value.  See
876
 * NodeManager::reclaimZombies() for more information.
877
 *
878
 * This doesn't support "non-inlined" NodeValues, which shouldn't need this
879
 * kind of cleanup.
880
 */
881
void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
882
883
/** Return the minimum arity of the given kind. */
884
uint32_t getMinArityForKind(::CVC4::Kind k);
885
/** Return the maximum arity of the given kind. */
886
uint32_t getMaxArityForKind(::CVC4::Kind k);
887
888
}/* CVC4::kind::metakind namespace */
889
890
/**
891
 * Map a kind of the operator to the kind of the enclosing expression. For
892
 * example, since the kind of functions is just VARIABLE, it should map
893
 * VARIABLE to APPLY_UF.
894
 */
895
Kind operatorToKind(::CVC4::expr::NodeValue* nv);
896
897
}/* CVC4::kind namespace */
898
899
}/* CVC4 namespace */
900
901
#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */