GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/api/cvc4cpp.cpp Lines: 2217 2825 78.5 %
Date: 2021-03-23 Branches: 6421 22591 28.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cvc4cpp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The CVC4 C++ API.
13
 **
14
 ** The CVC4 C++ API.
15
 **
16
 ** A brief note on how to guard API functions:
17
 **
18
 ** In general, we think of API guards as a fence -- they are supposed to make
19
 ** sure that no invalid arguments get passed into internal realms of CVC4.
20
 ** Thus we always want to catch such cases on the API level (and can then
21
 ** assert internally that no invalid argument is passed in).
22
 **
23
 ** The only special case is when we use 3rd party back-ends we have no control
24
 ** over, and which throw (invalid_argument) exceptions anyways. In this case,
25
 ** we do not replicate argument checks but delegate them to the back-end,
26
 ** catch thrown exceptions, and raise a CVC4ApiException.
27
 **
28
 ** Our Integer implementation, e.g., is such a special case since we support
29
 ** two different back end implementations (GMP, CLN). Be aware that they do
30
 ** not fully agree on what is (in)valid input, which requires extra checks for
31
 ** consistent behavior (see Solver::mkRealFromStrHelper for an example).
32
 **/
33
34
#include "api/cvc4cpp.h"
35
36
#include <cstring>
37
#include <sstream>
38
39
#include "api/checks.h"
40
#include "base/check.h"
41
#include "base/configuration.h"
42
#include "expr/dtype.h"
43
#include "expr/dtype_cons.h"
44
#include "expr/dtype_selector.h"
45
#include "expr/kind.h"
46
#include "expr/metakind.h"
47
#include "expr/node.h"
48
#include "expr/node_manager.h"
49
#include "expr/sequence.h"
50
#include "expr/type_node.h"
51
#include "options/main_options.h"
52
#include "options/options.h"
53
#include "options/smt_options.h"
54
#include "proof/unsat_core.h"
55
#include "smt/model.h"
56
#include "smt/smt_engine.h"
57
#include "smt/smt_mode.h"
58
#include "theory/logic_info.h"
59
#include "theory/theory_model.h"
60
#include "util/random.h"
61
#include "util/result.h"
62
#include "util/statistics_registry.h"
63
#include "util/stats_histogram.h"
64
#include "util/utility.h"
65
66
namespace CVC4 {
67
namespace api {
68
69
/* -------------------------------------------------------------------------- */
70
/* Statistics                                                                 */
71
/* -------------------------------------------------------------------------- */
72
73
6099
struct Statistics
74
{
75
6120
  Statistics()
76
6120
      : d_consts("api::CONSTANT"), d_vars("api::VARIABLE"), d_terms("api::TERM")
77
  {
78
6120
  }
79
  IntegralHistogramStat<TypeConstant> d_consts;
80
  IntegralHistogramStat<TypeConstant> d_vars;
81
  IntegralHistogramStat<Kind> d_terms;
82
};
83
84
/* -------------------------------------------------------------------------- */
85
/* Kind                                                                       */
86
/* -------------------------------------------------------------------------- */
87
88
/* Mapping from external (API) kind to internal kind. */
89
8895
const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
90
    {INTERNAL_KIND, CVC4::Kind::UNDEFINED_KIND},
91
    {UNDEFINED_KIND, CVC4::Kind::UNDEFINED_KIND},
92
    {NULL_EXPR, CVC4::Kind::NULL_EXPR},
93
    /* Builtin ------------------------------------------------------------- */
94
    {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT},
95
    {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE},
96
    {EQUAL, CVC4::Kind::EQUAL},
97
    {DISTINCT, CVC4::Kind::DISTINCT},
98
    {CONSTANT, CVC4::Kind::VARIABLE},
99
    {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
100
    {SEXPR, CVC4::Kind::SEXPR},
101
    {LAMBDA, CVC4::Kind::LAMBDA},
102
    {WITNESS, CVC4::Kind::WITNESS},
103
    /* Boolean ------------------------------------------------------------- */
104
    {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
105
    {NOT, CVC4::Kind::NOT},
106
    {AND, CVC4::Kind::AND},
107
    {IMPLIES, CVC4::Kind::IMPLIES},
108
    {OR, CVC4::Kind::OR},
109
    {XOR, CVC4::Kind::XOR},
110
    {ITE, CVC4::Kind::ITE},
111
    {MATCH, CVC4::Kind::MATCH},
112
    {MATCH_CASE, CVC4::Kind::MATCH_CASE},
113
    {MATCH_BIND_CASE, CVC4::Kind::MATCH_BIND_CASE},
114
    /* UF ------------------------------------------------------------------ */
115
    {APPLY_UF, CVC4::Kind::APPLY_UF},
116
    {CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT},
117
    {CARDINALITY_VALUE, CVC4::Kind::CARDINALITY_VALUE},
118
    {HO_APPLY, CVC4::Kind::HO_APPLY},
119
    /* Arithmetic ---------------------------------------------------------- */
120
    {PLUS, CVC4::Kind::PLUS},
121
    {MULT, CVC4::Kind::MULT},
122
    {IAND, CVC4::Kind::IAND},
123
    {MINUS, CVC4::Kind::MINUS},
124
    {UMINUS, CVC4::Kind::UMINUS},
125
    {DIVISION, CVC4::Kind::DIVISION},
126
    {INTS_DIVISION, CVC4::Kind::INTS_DIVISION},
127
    {INTS_MODULUS, CVC4::Kind::INTS_MODULUS},
128
    {ABS, CVC4::Kind::ABS},
129
    {DIVISIBLE, CVC4::Kind::DIVISIBLE},
130
    {POW, CVC4::Kind::POW},
131
    {EXPONENTIAL, CVC4::Kind::EXPONENTIAL},
132
    {SINE, CVC4::Kind::SINE},
133
    {COSINE, CVC4::Kind::COSINE},
134
    {TANGENT, CVC4::Kind::TANGENT},
135
    {COSECANT, CVC4::Kind::COSECANT},
136
    {SECANT, CVC4::Kind::SECANT},
137
    {COTANGENT, CVC4::Kind::COTANGENT},
138
    {ARCSINE, CVC4::Kind::ARCSINE},
139
    {ARCCOSINE, CVC4::Kind::ARCCOSINE},
140
    {ARCTANGENT, CVC4::Kind::ARCTANGENT},
141
    {ARCCOSECANT, CVC4::Kind::ARCCOSECANT},
142
    {ARCSECANT, CVC4::Kind::ARCSECANT},
143
    {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
144
    {SQRT, CVC4::Kind::SQRT},
145
    {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
146
    {LT, CVC4::Kind::LT},
147
    {LEQ, CVC4::Kind::LEQ},
148
    {GT, CVC4::Kind::GT},
149
    {GEQ, CVC4::Kind::GEQ},
150
    {IS_INTEGER, CVC4::Kind::IS_INTEGER},
151
    {TO_INTEGER, CVC4::Kind::TO_INTEGER},
152
    {TO_REAL, CVC4::Kind::TO_REAL},
153
    {PI, CVC4::Kind::PI},
154
    /* BV ------------------------------------------------------------------ */
155
    {CONST_BITVECTOR, CVC4::Kind::CONST_BITVECTOR},
156
    {BITVECTOR_CONCAT, CVC4::Kind::BITVECTOR_CONCAT},
157
    {BITVECTOR_AND, CVC4::Kind::BITVECTOR_AND},
158
    {BITVECTOR_OR, CVC4::Kind::BITVECTOR_OR},
159
    {BITVECTOR_XOR, CVC4::Kind::BITVECTOR_XOR},
160
    {BITVECTOR_NOT, CVC4::Kind::BITVECTOR_NOT},
161
    {BITVECTOR_NAND, CVC4::Kind::BITVECTOR_NAND},
162
    {BITVECTOR_NOR, CVC4::Kind::BITVECTOR_NOR},
163
    {BITVECTOR_XNOR, CVC4::Kind::BITVECTOR_XNOR},
164
    {BITVECTOR_COMP, CVC4::Kind::BITVECTOR_COMP},
165
    {BITVECTOR_MULT, CVC4::Kind::BITVECTOR_MULT},
166
    {BITVECTOR_PLUS, CVC4::Kind::BITVECTOR_PLUS},
167
    {BITVECTOR_SUB, CVC4::Kind::BITVECTOR_SUB},
168
    {BITVECTOR_NEG, CVC4::Kind::BITVECTOR_NEG},
169
    {BITVECTOR_UDIV, CVC4::Kind::BITVECTOR_UDIV},
170
    {BITVECTOR_UREM, CVC4::Kind::BITVECTOR_UREM},
171
    {BITVECTOR_SDIV, CVC4::Kind::BITVECTOR_SDIV},
172
    {BITVECTOR_SREM, CVC4::Kind::BITVECTOR_SREM},
173
    {BITVECTOR_SMOD, CVC4::Kind::BITVECTOR_SMOD},
174
    {BITVECTOR_SHL, CVC4::Kind::BITVECTOR_SHL},
175
    {BITVECTOR_LSHR, CVC4::Kind::BITVECTOR_LSHR},
176
    {BITVECTOR_ASHR, CVC4::Kind::BITVECTOR_ASHR},
177
    {BITVECTOR_ULT, CVC4::Kind::BITVECTOR_ULT},
178
    {BITVECTOR_ULE, CVC4::Kind::BITVECTOR_ULE},
179
    {BITVECTOR_UGT, CVC4::Kind::BITVECTOR_UGT},
180
    {BITVECTOR_UGE, CVC4::Kind::BITVECTOR_UGE},
181
    {BITVECTOR_SLT, CVC4::Kind::BITVECTOR_SLT},
182
    {BITVECTOR_SLE, CVC4::Kind::BITVECTOR_SLE},
183
    {BITVECTOR_SGT, CVC4::Kind::BITVECTOR_SGT},
184
    {BITVECTOR_SGE, CVC4::Kind::BITVECTOR_SGE},
185
    {BITVECTOR_ULTBV, CVC4::Kind::BITVECTOR_ULTBV},
186
    {BITVECTOR_SLTBV, CVC4::Kind::BITVECTOR_SLTBV},
187
    {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
188
    {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
189
    {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
190
    {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
191
    {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
192
    {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
193
    {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
194
    {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
195
    {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
196
    {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
197
    {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
198
    /* FP ------------------------------------------------------------------ */
199
    {CONST_FLOATINGPOINT, CVC4::Kind::CONST_FLOATINGPOINT},
200
    {CONST_ROUNDINGMODE, CVC4::Kind::CONST_ROUNDINGMODE},
201
    {FLOATINGPOINT_FP, CVC4::Kind::FLOATINGPOINT_FP},
202
    {FLOATINGPOINT_EQ, CVC4::Kind::FLOATINGPOINT_EQ},
203
    {FLOATINGPOINT_ABS, CVC4::Kind::FLOATINGPOINT_ABS},
204
    {FLOATINGPOINT_NEG, CVC4::Kind::FLOATINGPOINT_NEG},
205
    {FLOATINGPOINT_PLUS, CVC4::Kind::FLOATINGPOINT_PLUS},
206
    {FLOATINGPOINT_SUB, CVC4::Kind::FLOATINGPOINT_SUB},
207
    {FLOATINGPOINT_MULT, CVC4::Kind::FLOATINGPOINT_MULT},
208
    {FLOATINGPOINT_DIV, CVC4::Kind::FLOATINGPOINT_DIV},
209
    {FLOATINGPOINT_FMA, CVC4::Kind::FLOATINGPOINT_FMA},
210
    {FLOATINGPOINT_SQRT, CVC4::Kind::FLOATINGPOINT_SQRT},
211
    {FLOATINGPOINT_REM, CVC4::Kind::FLOATINGPOINT_REM},
212
    {FLOATINGPOINT_RTI, CVC4::Kind::FLOATINGPOINT_RTI},
213
    {FLOATINGPOINT_MIN, CVC4::Kind::FLOATINGPOINT_MIN},
214
    {FLOATINGPOINT_MAX, CVC4::Kind::FLOATINGPOINT_MAX},
215
    {FLOATINGPOINT_LEQ, CVC4::Kind::FLOATINGPOINT_LEQ},
216
    {FLOATINGPOINT_LT, CVC4::Kind::FLOATINGPOINT_LT},
217
    {FLOATINGPOINT_GEQ, CVC4::Kind::FLOATINGPOINT_GEQ},
218
    {FLOATINGPOINT_GT, CVC4::Kind::FLOATINGPOINT_GT},
219
    {FLOATINGPOINT_ISN, CVC4::Kind::FLOATINGPOINT_ISN},
220
    {FLOATINGPOINT_ISSN, CVC4::Kind::FLOATINGPOINT_ISSN},
221
    {FLOATINGPOINT_ISZ, CVC4::Kind::FLOATINGPOINT_ISZ},
222
    {FLOATINGPOINT_ISINF, CVC4::Kind::FLOATINGPOINT_ISINF},
223
    {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
224
    {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
225
    {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
226
    {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
227
     CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
228
    {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
229
    {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
230
     CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
231
    {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
232
     CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
233
    {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
234
    {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
235
    {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
236
    {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
237
    /* Arrays -------------------------------------------------------------- */
238
    {SELECT, CVC4::Kind::SELECT},
239
    {STORE, CVC4::Kind::STORE},
240
    {CONST_ARRAY, CVC4::Kind::STORE_ALL},
241
    {EQ_RANGE, CVC4::Kind::EQ_RANGE},
242
    /* Datatypes ----------------------------------------------------------- */
243
    {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
244
    {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
245
    {APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
246
    {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
247
    {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
248
    {DT_SIZE, CVC4::Kind::DT_SIZE},
249
    {TUPLE_PROJECT, CVC4::Kind::TUPLE_PROJECT},
250
    /* Separation Logic ---------------------------------------------------- */
251
    {SEP_NIL, CVC4::Kind::SEP_NIL},
252
    {SEP_EMP, CVC4::Kind::SEP_EMP},
253
    {SEP_PTO, CVC4::Kind::SEP_PTO},
254
    {SEP_STAR, CVC4::Kind::SEP_STAR},
255
    {SEP_WAND, CVC4::Kind::SEP_WAND},
256
    /* Sets ---------------------------------------------------------------- */
257
    {EMPTYSET, CVC4::Kind::EMPTYSET},
258
    {UNION, CVC4::Kind::UNION},
259
    {INTERSECTION, CVC4::Kind::INTERSECTION},
260
    {SETMINUS, CVC4::Kind::SETMINUS},
261
    {SUBSET, CVC4::Kind::SUBSET},
262
    {MEMBER, CVC4::Kind::MEMBER},
263
    {SINGLETON, CVC4::Kind::SINGLETON},
264
    {INSERT, CVC4::Kind::INSERT},
265
    {CARD, CVC4::Kind::CARD},
266
    {COMPLEMENT, CVC4::Kind::COMPLEMENT},
267
    {UNIVERSE_SET, CVC4::Kind::UNIVERSE_SET},
268
    {JOIN, CVC4::Kind::JOIN},
269
    {PRODUCT, CVC4::Kind::PRODUCT},
270
    {TRANSPOSE, CVC4::Kind::TRANSPOSE},
271
    {TCLOSURE, CVC4::Kind::TCLOSURE},
272
    {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE},
273
    {IDEN, CVC4::Kind::IDEN},
274
    {COMPREHENSION, CVC4::Kind::COMPREHENSION},
275
    {CHOOSE, CVC4::Kind::CHOOSE},
276
    {IS_SINGLETON, CVC4::Kind::IS_SINGLETON},
277
    /* Bags ---------------------------------------------------------------- */
278
    {UNION_MAX, CVC4::Kind::UNION_MAX},
279
    {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT},
280
    {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN},
281
    {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT},
282
    {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE},
283
    {SUBBAG, CVC4::Kind::SUBBAG},
284
    {BAG_COUNT, CVC4::Kind::BAG_COUNT},
285
    {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL},
286
    {MK_BAG, CVC4::Kind::MK_BAG},
287
    {EMPTYBAG, CVC4::Kind::EMPTYBAG},
288
    {BAG_CARD, CVC4::Kind::BAG_CARD},
289
    {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE},
290
    {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON},
291
    {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET},
292
    {BAG_TO_SET, CVC4::Kind::BAG_TO_SET},
293
    /* Strings ------------------------------------------------------------- */
294
    {STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
295
    {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
296
    {STRING_LENGTH, CVC4::Kind::STRING_LENGTH},
297
    {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR},
298
    {STRING_UPDATE, CVC4::Kind::STRING_UPDATE},
299
    {STRING_CHARAT, CVC4::Kind::STRING_CHARAT},
300
    {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN},
301
    {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF},
302
    {STRING_REPLACE, CVC4::Kind::STRING_STRREPL},
303
    {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL},
304
    {STRING_REPLACE_RE, CVC4::Kind::STRING_REPLACE_RE},
305
    {STRING_REPLACE_RE_ALL, CVC4::Kind::STRING_REPLACE_RE_ALL},
306
    {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER},
307
    {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER},
308
    {STRING_REV, CVC4::Kind::STRING_REV},
309
    {STRING_FROM_CODE, CVC4::Kind::STRING_FROM_CODE},
310
    {STRING_TO_CODE, CVC4::Kind::STRING_TO_CODE},
311
    {STRING_LT, CVC4::Kind::STRING_LT},
312
    {STRING_LEQ, CVC4::Kind::STRING_LEQ},
313
    {STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
314
    {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
315
    {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT},
316
    {STRING_FROM_INT, CVC4::Kind::STRING_ITOS},
317
    {STRING_TO_INT, CVC4::Kind::STRING_STOI},
318
    {CONST_STRING, CVC4::Kind::CONST_STRING},
319
    {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP},
320
    {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT},
321
    {REGEXP_UNION, CVC4::Kind::REGEXP_UNION},
322
    {REGEXP_INTER, CVC4::Kind::REGEXP_INTER},
323
    {REGEXP_DIFF, CVC4::Kind::REGEXP_DIFF},
324
    {REGEXP_STAR, CVC4::Kind::REGEXP_STAR},
325
    {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
326
    {REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
327
    {REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
328
    {REGEXP_REPEAT, CVC4::Kind::REGEXP_REPEAT},
329
    {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
330
    {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
331
    {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
332
    {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT},
333
    // maps to the same kind as the string versions
334
    {SEQ_CONCAT, CVC4::Kind::STRING_CONCAT},
335
    {SEQ_LENGTH, CVC4::Kind::STRING_LENGTH},
336
    {SEQ_EXTRACT, CVC4::Kind::STRING_SUBSTR},
337
    {SEQ_UPDATE, CVC4::Kind::STRING_UPDATE},
338
    {SEQ_AT, CVC4::Kind::STRING_CHARAT},
339
    {SEQ_CONTAINS, CVC4::Kind::STRING_STRCTN},
340
    {SEQ_INDEXOF, CVC4::Kind::STRING_STRIDOF},
341
    {SEQ_REPLACE, CVC4::Kind::STRING_STRREPL},
342
    {SEQ_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL},
343
    {SEQ_REV, CVC4::Kind::STRING_REV},
344
    {SEQ_PREFIX, CVC4::Kind::STRING_PREFIX},
345
    {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX},
346
    {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE},
347
    {SEQ_UNIT, CVC4::Kind::SEQ_UNIT},
348
    {SEQ_NTH, CVC4::Kind::SEQ_NTH},
349
    /* Quantifiers --------------------------------------------------------- */
350
    {FORALL, CVC4::Kind::FORALL},
351
    {EXISTS, CVC4::Kind::EXISTS},
352
    {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST},
353
    {INST_PATTERN, CVC4::Kind::INST_PATTERN},
354
    {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN},
355
    {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE},
356
    {INST_PATTERN_LIST, CVC4::Kind::INST_PATTERN_LIST},
357
    {LAST_KIND, CVC4::Kind::LAST_KIND},
358
};
359
360
/* Mapping from internal kind to external (API) kind. */
361
const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
362
8895
    s_kinds_internal{
363
        {CVC4::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
364
        {CVC4::Kind::NULL_EXPR, NULL_EXPR},
365
        /* Builtin --------------------------------------------------------- */
366
        {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
367
        {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
368
        {CVC4::Kind::EQUAL, EQUAL},
369
        {CVC4::Kind::DISTINCT, DISTINCT},
370
        {CVC4::Kind::VARIABLE, CONSTANT},
371
        {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
372
        {CVC4::Kind::SEXPR, SEXPR},
373
        {CVC4::Kind::LAMBDA, LAMBDA},
374
        {CVC4::Kind::WITNESS, WITNESS},
375
        /* Boolean --------------------------------------------------------- */
376
        {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
377
        {CVC4::Kind::NOT, NOT},
378
        {CVC4::Kind::AND, AND},
379
        {CVC4::Kind::IMPLIES, IMPLIES},
380
        {CVC4::Kind::OR, OR},
381
        {CVC4::Kind::XOR, XOR},
382
        {CVC4::Kind::ITE, ITE},
383
        {CVC4::Kind::MATCH, MATCH},
384
        {CVC4::Kind::MATCH_CASE, MATCH_CASE},
385
        {CVC4::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE},
386
        /* UF -------------------------------------------------------------- */
387
        {CVC4::Kind::APPLY_UF, APPLY_UF},
388
        {CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
389
        {CVC4::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE},
390
        {CVC4::Kind::HO_APPLY, HO_APPLY},
391
        /* Arithmetic ------------------------------------------------------ */
392
        {CVC4::Kind::PLUS, PLUS},
393
        {CVC4::Kind::MULT, MULT},
394
        {CVC4::Kind::IAND, IAND},
395
        {CVC4::Kind::MINUS, MINUS},
396
        {CVC4::Kind::UMINUS, UMINUS},
397
        {CVC4::Kind::DIVISION, DIVISION},
398
        {CVC4::Kind::DIVISION_TOTAL, INTERNAL_KIND},
399
        {CVC4::Kind::INTS_DIVISION, INTS_DIVISION},
400
        {CVC4::Kind::INTS_DIVISION_TOTAL, INTERNAL_KIND},
401
        {CVC4::Kind::INTS_MODULUS, INTS_MODULUS},
402
        {CVC4::Kind::INTS_MODULUS_TOTAL, INTERNAL_KIND},
403
        {CVC4::Kind::ABS, ABS},
404
        {CVC4::Kind::DIVISIBLE, DIVISIBLE},
405
        {CVC4::Kind::POW, POW},
406
        {CVC4::Kind::EXPONENTIAL, EXPONENTIAL},
407
        {CVC4::Kind::SINE, SINE},
408
        {CVC4::Kind::COSINE, COSINE},
409
        {CVC4::Kind::TANGENT, TANGENT},
410
        {CVC4::Kind::COSECANT, COSECANT},
411
        {CVC4::Kind::SECANT, SECANT},
412
        {CVC4::Kind::COTANGENT, COTANGENT},
413
        {CVC4::Kind::ARCSINE, ARCSINE},
414
        {CVC4::Kind::ARCCOSINE, ARCCOSINE},
415
        {CVC4::Kind::ARCTANGENT, ARCTANGENT},
416
        {CVC4::Kind::ARCCOSECANT, ARCCOSECANT},
417
        {CVC4::Kind::ARCSECANT, ARCSECANT},
418
        {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
419
        {CVC4::Kind::SQRT, SQRT},
420
        {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE},
421
        {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
422
        {CVC4::Kind::LT, LT},
423
        {CVC4::Kind::LEQ, LEQ},
424
        {CVC4::Kind::GT, GT},
425
        {CVC4::Kind::GEQ, GEQ},
426
        {CVC4::Kind::IS_INTEGER, IS_INTEGER},
427
        {CVC4::Kind::TO_INTEGER, TO_INTEGER},
428
        {CVC4::Kind::TO_REAL, TO_REAL},
429
        {CVC4::Kind::PI, PI},
430
        /* BV -------------------------------------------------------------- */
431
        {CVC4::Kind::CONST_BITVECTOR, CONST_BITVECTOR},
432
        {CVC4::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT},
433
        {CVC4::Kind::BITVECTOR_AND, BITVECTOR_AND},
434
        {CVC4::Kind::BITVECTOR_OR, BITVECTOR_OR},
435
        {CVC4::Kind::BITVECTOR_XOR, BITVECTOR_XOR},
436
        {CVC4::Kind::BITVECTOR_NOT, BITVECTOR_NOT},
437
        {CVC4::Kind::BITVECTOR_NAND, BITVECTOR_NAND},
438
        {CVC4::Kind::BITVECTOR_NOR, BITVECTOR_NOR},
439
        {CVC4::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR},
440
        {CVC4::Kind::BITVECTOR_COMP, BITVECTOR_COMP},
441
        {CVC4::Kind::BITVECTOR_MULT, BITVECTOR_MULT},
442
        {CVC4::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS},
443
        {CVC4::Kind::BITVECTOR_SUB, BITVECTOR_SUB},
444
        {CVC4::Kind::BITVECTOR_NEG, BITVECTOR_NEG},
445
        {CVC4::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV},
446
        {CVC4::Kind::BITVECTOR_UREM, BITVECTOR_UREM},
447
        {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV},
448
        {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM},
449
        {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD},
450
        {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL},
451
        {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR},
452
        {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR},
453
        {CVC4::Kind::BITVECTOR_ULT, BITVECTOR_ULT},
454
        {CVC4::Kind::BITVECTOR_ULE, BITVECTOR_ULE},
455
        {CVC4::Kind::BITVECTOR_UGT, BITVECTOR_UGT},
456
        {CVC4::Kind::BITVECTOR_UGE, BITVECTOR_UGE},
457
        {CVC4::Kind::BITVECTOR_SLT, BITVECTOR_SLT},
458
        {CVC4::Kind::BITVECTOR_SLE, BITVECTOR_SLE},
459
        {CVC4::Kind::BITVECTOR_SGT, BITVECTOR_SGT},
460
        {CVC4::Kind::BITVECTOR_SGE, BITVECTOR_SGE},
461
        {CVC4::Kind::BITVECTOR_ULTBV, BITVECTOR_ULTBV},
462
        {CVC4::Kind::BITVECTOR_SLTBV, BITVECTOR_SLTBV},
463
        {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
464
        {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
465
        {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
466
        {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT},
467
        {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT},
468
        {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND},
469
        {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND},
470
        {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT},
471
        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT},
472
        {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
473
        {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
474
        {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
475
        {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
476
        {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
477
        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
478
        {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR},
479
        {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
480
        {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
481
        /* FP -------------------------------------------------------------- */
482
        {CVC4::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT},
483
        {CVC4::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE},
484
        {CVC4::Kind::FLOATINGPOINT_FP, FLOATINGPOINT_FP},
485
        {CVC4::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ},
486
        {CVC4::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS},
487
        {CVC4::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG},
488
        {CVC4::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS},
489
        {CVC4::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB},
490
        {CVC4::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT},
491
        {CVC4::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV},
492
        {CVC4::Kind::FLOATINGPOINT_FMA, FLOATINGPOINT_FMA},
493
        {CVC4::Kind::FLOATINGPOINT_SQRT, FLOATINGPOINT_SQRT},
494
        {CVC4::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM},
495
        {CVC4::Kind::FLOATINGPOINT_RTI, FLOATINGPOINT_RTI},
496
        {CVC4::Kind::FLOATINGPOINT_MIN, FLOATINGPOINT_MIN},
497
        {CVC4::Kind::FLOATINGPOINT_MAX, FLOATINGPOINT_MAX},
498
        {CVC4::Kind::FLOATINGPOINT_LEQ, FLOATINGPOINT_LEQ},
499
        {CVC4::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
500
        {CVC4::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ},
501
        {CVC4::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT},
502
        {CVC4::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN},
503
        {CVC4::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN},
504
        {CVC4::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ},
505
        {CVC4::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF},
506
        {CVC4::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN},
507
        {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
508
        {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
509
        {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
510
         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
511
        {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
512
         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
513
        {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
514
         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
515
        {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
516
         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
517
        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL},
518
        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
519
        {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
520
         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
521
        {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
522
         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
523
        {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
524
         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
525
        {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
526
         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
527
        {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
528
         FLOATINGPOINT_TO_FP_GENERIC},
529
        {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
530
        {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV},
531
        {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
532
        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND},
533
        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, INTERNAL_KIND},
534
        {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV},
535
        {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
536
        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, INTERNAL_KIND},
537
        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, INTERNAL_KIND},
538
        {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
539
        {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND},
540
        /* Arrays ---------------------------------------------------------- */
541
        {CVC4::Kind::SELECT, SELECT},
542
        {CVC4::Kind::STORE, STORE},
543
        {CVC4::Kind::STORE_ALL, CONST_ARRAY},
544
        /* Datatypes ------------------------------------------------------- */
545
        {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
546
        {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
547
        {CVC4::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND},
548
        {CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
549
        {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE},
550
        {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
551
        {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
552
        {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
553
        {CVC4::Kind::DT_SIZE, DT_SIZE},
554
        {CVC4::Kind::TUPLE_PROJECT, TUPLE_PROJECT},
555
        /* Separation Logic ------------------------------------------------ */
556
        {CVC4::Kind::SEP_NIL, SEP_NIL},
557
        {CVC4::Kind::SEP_EMP, SEP_EMP},
558
        {CVC4::Kind::SEP_PTO, SEP_PTO},
559
        {CVC4::Kind::SEP_STAR, SEP_STAR},
560
        {CVC4::Kind::SEP_WAND, SEP_WAND},
561
        /* Sets ------------------------------------------------------------ */
562
        {CVC4::Kind::EMPTYSET, EMPTYSET},
563
        {CVC4::Kind::UNION, UNION},
564
        {CVC4::Kind::INTERSECTION, INTERSECTION},
565
        {CVC4::Kind::SETMINUS, SETMINUS},
566
        {CVC4::Kind::SUBSET, SUBSET},
567
        {CVC4::Kind::MEMBER, MEMBER},
568
        {CVC4::Kind::SINGLETON, SINGLETON},
569
        {CVC4::Kind::INSERT, INSERT},
570
        {CVC4::Kind::CARD, CARD},
571
        {CVC4::Kind::COMPLEMENT, COMPLEMENT},
572
        {CVC4::Kind::UNIVERSE_SET, UNIVERSE_SET},
573
        {CVC4::Kind::JOIN, JOIN},
574
        {CVC4::Kind::PRODUCT, PRODUCT},
575
        {CVC4::Kind::TRANSPOSE, TRANSPOSE},
576
        {CVC4::Kind::TCLOSURE, TCLOSURE},
577
        {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE},
578
        {CVC4::Kind::IDEN, IDEN},
579
        {CVC4::Kind::COMPREHENSION, COMPREHENSION},
580
        {CVC4::Kind::CHOOSE, CHOOSE},
581
        {CVC4::Kind::IS_SINGLETON, IS_SINGLETON},
582
        /* Bags ------------------------------------------------------------ */
583
        {CVC4::Kind::UNION_MAX, UNION_MAX},
584
        {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT},
585
        {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN},
586
        {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT},
587
        {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE},
588
        {CVC4::Kind::SUBBAG, SUBBAG},
589
        {CVC4::Kind::BAG_COUNT, BAG_COUNT},
590
        {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL},
591
        {CVC4::Kind::MK_BAG, MK_BAG},
592
        {CVC4::Kind::EMPTYBAG, EMPTYBAG},
593
        {CVC4::Kind::BAG_CARD, BAG_CARD},
594
        {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE},
595
        {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON},
596
        {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET},
597
        {CVC4::Kind::BAG_TO_SET, BAG_TO_SET},
598
        /* Strings --------------------------------------------------------- */
599
        {CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
600
        {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
601
        {CVC4::Kind::STRING_LENGTH, STRING_LENGTH},
602
        {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR},
603
        {CVC4::Kind::STRING_UPDATE, STRING_UPDATE},
604
        {CVC4::Kind::STRING_CHARAT, STRING_CHARAT},
605
        {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS},
606
        {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF},
607
        {CVC4::Kind::STRING_STRREPL, STRING_REPLACE},
608
        {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL},
609
        {CVC4::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE},
610
        {CVC4::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL},
611
        {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER},
612
        {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER},
613
        {CVC4::Kind::STRING_REV, STRING_REV},
614
        {CVC4::Kind::STRING_FROM_CODE, STRING_FROM_CODE},
615
        {CVC4::Kind::STRING_TO_CODE, STRING_TO_CODE},
616
        {CVC4::Kind::STRING_LT, STRING_LT},
617
        {CVC4::Kind::STRING_LEQ, STRING_LEQ},
618
        {CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
619
        {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
620
        {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT},
621
        {CVC4::Kind::STRING_ITOS, STRING_FROM_INT},
622
        {CVC4::Kind::STRING_STOI, STRING_TO_INT},
623
        {CVC4::Kind::CONST_STRING, CONST_STRING},
624
        {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP},
625
        {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT},
626
        {CVC4::Kind::REGEXP_UNION, REGEXP_UNION},
627
        {CVC4::Kind::REGEXP_INTER, REGEXP_INTER},
628
        {CVC4::Kind::REGEXP_DIFF, REGEXP_DIFF},
629
        {CVC4::Kind::REGEXP_STAR, REGEXP_STAR},
630
        {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
631
        {CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
632
        {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
633
        {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT},
634
        {CVC4::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT},
635
        {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
636
        {CVC4::Kind::REGEXP_LOOP_OP, REGEXP_LOOP},
637
        {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
638
        {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
639
        {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT},
640
        {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE},
641
        {CVC4::Kind::SEQ_UNIT, SEQ_UNIT},
642
        {CVC4::Kind::SEQ_NTH, SEQ_NTH},
643
        /* Quantifiers ----------------------------------------------------- */
644
        {CVC4::Kind::FORALL, FORALL},
645
        {CVC4::Kind::EXISTS, EXISTS},
646
        {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
647
        {CVC4::Kind::INST_PATTERN, INST_PATTERN},
648
        {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
649
        {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
650
        {CVC4::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST},
651
        /* ----------------------------------------------------------------- */
652
        {CVC4::Kind::LAST_KIND, LAST_KIND},
653
    };
654
655
/* Set of kinds for indexed operators */
656
8895
const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
657
    {RECORD_UPDATE,
658
     DIVISIBLE,
659
     IAND,
660
     BITVECTOR_REPEAT,
661
     BITVECTOR_ZERO_EXTEND,
662
     BITVECTOR_SIGN_EXTEND,
663
     BITVECTOR_ROTATE_LEFT,
664
     BITVECTOR_ROTATE_RIGHT,
665
     INT_TO_BITVECTOR,
666
     FLOATINGPOINT_TO_UBV,
667
     FLOATINGPOINT_TO_SBV,
668
     TUPLE_UPDATE,
669
     BITVECTOR_EXTRACT,
670
     FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
671
     FLOATINGPOINT_TO_FP_FLOATINGPOINT,
672
     FLOATINGPOINT_TO_FP_REAL,
673
     FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
674
     FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
675
     FLOATINGPOINT_TO_FP_GENERIC});
676
677
namespace {
678
679
/** Convert a CVC4::Kind (internal) to a CVC4::api::Kind (external). */
680
5000
CVC4::api::Kind intToExtKind(CVC4::Kind k)
681
{
682
5000
  auto it = api::s_kinds_internal.find(k);
683
5000
  if (it == api::s_kinds_internal.end())
684
  {
685
1054
    return api::INTERNAL_KIND;
686
  }
687
3946
  return it->second;
688
}
689
690
/** Convert a CVC4::api::Kind (external) to a CVC4::Kind (internal). */
691
22087079
CVC4::Kind extToIntKind(CVC4::api::Kind k)
692
{
693
22087079
  auto it = api::s_kinds.find(k);
694
22087079
  if (it == api::s_kinds.end())
695
  {
696
    return CVC4::Kind::UNDEFINED_KIND;
697
  }
698
22087079
  return it->second;
699
}
700
701
/** Return true if given kind is a defined external kind. */
702
10373341
bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
703
704
/**
705
 * Return true if the internal kind is one where the API term structure
706
 * differs from internal structure. This happens for APPLY_* kinds.
707
 * The API takes a "higher-order" perspective and treats functions as well
708
 * as datatype constructors/selectors/testers as terms
709
 * but interally they are not
710
 */
711
4687003
bool isApplyKind(CVC4::Kind k)
712
{
713
4066515
  return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR
714
8734310
          || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER);
715
}
716
717
#ifdef CVC4_ASSERTIONS
718
/** Return true if given kind is a defined internal kind. */
719
7027477
bool isDefinedIntKind(CVC4::Kind k)
720
{
721
7027477
  return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND;
722
}
723
#endif
724
725
/** Return the minimum arity of given kind. */
726
2342503
uint32_t minArity(Kind k)
727
{
728
2342503
  Assert(isDefinedKind(k));
729
2342503
  Assert(isDefinedIntKind(extToIntKind(k)));
730
2342503
  uint32_t min = CVC4::kind::metakind::getMinArityForKind(extToIntKind(k));
731
732
  // At the API level, we treat functions/constructors/selectors/testers as
733
  // normal terms instead of making them part of the operator
734
2342503
  if (isApplyKind(extToIntKind(k)))
735
  {
736
329992
    min++;
737
  }
738
2342503
  return min;
739
}
740
741
/** Return the maximum arity of given kind. */
742
2342489
uint32_t maxArity(Kind k)
743
{
744
2342489
  Assert(isDefinedKind(k));
745
2342489
  Assert(isDefinedIntKind(extToIntKind(k)));
746
2342489
  uint32_t max = CVC4::kind::metakind::getMaxArityForKind(extToIntKind(k));
747
748
  // At the API level, we treat functions/constructors/selectors/testers as
749
  // normal terms instead of making them part of the operator
750
4684978
  if (isApplyKind(extToIntKind(k))
751
2342489
      && max != std::numeric_limits<uint32_t>::max())  // be careful not to
752
                                                       // overflow
753
  {
754
329986
    max++;
755
  }
756
2342489
  return max;
757
}
758
759
}  // namespace
760
761
62
std::string kindToString(Kind k)
762
{
763
  return k == INTERNAL_KIND ? "INTERNAL_KIND"
764
62
                            : CVC4::kind::kindToString(extToIntKind(k));
765
}
766
767
2660
std::ostream& operator<<(std::ostream& out, Kind k)
768
{
769
2660
  switch (k)
770
  {
771
    case INTERNAL_KIND: out << "INTERNAL_KIND"; break;
772
2660
    default: out << extToIntKind(k);
773
  }
774
2660
  return out;
775
}
776
777
24488735
size_t KindHashFunction::operator()(Kind k) const { return k; }
778
779
/* -------------------------------------------------------------------------- */
780
/* API guard helpers                                                          */
781
/* -------------------------------------------------------------------------- */
782
783
namespace {
784
785
class CVC4ApiExceptionStream
786
{
787
 public:
788
749
  CVC4ApiExceptionStream() {}
789
  /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
790
   * a destructor that throws an exception and in C++11 all destructors
791
   * default to noexcept(true) (else this triggers a call to std::terminate). */
792
749
  ~CVC4ApiExceptionStream() noexcept(false)
793
749
  {
794
749
    if (std::uncaught_exceptions() == 0)
795
    {
796
749
      throw CVC4ApiException(d_stream.str());
797
    }
798
  }
799
800
749
  std::ostream& ostream() { return d_stream; }
801
802
 private:
803
  std::stringstream d_stream;
804
};
805
806
class CVC4ApiRecoverableExceptionStream
807
{
808
 public:
809
37
  CVC4ApiRecoverableExceptionStream() {}
810
  /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
811
   * a destructor that throws an exception and in C++11 all destructors
812
   * default to noexcept(true) (else this triggers a call to std::terminate). */
813
37
  ~CVC4ApiRecoverableExceptionStream() noexcept(false)
814
37
  {
815
37
    if (std::uncaught_exceptions() == 0)
816
    {
817
37
      throw CVC4ApiRecoverableException(d_stream.str());
818
    }
819
  }
820
821
37
  std::ostream& ostream() { return d_stream; }
822
823
 private:
824
  std::stringstream d_stream;
825
};
826
827
#define CVC4_API_TRY_CATCH_BEGIN \
828
  try                            \
829
  {
830
#define CVC4_API_TRY_CATCH_END                                                 \
831
  }                                                                            \
832
  catch (const UnrecognizedOptionException& e)                                 \
833
  {                                                                            \
834
    throw CVC4ApiRecoverableException(e.getMessage());                         \
835
  }                                                                            \
836
  catch (const CVC4::RecoverableModalException& e)                             \
837
  {                                                                            \
838
    throw CVC4ApiRecoverableException(e.getMessage());                         \
839
  }                                                                            \
840
  catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
841
  catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
842
843
}  // namespace
844
845
/* -------------------------------------------------------------------------- */
846
/* Result                                                                     */
847
/* -------------------------------------------------------------------------- */
848
849
9084
Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
850
851
303088
Result::Result() : d_result(new CVC4::Result()) {}
852
853
4
bool Result::isNull() const
854
{
855
4
  return d_result->getType() == CVC4::Result::TYPE_NONE;
856
}
857
858
143
bool Result::isSat(void) const
859
{
860
143
  return d_result->getType() == CVC4::Result::TYPE_SAT
861
143
         && d_result->isSat() == CVC4::Result::SAT;
862
}
863
864
283868
bool Result::isUnsat(void) const
865
{
866
283868
  return d_result->getType() == CVC4::Result::TYPE_SAT
867
283868
         && d_result->isSat() == CVC4::Result::UNSAT;
868
}
869
870
131
bool Result::isSatUnknown(void) const
871
{
872
131
  return d_result->getType() == CVC4::Result::TYPE_SAT
873
131
         && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
874
}
875
876
279699
bool Result::isEntailed(void) const
877
{
878
279699
  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
879
279699
         && d_result->isEntailed() == CVC4::Result::ENTAILED;
880
}
881
882
4
bool Result::isNotEntailed(void) const
883
{
884
4
  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
885
4
         && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED;
886
}
887
888
8
bool Result::isEntailmentUnknown(void) const
889
{
890
8
  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
891
8
         && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN;
892
}
893
894
4
bool Result::operator==(const Result& r) const
895
{
896
4
  return *d_result == *r.d_result;
897
}
898
899
bool Result::operator!=(const Result& r) const
900
{
901
  return *d_result != *r.d_result;
902
}
903
904
2
Result::UnknownExplanation Result::getUnknownExplanation(void) const
905
{
906
2
  CVC4::Result::UnknownExplanation expl = d_result->whyUnknown();
907
2
  switch (expl)
908
  {
909
    case CVC4::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK;
910
    case CVC4::Result::INCOMPLETE: return INCOMPLETE;
911
    case CVC4::Result::TIMEOUT: return TIMEOUT;
912
    case CVC4::Result::RESOURCEOUT: return RESOURCEOUT;
913
    case CVC4::Result::MEMOUT: return MEMOUT;
914
    case CVC4::Result::INTERRUPTED: return INTERRUPTED;
915
    case CVC4::Result::NO_STATUS: return NO_STATUS;
916
    case CVC4::Result::UNSUPPORTED: return UNSUPPORTED;
917
    case CVC4::Result::OTHER: return OTHER;
918
2
    default: return UNKNOWN_REASON;
919
  }
920
  return UNKNOWN_REASON;
921
}
922
923
14411
std::string Result::toString(void) const { return d_result->toString(); }
924
925
8975
std::ostream& operator<<(std::ostream& out, const Result& r)
926
{
927
8975
  out << r.toString();
928
8975
  return out;
929
}
930
931
std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e)
932
{
933
  switch (e)
934
  {
935
    case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
936
    case Result::INCOMPLETE: out << "INCOMPLETE"; break;
937
    case Result::TIMEOUT: out << "TIMEOUT"; break;
938
    case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
939
    case Result::MEMOUT: out << "MEMOUT"; break;
940
    case Result::INTERRUPTED: out << "INTERRUPTED"; break;
941
    case Result::NO_STATUS: out << "NO_STATUS"; break;
942
    case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
943
    case Result::OTHER: out << "OTHER"; break;
944
    case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
945
    default: Unhandled() << e;
946
  }
947
  return out;
948
}
949
950
/* -------------------------------------------------------------------------- */
951
/* Sort                                                                       */
952
/* -------------------------------------------------------------------------- */
953
954
5987790
Sort::Sort(const Solver* slv, const CVC4::TypeNode& t)
955
5987790
    : d_solver(slv), d_type(new CVC4::TypeNode(t))
956
{
957
5987790
}
958
959
37813904
Sort::Sort() : d_solver(nullptr), d_type(new CVC4::TypeNode()) {}
960
961
104148678
Sort::~Sort()
962
{
963
52074339
  if (d_solver != nullptr)
964
  {
965
    // Ensure that the correct node manager is in scope when the node is
966
    // destroyed.
967
15174616
    NodeManagerScope scope(d_solver->getNodeManager());
968
7587308
    d_type.reset();
969
  }
970
52074339
}
971
972
903
std::set<TypeNode> Sort::sortSetToTypeNodes(const std::set<Sort>& sorts)
973
{
974
903
  std::set<TypeNode> types;
975
2053
  for (const Sort& s : sorts)
976
  {
977
1150
    types.insert(s.getTypeNode());
978
  }
979
903
  return types;
980
}
981
982
27423
std::vector<TypeNode> Sort::sortVectorToTypeNodes(
983
    const std::vector<Sort>& sorts)
984
{
985
27423
  std::vector<TypeNode> typeNodes;
986
99795
  for (const Sort& sort : sorts)
987
  {
988
72372
    typeNodes.push_back(sort.getTypeNode());
989
  }
990
27423
  return typeNodes;
991
}
992
993
2880
std::vector<Sort> Sort::typeNodeVectorToSorts(
994
    const Solver* slv, const std::vector<TypeNode>& types)
995
{
996
2880
  std::vector<Sort> sorts;
997
9110
  for (size_t i = 0, tsize = types.size(); i < tsize; i++)
998
  {
999
6230
    sorts.push_back(Sort(slv, types[i]));
1000
  }
1001
2880
  return sorts;
1002
}
1003
1004
453198
bool Sort::operator==(const Sort& s) const
1005
{
1006
  CVC4_API_TRY_CATCH_BEGIN;
1007
  //////// all checks before this line
1008
453198
  return *d_type == *s.d_type;
1009
  ////////
1010
  CVC4_API_TRY_CATCH_END;
1011
}
1012
1013
1038
bool Sort::operator!=(const Sort& s) const
1014
{
1015
  CVC4_API_TRY_CATCH_BEGIN;
1016
  //////// all checks before this line
1017
1038
  return *d_type != *s.d_type;
1018
  ////////
1019
  CVC4_API_TRY_CATCH_END;
1020
}
1021
1022
1547
bool Sort::operator<(const Sort& s) const
1023
{
1024
  CVC4_API_TRY_CATCH_BEGIN;
1025
  //////// all checks before this line
1026
1547
  return *d_type < *s.d_type;
1027
  ////////
1028
  CVC4_API_TRY_CATCH_END;
1029
}
1030
1031
6
bool Sort::operator>(const Sort& s) const
1032
{
1033
  CVC4_API_TRY_CATCH_BEGIN;
1034
  //////// all checks before this line
1035
6
  return *d_type > *s.d_type;
1036
  ////////
1037
  CVC4_API_TRY_CATCH_END;
1038
}
1039
1040
4
bool Sort::operator<=(const Sort& s) const
1041
{
1042
  CVC4_API_TRY_CATCH_BEGIN;
1043
  //////// all checks before this line
1044
4
  return *d_type <= *s.d_type;
1045
  ////////
1046
  CVC4_API_TRY_CATCH_END;
1047
}
1048
1049
6
bool Sort::operator>=(const Sort& s) const
1050
{
1051
  CVC4_API_TRY_CATCH_BEGIN;
1052
  //////// all checks before this line
1053
6
  return *d_type >= *s.d_type;
1054
  ////////
1055
  CVC4_API_TRY_CATCH_END;
1056
}
1057
1058
3824164
bool Sort::isNull() const
1059
{
1060
  CVC4_API_TRY_CATCH_BEGIN;
1061
  //////// all checks before this line
1062
3824164
  return isNullHelper();
1063
  ////////
1064
  CVC4_API_TRY_CATCH_END;
1065
}
1066
1067
8
bool Sort::isBoolean() const
1068
{
1069
  CVC4_API_TRY_CATCH_BEGIN;
1070
  //////// all checks before this line
1071
8
  return d_type->isBoolean();
1072
  ////////
1073
  CVC4_API_TRY_CATCH_END;
1074
}
1075
1076
12
bool Sort::isInteger() const
1077
{
1078
  CVC4_API_TRY_CATCH_BEGIN;
1079
  //////// all checks before this line
1080
12
  return d_type->isInteger();
1081
  ////////
1082
  CVC4_API_TRY_CATCH_END;
1083
}
1084
1085
716
bool Sort::isReal() const
1086
{
1087
  CVC4_API_TRY_CATCH_BEGIN;
1088
  //////// all checks before this line
1089
716
  return d_type->isReal();
1090
  ////////
1091
  CVC4_API_TRY_CATCH_END;
1092
}
1093
1094
27935
bool Sort::isString() const
1095
{
1096
  CVC4_API_TRY_CATCH_BEGIN;
1097
  //////// all checks before this line
1098
27935
  return d_type->isString();
1099
  ////////
1100
  CVC4_API_TRY_CATCH_END;
1101
}
1102
1103
4
bool Sort::isRegExp() const
1104
{
1105
  CVC4_API_TRY_CATCH_BEGIN;
1106
  //////// all checks before this line
1107
4
  return d_type->isRegExp();
1108
  ////////
1109
  CVC4_API_TRY_CATCH_END;
1110
}
1111
1112
4
bool Sort::isRoundingMode() const
1113
{
1114
  CVC4_API_TRY_CATCH_BEGIN;
1115
  //////// all checks before this line
1116
4
  return d_type->isRoundingMode();
1117
  ////////
1118
  CVC4_API_TRY_CATCH_END;
1119
}
1120
1121
89
bool Sort::isBitVector() const
1122
{
1123
  CVC4_API_TRY_CATCH_BEGIN;
1124
  //////// all checks before this line
1125
89
  return d_type->isBitVector();
1126
  ////////
1127
  CVC4_API_TRY_CATCH_END;
1128
}
1129
1130
12
bool Sort::isFloatingPoint() const
1131
{
1132
  CVC4_API_TRY_CATCH_BEGIN;
1133
  //////// all checks before this line
1134
12
  return d_type->isFloatingPoint();
1135
  ////////
1136
  CVC4_API_TRY_CATCH_END;
1137
}
1138
1139
6485
bool Sort::isDatatype() const
1140
{
1141
  CVC4_API_TRY_CATCH_BEGIN;
1142
  //////// all checks before this line
1143
6485
  return d_type->isDatatype();
1144
  ////////
1145
  CVC4_API_TRY_CATCH_END;
1146
}
1147
1148
2056
bool Sort::isParametricDatatype() const
1149
{
1150
  CVC4_API_TRY_CATCH_BEGIN;
1151
  //////// all checks before this line
1152
2056
  if (!d_type->isDatatype()) return false;
1153
1620
  return d_type->isParametricDatatype();
1154
  ////////
1155
  CVC4_API_TRY_CATCH_END;
1156
}
1157
1158
3507591
bool Sort::isConstructor() const
1159
{
1160
  CVC4_API_TRY_CATCH_BEGIN;
1161
  //////// all checks before this line
1162
3507591
  return d_type->isConstructor();
1163
  ////////
1164
  CVC4_API_TRY_CATCH_END;
1165
}
1166
1167
19969
bool Sort::isSelector() const
1168
{
1169
  CVC4_API_TRY_CATCH_BEGIN;
1170
  //////// all checks before this line
1171
19969
  return d_type->isSelector();
1172
  ////////
1173
  CVC4_API_TRY_CATCH_END;
1174
}
1175
1176
10947
bool Sort::isTester() const
1177
{
1178
  CVC4_API_TRY_CATCH_BEGIN;
1179
  //////// all checks before this line
1180
10947
  return d_type->isTester();
1181
  ////////
1182
  CVC4_API_TRY_CATCH_END;
1183
}
1184
1185
1967300
bool Sort::isFunction() const
1186
{
1187
  CVC4_API_TRY_CATCH_BEGIN;
1188
  //////// all checks before this line
1189
1967300
  return d_type->isFunction();
1190
  ////////
1191
  CVC4_API_TRY_CATCH_END;
1192
}
1193
1194
4
bool Sort::isPredicate() const
1195
{
1196
  CVC4_API_TRY_CATCH_BEGIN;
1197
  //////// all checks before this line
1198
4
  return d_type->isPredicate();
1199
  ////////
1200
  CVC4_API_TRY_CATCH_END;
1201
}
1202
1203
166
bool Sort::isTuple() const
1204
{
1205
  CVC4_API_TRY_CATCH_BEGIN;
1206
  //////// all checks before this line
1207
166
  return d_type->isTuple();
1208
  ////////
1209
  CVC4_API_TRY_CATCH_END;
1210
}
1211
1212
127
bool Sort::isRecord() const
1213
{
1214
  CVC4_API_TRY_CATCH_BEGIN;
1215
  //////// all checks before this line
1216
127
  return d_type->isRecord();
1217
  ////////
1218
  CVC4_API_TRY_CATCH_END;
1219
}
1220
1221
170
bool Sort::isArray() const
1222
{
1223
  CVC4_API_TRY_CATCH_BEGIN;
1224
  //////// all checks before this line
1225
170
  return d_type->isArray();
1226
  ////////
1227
  CVC4_API_TRY_CATCH_END;
1228
}
1229
1230
29033
bool Sort::isSet() const
1231
{
1232
  CVC4_API_TRY_CATCH_BEGIN;
1233
  //////// all checks before this line
1234
29033
  return d_type->isSet();
1235
  ////////
1236
  CVC4_API_TRY_CATCH_END;
1237
}
1238
1239
32
bool Sort::isBag() const
1240
{
1241
  CVC4_API_TRY_CATCH_BEGIN;
1242
  //////// all checks before this line
1243
32
  return d_type->isBag();
1244
  ////////
1245
  CVC4_API_TRY_CATCH_END;
1246
}
1247
1248
30
bool Sort::isSequence() const
1249
{
1250
  CVC4_API_TRY_CATCH_BEGIN;
1251
  //////// all checks before this line
1252
30
  return d_type->isSequence();
1253
  ////////
1254
  CVC4_API_TRY_CATCH_END;
1255
}
1256
1257
20
bool Sort::isUninterpretedSort() const
1258
{
1259
  CVC4_API_TRY_CATCH_BEGIN;
1260
  //////// all checks before this line
1261
20
  return d_type->isSort();
1262
  ////////
1263
  CVC4_API_TRY_CATCH_END;
1264
}
1265
1266
864
bool Sort::isSortConstructor() const
1267
{
1268
  CVC4_API_TRY_CATCH_BEGIN;
1269
  //////// all checks before this line
1270
864
  return d_type->isSortConstructor();
1271
  ////////
1272
  CVC4_API_TRY_CATCH_END;
1273
}
1274
1275
88794
bool Sort::isFirstClass() const
1276
{
1277
  CVC4_API_TRY_CATCH_BEGIN;
1278
  //////// all checks before this line
1279
88794
  return d_type->isFirstClass();
1280
  ////////
1281
  CVC4_API_TRY_CATCH_END;
1282
}
1283
1284
4483
bool Sort::isFunctionLike() const
1285
{
1286
  CVC4_API_TRY_CATCH_BEGIN;
1287
  //////// all checks before this line
1288
4483
  return d_type->isFunctionLike();
1289
  ////////
1290
  CVC4_API_TRY_CATCH_END;
1291
}
1292
1293
217
bool Sort::isSubsortOf(const Sort& s) const
1294
{
1295
  CVC4_API_TRY_CATCH_BEGIN;
1296
217
  CVC4_API_ARG_CHECK_SOLVER("sort", s);
1297
  //////// all checks before this line
1298
217
  return d_type->isSubtypeOf(*s.d_type);
1299
  ////////
1300
  CVC4_API_TRY_CATCH_END;
1301
}
1302
1303
116
bool Sort::isComparableTo(const Sort& s) const
1304
{
1305
  CVC4_API_TRY_CATCH_BEGIN;
1306
116
  CVC4_API_ARG_CHECK_SOLVER("sort", s);
1307
  //////// all checks before this line
1308
116
  return d_type->isComparableTo(*s.d_type);
1309
  ////////
1310
  CVC4_API_TRY_CATCH_END;
1311
}
1312
1313
5823
Datatype Sort::getDatatype() const
1314
{
1315
11646
  NodeManagerScope scope(d_solver->getNodeManager());
1316
  CVC4_API_TRY_CATCH_BEGIN;
1317
5823
  CVC4_API_CHECK_NOT_NULL;
1318
5823
  CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
1319
  //////// all checks before this line
1320
11642
  return Datatype(d_solver, d_type->getDType());
1321
  ////////
1322
  CVC4_API_TRY_CATCH_END;
1323
}
1324
1325
626
Sort Sort::instantiate(const std::vector<Sort>& params) const
1326
{
1327
1252
  NodeManagerScope scope(d_solver->getNodeManager());
1328
  CVC4_API_TRY_CATCH_BEGIN;
1329
626
  CVC4_API_CHECK_NOT_NULL;
1330
626
  CVC4_API_CHECK_SORTS(params);
1331
628
  CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
1332
2
      << "Expected parametric datatype or sort constructor sort.";
1333
  //////// all checks before this line
1334
1248
  std::vector<CVC4::TypeNode> tparams = sortVectorToTypeNodes(params);
1335
624
  if (d_type->isDatatype())
1336
  {
1337
190
    return Sort(d_solver, d_type->instantiateParametricDatatype(tparams));
1338
  }
1339
434
  Assert(d_type->isSortConstructor());
1340
434
  return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams));
1341
  ////////
1342
  CVC4_API_TRY_CATCH_END;
1343
}
1344
1345
2
Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
1346
{
1347
4
  NodeManagerScope scope(d_solver->getNodeManager());
1348
  CVC4_API_TRY_CATCH_BEGIN;
1349
2
  CVC4_API_CHECK_NOT_NULL;
1350
2
  CVC4_API_CHECK_SORT(sort);
1351
2
  CVC4_API_CHECK_SORT(replacement);
1352
  //////// all checks before this line
1353
  return Sort(
1354
2
      d_solver,
1355
6
      d_type->substitute(sort.getTypeNode(), replacement.getTypeNode()));
1356
  ////////
1357
  CVC4_API_TRY_CATCH_END;
1358
}
1359
1360
4
Sort Sort::substitute(const std::vector<Sort>& sorts,
1361
                      const std::vector<Sort>& replacements) const
1362
{
1363
8
  NodeManagerScope scope(d_solver->getNodeManager());
1364
  CVC4_API_TRY_CATCH_BEGIN;
1365
4
  CVC4_API_CHECK_NOT_NULL;
1366
4
  CVC4_API_CHECK_SORTS(sorts);
1367
4
  CVC4_API_CHECK_SORTS(replacements);
1368
  //////// all checks before this line
1369
1370
8
  std::vector<CVC4::TypeNode> tSorts = sortVectorToTypeNodes(sorts),
1371
                              tReplacements =
1372
8
                                  sortVectorToTypeNodes(replacements);
1373
4
  return Sort(d_solver,
1374
8
              d_type->substitute(tSorts.begin(),
1375
                                 tSorts.end(),
1376
                                 tReplacements.begin(),
1377
8
                                 tReplacements.end()));
1378
  ////////
1379
  CVC4_API_TRY_CATCH_END;
1380
}
1381
1382
82
std::string Sort::toString() const
1383
{
1384
  CVC4_API_TRY_CATCH_BEGIN;
1385
  //////// all checks before this line
1386
82
  if (d_solver != nullptr)
1387
  {
1388
164
    NodeManagerScope scope(d_solver->getNodeManager());
1389
82
    return d_type->toString();
1390
  }
1391
  return d_type->toString();
1392
  ////////
1393
  CVC4_API_TRY_CATCH_END;
1394
}
1395
1396
303449
const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; }
1397
1398
/* Constructor sort ------------------------------------------------------- */
1399
1400
3540
size_t Sort::getConstructorArity() const
1401
{
1402
  CVC4_API_TRY_CATCH_BEGIN;
1403
3540
  CVC4_API_CHECK_NOT_NULL;
1404
3540
  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1405
  //////// all checks before this line
1406
3538
  return d_type->getNumChildren() - 1;
1407
  ////////
1408
  CVC4_API_TRY_CATCH_END;
1409
}
1410
1411
58
std::vector<Sort> Sort::getConstructorDomainSorts() const
1412
{
1413
  CVC4_API_TRY_CATCH_BEGIN;
1414
58
  CVC4_API_CHECK_NOT_NULL;
1415
58
  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1416
  //////// all checks before this line
1417
56
  return typeNodeVectorToSorts(d_solver, d_type->getArgTypes());
1418
  ////////
1419
  CVC4_API_TRY_CATCH_END;
1420
}
1421
1422
1484
Sort Sort::getConstructorCodomainSort() const
1423
{
1424
  CVC4_API_TRY_CATCH_BEGIN;
1425
1484
  CVC4_API_CHECK_NOT_NULL;
1426
1484
  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1427
  //////// all checks before this line
1428
1482
  return Sort(d_solver, d_type->getConstructorRangeType());
1429
  ////////
1430
  CVC4_API_TRY_CATCH_END;
1431
}
1432
1433
/* Selector sort ------------------------------------------------------- */
1434
1435
8
Sort Sort::getSelectorDomainSort() const
1436
{
1437
  CVC4_API_TRY_CATCH_BEGIN;
1438
8
  CVC4_API_CHECK_NOT_NULL;
1439
8
  CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1440
  //////// all checks before this line
1441
6
  return Sort(d_solver, d_type->getSelectorDomainType());
1442
  ////////
1443
  CVC4_API_TRY_CATCH_END;
1444
}
1445
1446
8
Sort Sort::getSelectorCodomainSort() const
1447
{
1448
  CVC4_API_TRY_CATCH_BEGIN;
1449
8
  CVC4_API_CHECK_NOT_NULL;
1450
8
  CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1451
  //////// all checks before this line
1452
6
  return Sort(d_solver, d_type->getSelectorRangeType());
1453
  ////////
1454
  CVC4_API_TRY_CATCH_END;
1455
}
1456
1457
/* Tester sort ------------------------------------------------------- */
1458
1459
16
Sort Sort::getTesterDomainSort() const
1460
{
1461
  CVC4_API_TRY_CATCH_BEGIN;
1462
16
  CVC4_API_CHECK_NOT_NULL;
1463
16
  CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1464
  //////// all checks before this line
1465
14
  return Sort(d_solver, d_type->getTesterDomainType());
1466
  ////////
1467
  CVC4_API_TRY_CATCH_END;
1468
}
1469
1470
16
Sort Sort::getTesterCodomainSort() const
1471
{
1472
  CVC4_API_TRY_CATCH_BEGIN;
1473
16
  CVC4_API_CHECK_NOT_NULL;
1474
16
  CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1475
  //////// all checks before this line
1476
14
  return d_solver->getBooleanSort();
1477
  ////////
1478
  CVC4_API_TRY_CATCH_END;
1479
}
1480
1481
/* Function sort ------------------------------------------------------- */
1482
1483
310294
size_t Sort::getFunctionArity() const
1484
{
1485
  CVC4_API_TRY_CATCH_BEGIN;
1486
310294
  CVC4_API_CHECK_NOT_NULL;
1487
310294
  CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1488
  //////// all checks before this line
1489
310292
  return d_type->getNumChildren() - 1;
1490
  ////////
1491
  CVC4_API_TRY_CATCH_END;
1492
}
1493
1494
1845
std::vector<Sort> Sort::getFunctionDomainSorts() const
1495
{
1496
  CVC4_API_TRY_CATCH_BEGIN;
1497
1845
  CVC4_API_CHECK_NOT_NULL;
1498
1845
  CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1499
  //////// all checks before this line
1500
1843
  return typeNodeVectorToSorts(d_solver, d_type->getArgTypes());
1501
  ////////
1502
  CVC4_API_TRY_CATCH_END;
1503
}
1504
1505
1733
Sort Sort::getFunctionCodomainSort() const
1506
{
1507
  CVC4_API_TRY_CATCH_BEGIN;
1508
1733
  CVC4_API_CHECK_NOT_NULL;
1509
1733
  CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1510
  //////// all checks before this line
1511
1731
  return Sort(d_solver, d_type->getRangeType());
1512
  ////////
1513
  CVC4_API_TRY_CATCH_END;
1514
}
1515
1516
/* Array sort ---------------------------------------------------------- */
1517
1518
4
Sort Sort::getArrayIndexSort() const
1519
{
1520
  CVC4_API_TRY_CATCH_BEGIN;
1521
4
  CVC4_API_CHECK_NOT_NULL;
1522
4
  CVC4_API_CHECK(isArray()) << "Not an array sort.";
1523
  //////// all checks before this line
1524
2
  return Sort(d_solver, d_type->getArrayIndexType());
1525
  ////////
1526
  CVC4_API_TRY_CATCH_END;
1527
}
1528
1529
82
Sort Sort::getArrayElementSort() const
1530
{
1531
  CVC4_API_TRY_CATCH_BEGIN;
1532
82
  CVC4_API_CHECK_NOT_NULL;
1533
82
  CVC4_API_CHECK(isArray()) << "Not an array sort.";
1534
  //////// all checks before this line
1535
80
  return Sort(d_solver, d_type->getArrayConstituentType());
1536
  ////////
1537
  CVC4_API_TRY_CATCH_END;
1538
}
1539
1540
/* Set sort ------------------------------------------------------------ */
1541
1542
6
Sort Sort::getSetElementSort() const
1543
{
1544
  CVC4_API_TRY_CATCH_BEGIN;
1545
6
  CVC4_API_CHECK_NOT_NULL;
1546
6
  CVC4_API_CHECK(isSet()) << "Not a set sort.";
1547
  //////// all checks before this line
1548
4
  return Sort(d_solver, d_type->getSetElementType());
1549
  ////////
1550
  CVC4_API_TRY_CATCH_END;
1551
}
1552
1553
/* Bag sort ------------------------------------------------------------ */
1554
1555
6
Sort Sort::getBagElementSort() const
1556
{
1557
  CVC4_API_TRY_CATCH_BEGIN;
1558
6
  CVC4_API_CHECK_NOT_NULL;
1559
6
  CVC4_API_CHECK(isBag()) << "Not a bag sort.";
1560
  //////// all checks before this line
1561
4
  return Sort(d_solver, d_type->getBagElementType());
1562
  ////////
1563
  CVC4_API_TRY_CATCH_END;
1564
}
1565
1566
/* Sequence sort ------------------------------------------------------- */
1567
1568
13
Sort Sort::getSequenceElementSort() const
1569
{
1570
  CVC4_API_TRY_CATCH_BEGIN;
1571
13
  CVC4_API_CHECK_NOT_NULL;
1572
13
  CVC4_API_CHECK(isSequence()) << "Not a sequence sort.";
1573
  //////// all checks before this line
1574
11
  return Sort(d_solver, d_type->getSequenceElementType());
1575
  ////////
1576
  CVC4_API_TRY_CATCH_END;
1577
}
1578
1579
/* Uninterpreted sort -------------------------------------------------- */
1580
1581
4
std::string Sort::getUninterpretedSortName() const
1582
{
1583
  CVC4_API_TRY_CATCH_BEGIN;
1584
4
  CVC4_API_CHECK_NOT_NULL;
1585
4
  CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1586
  //////// all checks before this line
1587
2
  return d_type->getName();
1588
  ////////
1589
  CVC4_API_TRY_CATCH_END;
1590
}
1591
1592
6
bool Sort::isUninterpretedSortParameterized() const
1593
{
1594
  CVC4_API_TRY_CATCH_BEGIN;
1595
6
  CVC4_API_CHECK_NOT_NULL;
1596
6
  CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1597
  //////// all checks before this line
1598
1599
  /* This method is not implemented in the NodeManager, since whether a
1600
   * uninterpreted sort is parameterized is irrelevant for solving. */
1601
4
  return d_type->getNumChildren() > 0;
1602
  ////////
1603
  CVC4_API_TRY_CATCH_END;
1604
}
1605
1606
6
std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
1607
{
1608
  CVC4_API_TRY_CATCH_BEGIN;
1609
6
  CVC4_API_CHECK_NOT_NULL;
1610
6
  CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1611
  //////// all checks before this line
1612
1613
  /* This method is not implemented in the NodeManager, since whether a
1614
   * uninterpreted sort is parameterized is irrelevant for solving. */
1615
8
  std::vector<TypeNode> params;
1616
8
  for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++)
1617
  {
1618
4
    params.push_back((*d_type)[i]);
1619
  }
1620
8
  return typeNodeVectorToSorts(d_solver, params);
1621
  ////////
1622
  CVC4_API_TRY_CATCH_END;
1623
}
1624
1625
/* Sort constructor sort ----------------------------------------------- */
1626
1627
4
std::string Sort::getSortConstructorName() const
1628
{
1629
  CVC4_API_TRY_CATCH_BEGIN;
1630
4
  CVC4_API_CHECK_NOT_NULL;
1631
4
  CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1632
  //////// all checks before this line
1633
2
  return d_type->getName();
1634
  ////////
1635
  CVC4_API_TRY_CATCH_END;
1636
}
1637
1638
4
size_t Sort::getSortConstructorArity() const
1639
{
1640
  CVC4_API_TRY_CATCH_BEGIN;
1641
4
  CVC4_API_CHECK_NOT_NULL;
1642
4
  CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1643
  //////// all checks before this line
1644
2
  return d_type->getSortConstructorArity();
1645
  ////////
1646
  CVC4_API_TRY_CATCH_END;
1647
}
1648
1649
/* Bit-vector sort ----------------------------------------------------- */
1650
1651
83
uint32_t Sort::getBVSize() const
1652
{
1653
  CVC4_API_TRY_CATCH_BEGIN;
1654
83
  CVC4_API_CHECK_NOT_NULL;
1655
83
  CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1656
  //////// all checks before this line
1657
81
  return d_type->getBitVectorSize();
1658
  ////////
1659
  CVC4_API_TRY_CATCH_END;
1660
}
1661
1662
/* Floating-point sort ------------------------------------------------- */
1663
1664
4
uint32_t Sort::getFPExponentSize() const
1665
{
1666
  CVC4_API_TRY_CATCH_BEGIN;
1667
4
  CVC4_API_CHECK_NOT_NULL;
1668
4
  CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1669
  //////// all checks before this line
1670
2
  return d_type->getFloatingPointExponentSize();
1671
  ////////
1672
  CVC4_API_TRY_CATCH_END;
1673
}
1674
1675
4
uint32_t Sort::getFPSignificandSize() const
1676
{
1677
  CVC4_API_TRY_CATCH_BEGIN;
1678
4
  CVC4_API_CHECK_NOT_NULL;
1679
4
  CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1680
  //////// all checks before this line
1681
2
  return d_type->getFloatingPointSignificandSize();
1682
  ////////
1683
  CVC4_API_TRY_CATCH_END;
1684
}
1685
1686
/* Datatype sort ------------------------------------------------------- */
1687
1688
55
std::vector<Sort> Sort::getDatatypeParamSorts() const
1689
{
1690
  CVC4_API_TRY_CATCH_BEGIN;
1691
55
  CVC4_API_CHECK_NOT_NULL;
1692
55
  CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1693
  //////// all checks before this line
1694
53
  return typeNodeVectorToSorts(d_solver, d_type->getParamTypes());
1695
  ////////
1696
  CVC4_API_TRY_CATCH_END;
1697
}
1698
1699
4
size_t Sort::getDatatypeArity() const
1700
{
1701
  CVC4_API_TRY_CATCH_BEGIN;
1702
4
  CVC4_API_CHECK_NOT_NULL;
1703
4
  CVC4_API_CHECK(isDatatype()) << "Not a datatype sort.";
1704
  //////// all checks before this line
1705
2
  return d_type->getNumChildren() - 1;
1706
  ////////
1707
  CVC4_API_TRY_CATCH_END;
1708
}
1709
1710
/* Tuple sort ---------------------------------------------------------- */
1711
1712
62
size_t Sort::getTupleLength() const
1713
{
1714
  CVC4_API_TRY_CATCH_BEGIN;
1715
62
  CVC4_API_CHECK_NOT_NULL;
1716
62
  CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
1717
  //////// all checks before this line
1718
60
  return d_type->getTupleLength();
1719
  ////////
1720
  CVC4_API_TRY_CATCH_END;
1721
}
1722
1723
23
std::vector<Sort> Sort::getTupleSorts() const
1724
{
1725
  CVC4_API_TRY_CATCH_BEGIN;
1726
23
  CVC4_API_CHECK_NOT_NULL;
1727
23
  CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
1728
  //////// all checks before this line
1729
21
  return typeNodeVectorToSorts(d_solver, d_type->getTupleTypes());
1730
  ////////
1731
  CVC4_API_TRY_CATCH_END;
1732
}
1733
1734
/* --------------------------------------------------------------------- */
1735
1736
74
std::ostream& operator<<(std::ostream& out, const Sort& s)
1737
{
1738
74
  out << s.toString();
1739
74
  return out;
1740
}
1741
1742
size_t SortHashFunction::operator()(const Sort& s) const
1743
{
1744
  return TypeNodeHashFunction()(*s.d_type);
1745
}
1746
1747
/* Helpers                                                                    */
1748
/* -------------------------------------------------------------------------- */
1749
1750
/* Split out to avoid nested API calls (problematic with API tracing).        */
1751
/* .......................................................................... */
1752
1753
4149991
bool Sort::isNullHelper() const { return d_type->isNull(); }
1754
1755
/* -------------------------------------------------------------------------- */
1756
/* Op                                                                     */
1757
/* -------------------------------------------------------------------------- */
1758
1759
14418423
Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {}
1760
1761
52
Op::Op(const Solver* slv, const Kind k)
1762
52
    : d_solver(slv), d_kind(k), d_node(new CVC4::Node())
1763
{
1764
52
}
1765
1766
82447
Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n)
1767
82447
    : d_solver(slv), d_kind(k), d_node(new CVC4::Node(n))
1768
{
1769
82447
}
1770
1771
29205942
Op::~Op()
1772
{
1773
14602971
  if (d_solver != nullptr)
1774
  {
1775
    // Ensure that the correct node manager is in scope when the type node is
1776
    // destroyed.
1777
823894
    NodeManagerScope scope(d_solver->getNodeManager());
1778
411947
    d_node.reset();
1779
  }
1780
14602971
}
1781
1782
/* Public methods                                                             */
1783
26
bool Op::operator==(const Op& t) const
1784
{
1785
  CVC4_API_TRY_CATCH_BEGIN;
1786
  //////// all checks before this line
1787
26
  if (d_node->isNull() && t.d_node->isNull())
1788
  {
1789
22
    return (d_kind == t.d_kind);
1790
  }
1791
4
  else if (d_node->isNull() || t.d_node->isNull())
1792
  {
1793
    return false;
1794
  }
1795
4
  return (d_kind == t.d_kind) && (*d_node == *t.d_node);
1796
  ////////
1797
  CVC4_API_TRY_CATCH_END;
1798
}
1799
1800
bool Op::operator!=(const Op& t) const
1801
{
1802
  CVC4_API_TRY_CATCH_BEGIN;
1803
  //////// all checks before this line
1804
  return !(*this == t);
1805
  ////////
1806
  CVC4_API_TRY_CATCH_END;
1807
}
1808
1809
2
Kind Op::getKind() const
1810
{
1811
2
  CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind";
1812
  //////// all checks before this line
1813
2
  return d_kind;
1814
}
1815
1816
3800301
bool Op::isNull() const
1817
{
1818
  CVC4_API_TRY_CATCH_BEGIN;
1819
  //////// all checks before this line
1820
3800301
  return isNullHelper();
1821
  ////////
1822
  CVC4_API_TRY_CATCH_END;
1823
}
1824
1825
12
bool Op::isIndexed() const
1826
{
1827
  CVC4_API_TRY_CATCH_BEGIN;
1828
  //////// all checks before this line
1829
12
  return isIndexedHelper();
1830
  ////////
1831
  CVC4_API_TRY_CATCH_END;
1832
}
1833
1834
template <>
1835
10
std::string Op::getIndices() const
1836
{
1837
  CVC4_API_TRY_CATCH_BEGIN;
1838
10
  CVC4_API_CHECK_NOT_NULL;
1839
8
  CVC4_API_CHECK(!d_node->isNull())
1840
      << "Expecting a non-null internal expression. This Op is not indexed.";
1841
8
  Kind k = intToExtKind(d_node->getKind());
1842
24
  CVC4_API_CHECK(k == DIVISIBLE || k == RECORD_UPDATE)
1843
      << "Can't get string index from"
1844
16
      << " kind " << kindToString(k);
1845
  //////// all checks before this line
1846
2
  return k == DIVISIBLE ? d_node->getConst<Divisible>().k.toString()
1847
6
                        : d_node->getConst<RecordUpdate>().getField();
1848
  ////////
1849
  CVC4_API_TRY_CATCH_END;
1850
}
1851
1852
template <>
1853
22
uint32_t Op::getIndices() const
1854
{
1855
  CVC4_API_TRY_CATCH_BEGIN;
1856
22
  CVC4_API_CHECK_NOT_NULL;
1857
24
  CVC4_API_CHECK(!d_node->isNull())
1858
2
      << "Expecting a non-null internal expression. This Op is not indexed.";
1859
  //////// all checks before this line
1860
1861
20
  uint32_t i = 0;
1862
20
  Kind k = intToExtKind(d_node->getKind());
1863
20
  switch (k)
1864
  {
1865
2
    case BITVECTOR_REPEAT:
1866
2
      i = d_node->getConst<BitVectorRepeat>().d_repeatAmount;
1867
2
      break;
1868
2
    case BITVECTOR_ZERO_EXTEND:
1869
2
      i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
1870
2
      break;
1871
2
    case BITVECTOR_SIGN_EXTEND:
1872
2
      i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount;
1873
2
      break;
1874
2
    case BITVECTOR_ROTATE_LEFT:
1875
2
      i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
1876
2
      break;
1877
2
    case BITVECTOR_ROTATE_RIGHT:
1878
2
      i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount;
1879
2
      break;
1880
2
    case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
1881
    case IAND: i = d_node->getConst<IntAnd>().d_size; break;
1882
2
    case FLOATINGPOINT_TO_UBV:
1883
2
      i = d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size;
1884
2
      break;
1885
2
    case FLOATINGPOINT_TO_SBV:
1886
2
      i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size;
1887
2
      break;
1888
2
    case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
1889
    case REGEXP_REPEAT:
1890
      i = d_node->getConst<RegExpRepeat>().d_repeatAmount;
1891
      break;
1892
2
    default:
1893
8
      CVC4_API_CHECK(false) << "Can't get uint32_t index from"
1894
6
                            << " kind " << kindToString(k);
1895
  }
1896
18
  return i;
1897
  ////////
1898
  CVC4_API_TRY_CATCH_END;
1899
}
1900
1901
template <>
1902
16
std::pair<uint32_t, uint32_t> Op::getIndices() const
1903
{
1904
  CVC4_API_TRY_CATCH_BEGIN;
1905
16
  CVC4_API_CHECK_NOT_NULL;
1906
16
  CVC4_API_CHECK(!d_node->isNull())
1907
      << "Expecting a non-null internal expression. This Op is not indexed.";
1908
  //////// all checks before this line
1909
1910
16
  std::pair<uint32_t, uint32_t> indices;
1911
16
  Kind k = intToExtKind(d_node->getKind());
1912
1913
  // using if/else instead of case statement because want local variables
1914
16
  if (k == BITVECTOR_EXTRACT)
1915
  {
1916
2
    CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
1917
966054
    indices = std::make_pair(ext.d_high, ext.d_low);
1918
  }
1919
14
  else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
1920
  {
1921
    CVC4::FloatingPointToFPIEEEBitVector ext =
1922
2
        d_node->getConst<FloatingPointToFPIEEEBitVector>();
1923
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1924
4
                             ext.d_fp_size.significandWidth());
1925
  }
1926
12
  else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
1927
  {
1928
    CVC4::FloatingPointToFPFloatingPoint ext =
1929
2
        d_node->getConst<FloatingPointToFPFloatingPoint>();
1930
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1931
4
                             ext.d_fp_size.significandWidth());
1932
  }
1933
10
  else if (k == FLOATINGPOINT_TO_FP_REAL)
1934
  {
1935
2
    CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
1936
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1937
4
                             ext.d_fp_size.significandWidth());
1938
  }
1939
8
  else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
1940
  {
1941
    CVC4::FloatingPointToFPSignedBitVector ext =
1942
2
        d_node->getConst<FloatingPointToFPSignedBitVector>();
1943
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1944
4
                             ext.d_fp_size.significandWidth());
1945
  }
1946
6
  else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
1947
  {
1948
    CVC4::FloatingPointToFPUnsignedBitVector ext =
1949
2
        d_node->getConst<FloatingPointToFPUnsignedBitVector>();
1950
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1951
4
                             ext.d_fp_size.significandWidth());
1952
  }
1953
4
  else if (k == FLOATINGPOINT_TO_FP_GENERIC)
1954
  {
1955
    CVC4::FloatingPointToFPGeneric ext =
1956
2
        d_node->getConst<FloatingPointToFPGeneric>();
1957
2
    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
1958
4
                             ext.d_fp_size.significandWidth());
1959
  }
1960
2
  else if (k == REGEXP_LOOP)
1961
  {
1962
    CVC4::RegExpLoop ext = d_node->getConst<RegExpLoop>();
1963
    indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc);
1964
  }
1965
  else
1966
  {
1967
8
    CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
1968
6
                          << " kind " << kindToString(k);
1969
  }
1970
14
  return indices;
1971
  ////////
1972
  CVC4_API_TRY_CATCH_END;
1973
}
1974
1975
4
std::string Op::toString() const
1976
{
1977
  CVC4_API_TRY_CATCH_BEGIN;
1978
  //////// all checks before this line
1979
4
  if (d_node->isNull())
1980
  {
1981
    return kindToString(d_kind);
1982
  }
1983
  else
1984
  {
1985
4
    CVC4_API_CHECK(!d_node->isNull())
1986
        << "Expecting a non-null internal expression";
1987
4
    if (d_solver != nullptr)
1988
    {
1989
8
      NodeManagerScope scope(d_solver->getNodeManager());
1990
4
      return d_node->toString();
1991
    }
1992
    return d_node->toString();
1993
  }
1994
  ////////
1995
  CVC4_API_TRY_CATCH_END;
1996
}
1997
1998
std::ostream& operator<<(std::ostream& out, const Op& t)
1999
{
2000
  out << t.toString();
2001
  return out;
2002
}
2003
2004
size_t OpHashFunction::operator()(const Op& t) const
2005
{
2006
  if (t.isIndexedHelper())
2007
  {
2008
    return NodeHashFunction()(*t.d_node);
2009
  }
2010
  else
2011
  {
2012
    return KindHashFunction()(t.d_kind);
2013
  }
2014
}
2015
2016
/* Helpers                                                                    */
2017
/* -------------------------------------------------------------------------- */
2018
2019
/* Split out to avoid nested API calls (problematic with API tracing).        */
2020
/* .......................................................................... */
2021
2022
3800349
bool Op::isNullHelper() const
2023
{
2024
3800349
  return (d_node->isNull() && (d_kind == NULL_EXPR));
2025
}
2026
2027
82405
bool Op::isIndexedHelper() const { return !d_node->isNull(); }
2028
2029
/* -------------------------------------------------------------------------- */
2030
/* Term                                                                       */
2031
/* -------------------------------------------------------------------------- */
2032
2033
69071086
Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
2034
2035
4254347
Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
2036
{
2037
  // Ensure that we create the node in the correct node manager.
2038
8508694
  NodeManagerScope scope(d_solver->getNodeManager());
2039
4254347
  d_node.reset(new CVC4::Node(n));
2040
4254347
}
2041
2042
220296998
Term::~Term()
2043
{
2044
110148499
  if (d_solver != nullptr)
2045
  {
2046
    // Ensure that the correct node manager is in scope when the node is
2047
    // destroyed.
2048
90101776
    NodeManagerScope scope(d_solver->getNodeManager());
2049
45050888
    d_node.reset();
2050
  }
2051
110148499
}
2052
2053
105542
bool Term::operator==(const Term& t) const
2054
{
2055
  CVC4_API_TRY_CATCH_BEGIN;
2056
  //////// all checks before this line
2057
105542
  return *d_node == *t.d_node;
2058
  ////////
2059
  CVC4_API_TRY_CATCH_END;
2060
}
2061
2062
42
bool Term::operator!=(const Term& t) const
2063
{
2064
  CVC4_API_TRY_CATCH_BEGIN;
2065
  //////// all checks before this line
2066
42
  return *d_node != *t.d_node;
2067
  ////////
2068
  CVC4_API_TRY_CATCH_END;
2069
}
2070
2071
43
bool Term::operator<(const Term& t) const
2072
{
2073
  CVC4_API_TRY_CATCH_BEGIN;
2074
  //////// all checks before this line
2075
43
  return *d_node < *t.d_node;
2076
  ////////
2077
  CVC4_API_TRY_CATCH_END;
2078
}
2079
2080
4
bool Term::operator>(const Term& t) const
2081
{
2082
  CVC4_API_TRY_CATCH_BEGIN;
2083
  //////// all checks before this line
2084
4
  return *d_node > *t.d_node;
2085
  ////////
2086
  CVC4_API_TRY_CATCH_END;
2087
}
2088
2089
2
bool Term::operator<=(const Term& t) const
2090
{
2091
  CVC4_API_TRY_CATCH_BEGIN;
2092
  //////// all checks before this line
2093
2
  return *d_node <= *t.d_node;
2094
  ////////
2095
  CVC4_API_TRY_CATCH_END;
2096
}
2097
2098
4
bool Term::operator>=(const Term& t) const
2099
{
2100
  CVC4_API_TRY_CATCH_BEGIN;
2101
  //////// all checks before this line
2102
4
  return *d_node >= *t.d_node;
2103
  ////////
2104
  CVC4_API_TRY_CATCH_END;
2105
}
2106
2107
835
size_t Term::getNumChildren() const
2108
{
2109
  CVC4_API_TRY_CATCH_BEGIN;
2110
835
  CVC4_API_CHECK_NOT_NULL;
2111
  //////// all checks before this line
2112
2113
  // special case for apply kinds
2114
833
  if (isApplyKind(d_node->getKind()))
2115
  {
2116
745
    return d_node->getNumChildren() + 1;
2117
  }
2118
88
  if(isCastedReal())
2119
  {
2120
    return 0;
2121
  }
2122
88
  return d_node->getNumChildren();
2123
  ////////
2124
  CVC4_API_TRY_CATCH_END;
2125
}
2126
2127
457
Term Term::operator[](size_t index) const
2128
{
2129
  CVC4_API_TRY_CATCH_BEGIN;
2130
457
  CVC4_API_CHECK_NOT_NULL;
2131
455
  CVC4_API_CHECK(index < getNumChildren()) << "index out of bound";
2132
455
  CVC4_API_CHECK(!isApplyKind(d_node->getKind()) || d_node->hasOperator())
2133
      << "Expected apply kind to have operator when accessing child of Term";
2134
  //////// all checks before this line
2135
2136
  // special cases for apply kinds
2137
455
  if (isApplyKind(d_node->getKind()))
2138
  {
2139
375
    if (index == 0)
2140
    {
2141
      // return the operator
2142
373
      return Term(d_solver, d_node->getOperator());
2143
    }
2144
    else
2145
    {
2146
2
      index -= 1;
2147
    }
2148
  }
2149
  // otherwise we are looking up child at (index-1)
2150
82
  return Term(d_solver, (*d_node)[index]);
2151
  ////////
2152
  CVC4_API_TRY_CATCH_END;
2153
}
2154
2155
12
uint64_t Term::getId() const
2156
{
2157
  CVC4_API_TRY_CATCH_BEGIN;
2158
12
  CVC4_API_CHECK_NOT_NULL;
2159
  //////// all checks before this line
2160
10
  return d_node->getId();
2161
  ////////
2162
  CVC4_API_TRY_CATCH_END;
2163
}
2164
2165
4930
Kind Term::getKind() const
2166
{
2167
  CVC4_API_TRY_CATCH_BEGIN;
2168
4930
  CVC4_API_CHECK_NOT_NULL;
2169
  //////// all checks before this line
2170
4928
  return getKindHelper();
2171
  ////////
2172
  CVC4_API_TRY_CATCH_END;
2173
}
2174
2175
5469343
Sort Term::getSort() const
2176
{
2177
  CVC4_API_TRY_CATCH_BEGIN;
2178
5469343
  CVC4_API_CHECK_NOT_NULL;
2179
10938682
  NodeManagerScope scope(d_solver->getNodeManager());
2180
  //////// all checks before this line
2181
10938682
  return Sort(d_solver, d_node->getType());
2182
  ////////
2183
  CVC4_API_TRY_CATCH_END;
2184
}
2185
2186
15
Term Term::substitute(const Term& term, const Term& replacement) const
2187
{
2188
  CVC4_API_TRY_CATCH_BEGIN;
2189
15
  CVC4_API_CHECK_NOT_NULL;
2190
13
  CVC4_API_CHECK_TERM(term);
2191
11
  CVC4_API_CHECK_TERM(replacement);
2192
11
  CVC4_API_CHECK(term.getSort().isComparableTo(replacement.getSort()))
2193
2
      << "Expecting terms of comparable sort in substitute";
2194
  //////// all checks before this line
2195
  return Term(
2196
7
      d_solver,
2197
14
      d_node->substitute(TNode(*term.d_node), TNode(*replacement.d_node)));
2198
  ////////
2199
  CVC4_API_TRY_CATCH_END;
2200
}
2201
2202
12
Term Term::substitute(const std::vector<Term>& terms,
2203
                      const std::vector<Term>& replacements) const
2204
{
2205
  CVC4_API_TRY_CATCH_BEGIN;
2206
12
  CVC4_API_CHECK_NOT_NULL;
2207
12
  CVC4_API_CHECK(terms.size() == replacements.size())
2208
2
      << "Expecting vectors of the same arity in substitute";
2209
8
  CVC4_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms, replacements);
2210
  //////// all checks before this line
2211
4
  std::vector<Node> nodes = Term::termVectorToNodes(terms);
2212
4
  std::vector<Node> nodeReplacements = Term::termVectorToNodes(replacements);
2213
2
  return Term(d_solver,
2214
4
              d_node->substitute(nodes.begin(),
2215
                                 nodes.end(),
2216
                                 nodeReplacements.begin(),
2217
4
                                 nodeReplacements.end()));
2218
  ////////
2219
  CVC4_API_TRY_CATCH_END;
2220
}
2221
2222
36
bool Term::hasOp() const
2223
{
2224
  CVC4_API_TRY_CATCH_BEGIN;
2225
36
  CVC4_API_CHECK_NOT_NULL;
2226
  //////// all checks before this line
2227
36
  return d_node->hasOperator();
2228
  ////////
2229
  CVC4_API_TRY_CATCH_END;
2230
}
2231
2232
38
Op Term::getOp() const
2233
{
2234
  CVC4_API_TRY_CATCH_BEGIN;
2235
38
  CVC4_API_CHECK_NOT_NULL;
2236
44
  CVC4_API_CHECK(d_node->hasOperator())
2237
6
      << "Expecting Term to have an Op when calling getOp()";
2238
  //////// all checks before this line
2239
2240
  // special cases for parameterized operators that are not indexed operators
2241
  // the API level differs from the internal structure
2242
  // indexed operators are stored in Ops
2243
  // whereas functions and datatype operators are terms, and the Op
2244
  // is one of the APPLY_* kinds
2245
32
  if (isApplyKind(d_node->getKind()))
2246
  {
2247
20
    return Op(d_solver, intToExtKind(d_node->getKind()));
2248
  }
2249
12
  else if (d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
2250
  {
2251
    // it's an indexed operator
2252
    // so we should return the indexed op
2253
12
    CVC4::Node op = d_node->getOperator();
2254
6
    return Op(d_solver, intToExtKind(d_node->getKind()), op);
2255
  }
2256
  // Notice this is the only case where getKindHelper is used, since the
2257
  // cases above do not have special cases for intToExtKind.
2258
6
  return Op(d_solver, getKindHelper());
2259
  ////////
2260
  CVC4_API_TRY_CATCH_END;
2261
}
2262
2263
25669099
bool Term::isNull() const
2264
{
2265
  CVC4_API_TRY_CATCH_BEGIN;
2266
  //////// all checks before this line
2267
25669099
  return isNullHelper();
2268
  ////////
2269
  CVC4_API_TRY_CATCH_END;
2270
}
2271
2272
4
Term Term::getConstArrayBase() const
2273
{
2274
8
  NodeManagerScope scope(d_solver->getNodeManager());
2275
  CVC4_API_TRY_CATCH_BEGIN;
2276
4
  CVC4_API_CHECK_NOT_NULL;
2277
  // CONST_ARRAY kind maps to STORE_ALL internal kind
2278
6
  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL)
2279
2
      << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
2280
  //////// all checks before this line
2281
4
  return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
2282
  ////////
2283
  CVC4_API_TRY_CATCH_END;
2284
}
2285
2286
13
std::vector<Term> Term::getConstSequenceElements() const
2287
{
2288
  CVC4_API_TRY_CATCH_BEGIN;
2289
13
  CVC4_API_CHECK_NOT_NULL;
2290
15
  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE)
2291
      << "Expecting a CONST_SEQUENCE Term when calling "
2292
2
         "getConstSequenceElements()";
2293
  //////// all checks before this line
2294
11
  const std::vector<Node>& elems = d_node->getConst<Sequence>().getVec();
2295
22
  std::vector<Term> terms;
2296
11
  for (const Node& t : elems)
2297
  {
2298
    terms.push_back(Term(d_solver, t));
2299
  }
2300
22
  return terms;
2301
  ////////
2302
  CVC4_API_TRY_CATCH_END;
2303
}
2304
2305
17765
Term Term::notTerm() const
2306
{
2307
  CVC4_API_TRY_CATCH_BEGIN;
2308
17765
  CVC4_API_CHECK_NOT_NULL;
2309
  //////// all checks before this line
2310
35514
  Node res = d_node->notNode();
2311
17751
  (void)res.getType(true); /* kick off type checking */
2312
35502
  return Term(d_solver, res);
2313
  ////////
2314
  CVC4_API_TRY_CATCH_END;
2315
}
2316
2317
94
Term Term::andTerm(const Term& t) const
2318
{
2319
  CVC4_API_TRY_CATCH_BEGIN;
2320
94
  CVC4_API_CHECK_NOT_NULL;
2321
92
  CVC4_API_CHECK_TERM(t);
2322
  //////// all checks before this line
2323
102
  Node res = d_node->andNode(*t.d_node);
2324
12
  (void)res.getType(true); /* kick off type checking */
2325
24
  return Term(d_solver, res);
2326
  ////////
2327
  CVC4_API_TRY_CATCH_END;
2328
}
2329
2330
94
Term Term::orTerm(const Term& t) const
2331
{
2332
  CVC4_API_TRY_CATCH_BEGIN;
2333
94
  CVC4_API_CHECK_NOT_NULL;
2334
92
  CVC4_API_CHECK_TERM(t);
2335
  //////// all checks before this line
2336
102
  Node res = d_node->orNode(*t.d_node);
2337
12
  (void)res.getType(true); /* kick off type checking */
2338
24
  return Term(d_solver, res);
2339
  ////////
2340
  CVC4_API_TRY_CATCH_END;
2341
}
2342
2343
94
Term Term::xorTerm(const Term& t) const
2344
{
2345
  CVC4_API_TRY_CATCH_BEGIN;
2346
94
  CVC4_API_CHECK_NOT_NULL;
2347
92
  CVC4_API_CHECK_TERM(t);
2348
  //////// all checks before this line
2349
102
  Node res = d_node->xorNode(*t.d_node);
2350
12
  (void)res.getType(true); /* kick off type checking */
2351
24
  return Term(d_solver, res);
2352
  ////////
2353
  CVC4_API_TRY_CATCH_END;
2354
}
2355
2356
140
Term Term::eqTerm(const Term& t) const
2357
{
2358
  CVC4_API_TRY_CATCH_BEGIN;
2359
140
  CVC4_API_CHECK_NOT_NULL;
2360
138
  CVC4_API_CHECK_TERM(t);
2361
  //////// all checks before this line
2362
212
  Node res = d_node->eqNode(*t.d_node);
2363
76
  (void)res.getType(true); /* kick off type checking */
2364
152
  return Term(d_solver, res);
2365
  ////////
2366
  CVC4_API_TRY_CATCH_END;
2367
}
2368
2369
94
Term Term::impTerm(const Term& t) const
2370
{
2371
  CVC4_API_TRY_CATCH_BEGIN;
2372
94
  CVC4_API_CHECK_NOT_NULL;
2373
92
  CVC4_API_CHECK_TERM(t);
2374
  //////// all checks before this line
2375
102
  Node res = d_node->impNode(*t.d_node);
2376
12
  (void)res.getType(true); /* kick off type checking */
2377
24
  return Term(d_solver, res);
2378
  ////////
2379
  CVC4_API_TRY_CATCH_END;
2380
}
2381
2382
50
Term Term::iteTerm(const Term& then_t, const Term& else_t) const
2383
{
2384
  CVC4_API_TRY_CATCH_BEGIN;
2385
50
  CVC4_API_CHECK_NOT_NULL;
2386
48
  CVC4_API_CHECK_TERM(then_t);
2387
46
  CVC4_API_CHECK_TERM(else_t);
2388
  //////// all checks before this line
2389
58
  Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node);
2390
14
  (void)res.getType(true); /* kick off type checking */
2391
28
  return Term(d_solver, res);
2392
  ////////
2393
  CVC4_API_TRY_CATCH_END;
2394
}
2395
2396
5193
std::string Term::toString() const
2397
{
2398
  CVC4_API_TRY_CATCH_BEGIN;
2399
  //////// all checks before this line
2400
5193
  if (d_solver != nullptr)
2401
  {
2402
10386
    NodeManagerScope scope(d_solver->getNodeManager());
2403
5193
    return d_node->toString();
2404
  }
2405
  return d_node->toString();
2406
  ////////
2407
  CVC4_API_TRY_CATCH_END;
2408
}
2409
2410
Term::const_iterator::const_iterator()
2411
    : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2412
{
2413
}
2414
2415
187
Term::const_iterator::const_iterator(const Solver* slv,
2416
                                     const std::shared_ptr<CVC4::Node>& n,
2417
187
                                     uint32_t p)
2418
187
    : d_solver(slv), d_origNode(n), d_pos(p)
2419
{
2420
187
}
2421
2422
281
Term::const_iterator::const_iterator(const const_iterator& it)
2423
281
    : d_solver(nullptr), d_origNode(nullptr)
2424
{
2425
281
  if (it.d_origNode != nullptr)
2426
  {
2427
281
    d_solver = it.d_solver;
2428
281
    d_origNode = it.d_origNode;
2429
281
    d_pos = it.d_pos;
2430
  }
2431
281
}
2432
2433
Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
2434
{
2435
  d_solver = it.d_solver;
2436
  d_origNode = it.d_origNode;
2437
  d_pos = it.d_pos;
2438
  return *this;
2439
}
2440
2441
210
bool Term::const_iterator::operator==(const const_iterator& it) const
2442
{
2443
210
  if (d_origNode == nullptr || it.d_origNode == nullptr)
2444
  {
2445
    return false;
2446
  }
2447
420
  return (d_solver == it.d_solver && *d_origNode == *it.d_origNode)
2448
420
         && (d_pos == it.d_pos);
2449
}
2450
2451
210
bool Term::const_iterator::operator!=(const const_iterator& it) const
2452
{
2453
210
  return !(*this == it);
2454
}
2455
2456
139
Term::const_iterator& Term::const_iterator::operator++()
2457
{
2458
139
  Assert(d_origNode != nullptr);
2459
139
  ++d_pos;
2460
139
  return *this;
2461
}
2462
2463
Term::const_iterator Term::const_iterator::operator++(int)
2464
{
2465
  Assert(d_origNode != nullptr);
2466
  const_iterator it = *this;
2467
  ++d_pos;
2468
  return it;
2469
}
2470
2471
136
Term Term::const_iterator::operator*() const
2472
{
2473
136
  Assert(d_origNode != nullptr);
2474
  // this term has an extra child (mismatch between API and internal structure)
2475
  // the extra child will be the first child
2476
136
  bool extra_child = isApplyKind(d_origNode->getKind());
2477
2478
136
  if (!d_pos && extra_child)
2479
  {
2480
49
    return Term(d_solver, d_origNode->getOperator());
2481
  }
2482
  else
2483
  {
2484
87
    uint32_t idx = d_pos;
2485
87
    if (extra_child)
2486
    {
2487
32
      Assert(idx > 0);
2488
32
      --idx;
2489
    }
2490
87
    Assert(idx >= 0);
2491
87
    return Term(d_solver, (*d_origNode)[idx]);
2492
  }
2493
}
2494
2495
87
Term::const_iterator Term::begin() const
2496
{
2497
87
  return Term::const_iterator(d_solver, d_node, 0);
2498
}
2499
2500
100
Term::const_iterator Term::end() const
2501
{
2502
100
  int endpos = d_node->getNumChildren();
2503
  // special cases for APPLY_*
2504
  // the API differs from the internal structure
2505
  // the API takes a "higher-order" perspective and the applied
2506
  //   function or datatype constructor/selector/tester is a Term
2507
  // which means it needs to be one of the children, even though
2508
  //   internally it is not
2509
100
  if (isApplyKind(d_node->getKind()))
2510
  {
2511
    // one more child if this is a UF application (count the UF as a child)
2512
52
    ++endpos;
2513
  }
2514
100
  return Term::const_iterator(d_solver, d_node, endpos);
2515
}
2516
2517
7613513
const CVC4::Node& Term::getNode(void) const { return *d_node; }
2518
2519
namespace detail {
2520
const Rational& getRational(const CVC4::Node& node)
2521
{
2522
  return node.getConst<Rational>();
2523
}
2524
194
Integer getInteger(const CVC4::Node& node)
2525
{
2526
194
  return node.getConst<Rational>().getNumerator();
2527
}
2528
template <typename T>
2529
132
bool checkIntegerBounds(const Integer& i)
2530
{
2531
396
  return i >= std::numeric_limits<T>::min()
2532
528
         && i <= std::numeric_limits<T>::max();
2533
}
2534
bool checkReal32Bounds(const Rational& r)
2535
{
2536
  return checkIntegerBounds<std::int32_t>(r.getNumerator())
2537
         && checkIntegerBounds<std::uint32_t>(r.getDenominator());
2538
}
2539
bool checkReal64Bounds(const Rational& r)
2540
{
2541
  return checkIntegerBounds<std::int64_t>(r.getNumerator())
2542
         && checkIntegerBounds<std::uint64_t>(r.getDenominator());
2543
}
2544
2545
176
bool isInteger(const Node& node)
2546
{
2547
176
  return node.getKind() == CVC4::Kind::CONST_RATIONAL
2548
176
         && node.getConst<Rational>().isIntegral();
2549
}
2550
28
bool isInt32(const Node& node)
2551
{
2552
28
  return isInteger(node)
2553
56
         && checkIntegerBounds<std::int32_t>(getInteger(node));
2554
}
2555
28
bool isUInt32(const Node& node)
2556
{
2557
28
  return isInteger(node)
2558
56
         && checkIntegerBounds<std::uint32_t>(getInteger(node));
2559
}
2560
36
bool isInt64(const Node& node)
2561
{
2562
36
  return isInteger(node)
2563
72
         && checkIntegerBounds<std::int64_t>(getInteger(node));
2564
}
2565
40
bool isUInt64(const Node& node)
2566
{
2567
40
  return isInteger(node)
2568
80
         && checkIntegerBounds<std::uint64_t>(getInteger(node));
2569
}
2570
}  // namespace detail
2571
2572
22
bool Term::isInt32() const
2573
{
2574
  CVC4_API_TRY_CATCH_BEGIN;
2575
22
  CVC4_API_CHECK_NOT_NULL;
2576
  //////// all checks before this line
2577
22
  return detail::isInt32(*d_node);
2578
  ////////
2579
  CVC4_API_TRY_CATCH_END;
2580
}
2581
2582
6
std::int32_t Term::getInt32() const
2583
{
2584
  CVC4_API_TRY_CATCH_BEGIN;
2585
6
  CVC4_API_CHECK_NOT_NULL;
2586
6
  CVC4_API_CHECK(detail::isInt32(*d_node))
2587
      << "Term should be a Int32 when calling getInt32()";
2588
  //////// all checks before this line
2589
6
  return detail::getInteger(*d_node).getSignedInt();
2590
  ////////
2591
  CVC4_API_TRY_CATCH_END;
2592
}
2593
2594
22
bool Term::isUInt32() const { return detail::isUInt32(*d_node); }
2595
6
std::uint32_t Term::getUInt32() const
2596
{
2597
  CVC4_API_TRY_CATCH_BEGIN;
2598
6
  CVC4_API_CHECK_NOT_NULL;
2599
6
  CVC4_API_CHECK(detail::isUInt32(*d_node))
2600
      << "Term should be a UInt32 when calling getUInt32()";
2601
  //////// all checks before this line
2602
6
  return detail::getInteger(*d_node).getUnsignedInt();
2603
  ////////
2604
  CVC4_API_TRY_CATCH_END;
2605
}
2606
2607
22
bool Term::isInt64() const { return detail::isInt64(*d_node); }
2608
14
std::int64_t Term::getInt64() const
2609
{
2610
  CVC4_API_TRY_CATCH_BEGIN;
2611
14
  CVC4_API_CHECK_NOT_NULL;
2612
14
  CVC4_API_CHECK(detail::isInt64(*d_node))
2613
      << "Term should be a Int64 when calling getInt64()";
2614
  //////// all checks before this line
2615
14
  return detail::getInteger(*d_node).getLong();
2616
  ////////
2617
  CVC4_API_TRY_CATCH_END;
2618
}
2619
2620
26
bool Term::isUInt64() const
2621
{
2622
  CVC4_API_TRY_CATCH_BEGIN;
2623
26
  CVC4_API_CHECK_NOT_NULL;
2624
  //////// all checks before this line
2625
26
  return detail::isUInt64(*d_node);
2626
  ////////
2627
  CVC4_API_TRY_CATCH_END;
2628
}
2629
2630
14
std::uint64_t Term::getUInt64() const
2631
{
2632
  CVC4_API_TRY_CATCH_BEGIN;
2633
14
  CVC4_API_CHECK_NOT_NULL;
2634
14
  CVC4_API_CHECK(detail::isUInt64(*d_node))
2635
      << "Term should be a UInt64 when calling getUInt64()";
2636
  //////// all checks before this line
2637
14
  return detail::getInteger(*d_node).getUnsignedLong();
2638
  ////////
2639
  CVC4_API_TRY_CATCH_END;
2640
}
2641
2642
22
bool Term::isInteger() const { return detail::isInteger(*d_node); }
2643
22
std::string Term::getInteger() const
2644
{
2645
  CVC4_API_TRY_CATCH_BEGIN;
2646
22
  CVC4_API_CHECK_NOT_NULL;
2647
22
  CVC4_API_CHECK(detail::isInteger(*d_node))
2648
      << "Term should be an Int when calling getIntString()";
2649
  //////// all checks before this line
2650
22
  return detail::getInteger(*d_node).toString();
2651
  ////////
2652
  CVC4_API_TRY_CATCH_END;
2653
}
2654
2655
12096
bool Term::isString() const
2656
{
2657
  CVC4_API_TRY_CATCH_BEGIN;
2658
12096
  CVC4_API_CHECK_NOT_NULL;
2659
  //////// all checks before this line
2660
12096
  return d_node->getKind() == CVC4::Kind::CONST_STRING;
2661
  ////////
2662
  CVC4_API_TRY_CATCH_END;
2663
}
2664
2665
12083
std::wstring Term::getString() const
2666
{
2667
  CVC4_API_TRY_CATCH_BEGIN;
2668
12083
  CVC4_API_CHECK_NOT_NULL;
2669
12083
  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING)
2670
      << "Term should be a String when calling getString()";
2671
  //////// all checks before this line
2672
12083
  return d_node->getConst<CVC4::String>().toWString();
2673
  ////////
2674
  CVC4_API_TRY_CATCH_END;
2675
}
2676
2677
3351939
std::vector<Node> Term::termVectorToNodes(const std::vector<Term>& terms)
2678
{
2679
3351939
  std::vector<Node> res;
2680
10890928
  for (const Term& t : terms)
2681
  {
2682
7538989
    res.push_back(t.getNode());
2683
  }
2684
3351939
  return res;
2685
}
2686
2687
2452
std::ostream& operator<<(std::ostream& out, const Term& t)
2688
{
2689
2452
  out << t.toString();
2690
2452
  return out;
2691
}
2692
2693
std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector)
2694
{
2695
  container_to_stream(out, vector);
2696
  return out;
2697
}
2698
2699
std::ostream& operator<<(std::ostream& out, const std::set<Term>& set)
2700
{
2701
  container_to_stream(out, set);
2702
  return out;
2703
}
2704
2705
std::ostream& operator<<(
2706
    std::ostream& out,
2707
    const std::unordered_set<Term, TermHashFunction>& unordered_set)
2708
{
2709
  container_to_stream(out, unordered_set);
2710
  return out;
2711
}
2712
2713
template <typename V>
2714
std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map)
2715
{
2716
  container_to_stream(out, map);
2717
  return out;
2718
}
2719
2720
template <typename V>
2721
std::ostream& operator<<(
2722
    std::ostream& out,
2723
    const std::unordered_map<Term, V, TermHashFunction>& unordered_map)
2724
{
2725
  container_to_stream(out, unordered_map);
2726
  return out;
2727
}
2728
2729
3885239
size_t TermHashFunction::operator()(const Term& t) const
2730
{
2731
3885239
  return NodeHashFunction()(*t.d_node);
2732
}
2733
2734
/* Helpers                                                                    */
2735
/* -------------------------------------------------------------------------- */
2736
2737
/* Split out to avoid nested API calls (problematic with API tracing).        */
2738
/* .......................................................................... */
2739
2740
31187414
bool Term::isNullHelper() const
2741
{
2742
  /* Split out to avoid nested API calls (problematic with API tracing). */
2743
31187414
  return d_node->isNull();
2744
}
2745
2746
4934
Kind Term::getKindHelper() const
2747
{
2748
  /* Sequence kinds do not exist internally, so we must convert their internal
2749
   * (string) versions back to sequence. All operators where this is
2750
   * necessary are such that their first child is of sequence type, which
2751
   * we check here. */
2752
4934
  if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence())
2753
  {
2754
2
    switch (d_node->getKind())
2755
    {
2756
2
      case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT;
2757
      case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH;
2758
      case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT;
2759
      case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE;
2760
      case CVC4::Kind::STRING_CHARAT: return SEQ_AT;
2761
      case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS;
2762
      case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF;
2763
      case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE;
2764
      case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL;
2765
      case CVC4::Kind::STRING_REV: return SEQ_REV;
2766
      case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX;
2767
      case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX;
2768
      default:
2769
        // fall through to conversion below
2770
        break;
2771
    }
2772
  }
2773
  // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
2774
  // INTERNAL_KIND.
2775
4932
  if (isCastedReal())
2776
  {
2777
2
    return CONST_RATIONAL;
2778
  }
2779
4930
  return intToExtKind(d_node->getKind());
2780
}
2781
2782
5071
bool Term::isCastedReal() const
2783
{
2784
5071
  if (d_node->getKind() == kind::CAST_TO_REAL)
2785
  {
2786
6
    return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger();
2787
  }
2788
5065
  return false;
2789
}
2790
2791
/* -------------------------------------------------------------------------- */
2792
/* Datatypes                                                                  */
2793
/* -------------------------------------------------------------------------- */
2794
2795
/* DatatypeConstructorDecl -------------------------------------------------- */
2796
2797
DatatypeConstructorDecl::DatatypeConstructorDecl()
2798
    : d_solver(nullptr), d_ctor(nullptr)
2799
{
2800
}
2801
2802
2408
DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
2803
2408
                                                 const std::string& name)
2804
2408
    : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name))
2805
{
2806
2408
}
2807
4856
DatatypeConstructorDecl::~DatatypeConstructorDecl()
2808
{
2809
2428
  if (d_ctor != nullptr)
2810
  {
2811
    // ensure proper node manager is in scope
2812
4856
    NodeManagerScope scope(d_solver->getNodeManager());
2813
2428
    d_ctor.reset();
2814
  }
2815
2428
}
2816
2817
2324
void DatatypeConstructorDecl::addSelector(const std::string& name,
2818
                                          const Sort& sort)
2819
{
2820
4648
  NodeManagerScope scope(d_solver->getNodeManager());
2821
  CVC4_API_TRY_CATCH_BEGIN;
2822
2324
  CVC4_API_CHECK_NOT_NULL;
2823
2324
  CVC4_API_CHECK_SORT(sort);
2824
2322
  CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort)
2825
      << "non-null range sort for selector";
2826
  //////// all checks before this line
2827
2322
  d_ctor->addArg(name, *sort.d_type);
2828
  ////////
2829
  CVC4_API_TRY_CATCH_END;
2830
2322
}
2831
2832
32
void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
2833
{
2834
64
  NodeManagerScope scope(d_solver->getNodeManager());
2835
  CVC4_API_TRY_CATCH_BEGIN;
2836
32
  CVC4_API_CHECK_NOT_NULL;
2837
  //////// all checks before this line
2838
32
  d_ctor->addArgSelf(name);
2839
  ////////
2840
  CVC4_API_TRY_CATCH_END;
2841
32
}
2842
2843
2418
bool DatatypeConstructorDecl::isNull() const
2844
{
2845
  CVC4_API_TRY_CATCH_BEGIN;
2846
  //////// all checks before this line
2847
2418
  return isNullHelper();
2848
  ////////
2849
  CVC4_API_TRY_CATCH_END;
2850
}
2851
2852
std::string DatatypeConstructorDecl::toString() const
2853
{
2854
  CVC4_API_TRY_CATCH_BEGIN;
2855
  //////// all checks before this line
2856
  std::stringstream ss;
2857
  ss << *d_ctor;
2858
  return ss.str();
2859
  ////////
2860
  CVC4_API_TRY_CATCH_END;
2861
}
2862
2863
std::ostream& operator<<(std::ostream& out,
2864
                         const DatatypeConstructorDecl& ctordecl)
2865
{
2866
  out << ctordecl.toString();
2867
  return out;
2868
}
2869
2870
4
std::ostream& operator<<(std::ostream& out,
2871
                         const std::vector<DatatypeConstructorDecl>& vector)
2872
{
2873
4
  container_to_stream(out, vector);
2874
4
  return out;
2875
}
2876
2877
4774
bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor == nullptr; }
2878
2879
/* DatatypeDecl ------------------------------------------------------------- */
2880
2881
2
DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
2882
2883
717
DatatypeDecl::DatatypeDecl(const Solver* slv,
2884
                           const std::string& name,
2885
717
                           bool isCoDatatype)
2886
717
    : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype))
2887
{
2888
717
}
2889
2890
12
DatatypeDecl::DatatypeDecl(const Solver* slv,
2891
                           const std::string& name,
2892
                           const Sort& param,
2893
12
                           bool isCoDatatype)
2894
    : d_solver(slv),
2895
      d_dtype(new CVC4::DType(
2896
12
          name, std::vector<TypeNode>{*param.d_type}, isCoDatatype))
2897
{
2898
12
}
2899
2900
1167
DatatypeDecl::DatatypeDecl(const Solver* slv,
2901
                           const std::string& name,
2902
                           const std::vector<Sort>& params,
2903
1167
                           bool isCoDatatype)
2904
1167
    : d_solver(slv)
2905
{
2906
2334
  std::vector<TypeNode> tparams = Sort::sortVectorToTypeNodes(params);
2907
3501
  d_dtype = std::shared_ptr<CVC4::DType>(
2908
2334
      new CVC4::DType(name, tparams, isCoDatatype));
2909
1167
}
2910
2911
7594
bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
2912
2913
6922
DatatypeDecl::~DatatypeDecl()
2914
{
2915
3461
  if (d_dtype != nullptr)
2916
  {
2917
    // ensure proper node manager is in scope
2918
6918
    NodeManagerScope scope(d_solver->getNodeManager());
2919
3459
    d_dtype.reset();
2920
  }
2921
3461
}
2922
2923
2406
void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
2924
{
2925
4812
  NodeManagerScope scope(d_solver->getNodeManager());
2926
  CVC4_API_TRY_CATCH_BEGIN;
2927
2406
  CVC4_API_CHECK_NOT_NULL;
2928
2406
  CVC4_API_ARG_CHECK_NOT_NULL(ctor);
2929
2406
  CVC4_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor);
2930
  //////// all checks before this line
2931
2406
  d_dtype->addConstructor(ctor.d_ctor);
2932
  ////////
2933
  CVC4_API_TRY_CATCH_END;
2934
2406
}
2935
2936
1245
size_t DatatypeDecl::getNumConstructors() const
2937
{
2938
  CVC4_API_TRY_CATCH_BEGIN;
2939
1245
  CVC4_API_CHECK_NOT_NULL;
2940
  //////// all checks before this line
2941
1245
  return d_dtype->getNumConstructors();
2942
  ////////
2943
  CVC4_API_TRY_CATCH_END;
2944
}
2945
2946
bool DatatypeDecl::isParametric() const
2947
{
2948
  CVC4_API_TRY_CATCH_BEGIN;
2949
  CVC4_API_CHECK_NOT_NULL;
2950
  //////// all checks before this line
2951
  return d_dtype->isParametric();
2952
  ////////
2953
  CVC4_API_TRY_CATCH_END;
2954
}
2955
2956
2
std::string DatatypeDecl::toString() const
2957
{
2958
  CVC4_API_TRY_CATCH_BEGIN;
2959
2
  CVC4_API_CHECK_NOT_NULL;
2960
  //////// all checks before this line
2961
4
  std::stringstream ss;
2962
2
  ss << *d_dtype;
2963
4
  return ss.str();
2964
  ////////
2965
  CVC4_API_TRY_CATCH_END;
2966
}
2967
2968
10
std::string DatatypeDecl::getName() const
2969
{
2970
  CVC4_API_TRY_CATCH_BEGIN;
2971
10
  CVC4_API_CHECK_NOT_NULL;
2972
  //////// all checks before this line
2973
8
  return d_dtype->getName();
2974
  ////////
2975
  CVC4_API_TRY_CATCH_END;
2976
}
2977
2978
3931
bool DatatypeDecl::isNull() const
2979
{
2980
  CVC4_API_TRY_CATCH_BEGIN;
2981
  //////// all checks before this line
2982
3931
  return isNullHelper();
2983
  ////////
2984
  CVC4_API_TRY_CATCH_END;
2985
}
2986
2987
2
std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
2988
{
2989
2
  out << dtdecl.toString();
2990
2
  return out;
2991
}
2992
2993
1187
CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
2994
2995
/* DatatypeSelector --------------------------------------------------------- */
2996
2997
DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
2998
2999
2452
DatatypeSelector::DatatypeSelector(const Solver* slv,
3000
2452
                                   const CVC4::DTypeSelector& stor)
3001
2452
    : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor))
3002
{
3003
2452
  CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
3004
2452
}
3005
3006
4904
DatatypeSelector::~DatatypeSelector()
3007
{
3008
2452
  if (d_stor != nullptr)
3009
  {
3010
    // ensure proper node manager is in scope
3011
4904
    NodeManagerScope scope(d_solver->getNodeManager());
3012
2452
    d_stor.reset();
3013
  }
3014
2452
}
3015
3016
2223
std::string DatatypeSelector::getName() const
3017
{
3018
  CVC4_API_TRY_CATCH_BEGIN;
3019
2223
  CVC4_API_CHECK_NOT_NULL;
3020
  //////// all checks before this line
3021
2223
  return d_stor->getName();
3022
  ////////
3023
  CVC4_API_TRY_CATCH_END;
3024
}
3025
3026
2440
Term DatatypeSelector::getSelectorTerm() const
3027
{
3028
  CVC4_API_TRY_CATCH_BEGIN;
3029
2440
  CVC4_API_CHECK_NOT_NULL;
3030
  //////// all checks before this line
3031
2440
  return Term(d_solver, d_stor->getSelector());
3032
  ////////
3033
  CVC4_API_TRY_CATCH_END;
3034
}
3035
3036
10
Sort DatatypeSelector::getRangeSort() const
3037
{
3038
  CVC4_API_TRY_CATCH_BEGIN;
3039
10
  CVC4_API_CHECK_NOT_NULL;
3040
  //////// all checks before this line
3041
10
  return Sort(d_solver, d_stor->getRangeType());
3042
  ////////
3043
  CVC4_API_TRY_CATCH_END;
3044
}
3045
3046
bool DatatypeSelector::isNull() const
3047
{
3048
  CVC4_API_TRY_CATCH_BEGIN;
3049
  //////// all checks before this line
3050
  return isNullHelper();
3051
  ////////
3052
  CVC4_API_TRY_CATCH_END;
3053
}
3054
3055
std::string DatatypeSelector::toString() const
3056
{
3057
  CVC4_API_TRY_CATCH_BEGIN;
3058
  //////// all checks before this line
3059
  std::stringstream ss;
3060
  ss << *d_stor;
3061
  return ss.str();
3062
  ////////
3063
  CVC4_API_TRY_CATCH_END;
3064
}
3065
3066
std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
3067
{
3068
  out << stor.toString();
3069
  return out;
3070
}
3071
3072
4673
bool DatatypeSelector::isNullHelper() const { return d_stor == nullptr; }
3073
3074
/* DatatypeConstructor ------------------------------------------------------ */
3075
3076
DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3077
{
3078
}
3079
3080
5728
DatatypeConstructor::DatatypeConstructor(const Solver* slv,
3081
5728
                                         const CVC4::DTypeConstructor& ctor)
3082
5728
    : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor))
3083
{
3084
5728
  CVC4_API_CHECK(d_ctor->isResolved())
3085
      << "Expected resolved datatype constructor";
3086
5728
}
3087
3088
11456
DatatypeConstructor::~DatatypeConstructor()
3089
{
3090
5728
  if (d_ctor != nullptr)
3091
  {
3092
    // ensure proper node manager is in scope
3093
11456
    NodeManagerScope scope(d_solver->getNodeManager());
3094
5728
    d_ctor.reset();
3095
  }
3096
5728
}
3097
3098
2246
std::string DatatypeConstructor::getName() const
3099
{
3100
  CVC4_API_TRY_CATCH_BEGIN;
3101
2246
  CVC4_API_CHECK_NOT_NULL;
3102
  //////// all checks before this line
3103
2246
  return d_ctor->getName();
3104
  ////////
3105
  CVC4_API_TRY_CATCH_END;
3106
}
3107
3108
4089
Term DatatypeConstructor::getConstructorTerm() const
3109
{
3110
  CVC4_API_TRY_CATCH_BEGIN;
3111
4089
  CVC4_API_CHECK_NOT_NULL;
3112
  //////// all checks before this line
3113
4089
  return Term(d_solver, d_ctor->getConstructor());
3114
  ////////
3115
  CVC4_API_TRY_CATCH_END;
3116
}
3117
3118
42
Term DatatypeConstructor::getSpecializedConstructorTerm(
3119
    const Sort& retSort) const
3120
{
3121
84
  NodeManagerScope scope(d_solver->getNodeManager());
3122
  CVC4_API_TRY_CATCH_BEGIN;
3123
42
  CVC4_API_CHECK_NOT_NULL;
3124
42
  CVC4_API_CHECK(d_ctor->isResolved())
3125
      << "Expected resolved datatype constructor";
3126
44
  CVC4_API_CHECK(retSort.isDatatype())
3127
2
      << "Cannot get specialized constructor type for non-datatype type "
3128
      << retSort;
3129
  //////// all checks before this line
3130
3131
40
  NodeManager* nm = d_solver->getNodeManager();
3132
  Node ret =
3133
      nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
3134
80
                 nm->mkConst(AscriptionType(
3135
80
                     d_ctor->getSpecializedConstructorType(*retSort.d_type))),
3136
160
                 d_ctor->getConstructor());
3137
40
  (void)ret.getType(true); /* kick off type checking */
3138
  // apply type ascription to the operator
3139
80
  Term sctor = api::Term(d_solver, ret);
3140
80
  return sctor;
3141
  ////////
3142
  CVC4_API_TRY_CATCH_END;
3143
}
3144
3145
3619
Term DatatypeConstructor::getTesterTerm() const
3146
{
3147
  CVC4_API_TRY_CATCH_BEGIN;
3148
3619
  CVC4_API_CHECK_NOT_NULL;
3149
  //////// all checks before this line
3150
3619
  return Term(d_solver, d_ctor->getTester());
3151
  ////////
3152
  CVC4_API_TRY_CATCH_END;
3153
}
3154
3155
2392
size_t DatatypeConstructor::getNumSelectors() const
3156
{
3157
  CVC4_API_TRY_CATCH_BEGIN;
3158
2392
  CVC4_API_CHECK_NOT_NULL;
3159
  //////// all checks before this line
3160
2392
  return d_ctor->getNumArgs();
3161
  ////////
3162
  CVC4_API_TRY_CATCH_END;
3163
}
3164
3165
2303
DatatypeSelector DatatypeConstructor::operator[](size_t index) const
3166
{
3167
  CVC4_API_TRY_CATCH_BEGIN;
3168
2303
  CVC4_API_CHECK_NOT_NULL;
3169
  //////// all checks before this line
3170
2303
  return DatatypeSelector(d_solver, (*d_ctor)[index]);
3171
  ////////
3172
  CVC4_API_TRY_CATCH_END;
3173
}
3174
3175
127
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
3176
{
3177
  CVC4_API_TRY_CATCH_BEGIN;
3178
127
  CVC4_API_CHECK_NOT_NULL;
3179
  //////// all checks before this line
3180
127
  return getSelectorForName(name);
3181
  ////////
3182
  CVC4_API_TRY_CATCH_END;
3183
}
3184
3185
24
DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
3186
{
3187
  CVC4_API_TRY_CATCH_BEGIN;
3188
24
  CVC4_API_CHECK_NOT_NULL;
3189
  //////// all checks before this line
3190
24
  return getSelectorForName(name);
3191
  ////////
3192
  CVC4_API_TRY_CATCH_END;
3193
}
3194
3195
18
Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
3196
{
3197
  CVC4_API_TRY_CATCH_BEGIN;
3198
18
  CVC4_API_CHECK_NOT_NULL;
3199
  //////// all checks before this line
3200
18
  return getSelector(name).getSelectorTerm();
3201
  ////////
3202
  CVC4_API_TRY_CATCH_END;
3203
}
3204
3205
DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
3206
{
3207
  return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);
3208
}
3209
3210
DatatypeConstructor::const_iterator DatatypeConstructor::end() const
3211
{
3212
  return DatatypeConstructor::const_iterator(d_solver, *d_ctor, false);
3213
}
3214
3215
DatatypeConstructor::const_iterator::const_iterator(
3216
    const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin)
3217
{
3218
  d_solver = slv;
3219
  d_int_stors = &ctor.getArgs();
3220
3221
  const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels =
3222
      ctor.getArgs();
3223
  for (const std::shared_ptr<CVC4::DTypeSelector>& s : sels)
3224
  {
3225
    /* Can not use emplace_back here since constructor is private. */
3226
    d_stors.push_back(DatatypeSelector(d_solver, *s.get()));
3227
  }
3228
  d_idx = begin ? 0 : sels.size();
3229
}
3230
3231
DatatypeConstructor::const_iterator::const_iterator()
3232
    : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3233
{
3234
}
3235
3236
DatatypeConstructor::const_iterator&
3237
DatatypeConstructor::const_iterator::operator=(
3238
    const DatatypeConstructor::const_iterator& it)
3239
{
3240
  d_solver = it.d_solver;
3241
  d_int_stors = it.d_int_stors;
3242
  d_stors = it.d_stors;
3243
  d_idx = it.d_idx;
3244
  return *this;
3245
}
3246
3247
const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const
3248
{
3249
  return d_stors[d_idx];
3250
}
3251
3252
const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const
3253
{
3254
  return &d_stors[d_idx];
3255
}
3256
3257
DatatypeConstructor::const_iterator&
3258
DatatypeConstructor::const_iterator::operator++()
3259
{
3260
  ++d_idx;
3261
  return *this;
3262
}
3263
3264
DatatypeConstructor::const_iterator
3265
DatatypeConstructor::const_iterator::operator++(int)
3266
{
3267
  DatatypeConstructor::const_iterator it(*this);
3268
  ++d_idx;
3269
  return it;
3270
}
3271
3272
bool DatatypeConstructor::const_iterator::operator==(
3273
    const DatatypeConstructor::const_iterator& other) const
3274
{
3275
  return d_int_stors == other.d_int_stors && d_idx == other.d_idx;
3276
}
3277
3278
bool DatatypeConstructor::const_iterator::operator!=(
3279
    const DatatypeConstructor::const_iterator& other) const
3280
{
3281
  return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
3282
}
3283
3284
bool DatatypeConstructor::isNull() const
3285
{
3286
  CVC4_API_TRY_CATCH_BEGIN;
3287
  //////// all checks before this line
3288
  return isNullHelper();
3289
  ////////
3290
  CVC4_API_TRY_CATCH_END;
3291
}
3292
3293
std::string DatatypeConstructor::toString() const
3294
{
3295
  CVC4_API_TRY_CATCH_BEGIN;
3296
  //////// all checks before this line
3297
  std::stringstream ss;
3298
  ss << *d_ctor;
3299
  return ss.str();
3300
  ////////
3301
  CVC4_API_TRY_CATCH_END;
3302
}
3303
3304
14860
bool DatatypeConstructor::isNullHelper() const { return d_ctor == nullptr; }
3305
3306
151
DatatypeSelector DatatypeConstructor::getSelectorForName(
3307
    const std::string& name) const
3308
{
3309
151
  bool foundSel = false;
3310
151
  size_t index = 0;
3311
277
  for (size_t i = 0, nsels = getNumSelectors(); i < nsels; i++)
3312
  {
3313
275
    if ((*d_ctor)[i].getName() == name)
3314
    {
3315
149
      index = i;
3316
149
      foundSel = true;
3317
149
      break;
3318
    }
3319
  }
3320
151
  if (!foundSel)
3321
  {
3322
4
    std::stringstream snames;
3323
2
    snames << "{ ";
3324
6
    for (size_t i = 0, ncons = getNumSelectors(); i < ncons; i++)
3325
    {
3326
4
      snames << (*d_ctor)[i].getName() << " ";
3327
    }
3328
2
    snames << "} ";
3329
10
    CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
3330
8
                             << getName() << " exists among " << snames.str();
3331
  }
3332
149
  return DatatypeSelector(d_solver, (*d_ctor)[index]);
3333
}
3334
3335
std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
3336
{
3337
  out << ctor.toString();
3338
  return out;
3339
}
3340
3341
/* Datatype ----------------------------------------------------------------- */
3342
3343
5821
Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype)
3344
5821
    : d_solver(slv), d_dtype(new CVC4::DType(dtype))
3345
{
3346
5821
  CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
3347
5821
}
3348
3349
Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
3350
3351
11642
Datatype::~Datatype()
3352
{
3353
5821
  if (d_dtype != nullptr)
3354
  {
3355
    // ensure proper node manager is in scope
3356
11642
    NodeManagerScope scope(d_solver->getNodeManager());
3357
5821
    d_dtype.reset();
3358
  }
3359
5821
}
3360
3361
4260
DatatypeConstructor Datatype::operator[](size_t idx) const
3362
{
3363
  CVC4_API_TRY_CATCH_BEGIN;
3364
4260
  CVC4_API_CHECK_NOT_NULL;
3365
4260
  CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
3366
  //////// all checks before this line
3367
4258
  return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
3368
  ////////
3369
  CVC4_API_TRY_CATCH_END;
3370
}
3371
3372
24
DatatypeConstructor Datatype::operator[](const std::string& name) const
3373
{
3374
  CVC4_API_TRY_CATCH_BEGIN;
3375
24
  CVC4_API_CHECK_NOT_NULL;
3376
  //////// all checks before this line
3377
24
  return getConstructorForName(name);
3378
  ////////
3379
  CVC4_API_TRY_CATCH_END;
3380
}
3381
3382
1450
DatatypeConstructor Datatype::getConstructor(const std::string& name) const
3383
{
3384
  CVC4_API_TRY_CATCH_BEGIN;
3385
1450
  CVC4_API_CHECK_NOT_NULL;
3386
  //////// all checks before this line
3387
1450
  return getConstructorForName(name);
3388
  ////////
3389
  CVC4_API_TRY_CATCH_END;
3390
}
3391
3392
24
Term Datatype::getConstructorTerm(const std::string& name) const
3393
{
3394
  CVC4_API_TRY_CATCH_BEGIN;
3395
24
  CVC4_API_CHECK_NOT_NULL;
3396
  //////// all checks before this line
3397
24
  return getConstructor(name).getConstructorTerm();
3398
  ////////
3399
  CVC4_API_TRY_CATCH_END;
3400
}
3401
3402
1167
std::string Datatype::getName() const
3403
{
3404
  CVC4_API_TRY_CATCH_BEGIN;
3405
1167
  CVC4_API_CHECK_NOT_NULL;
3406
  //////// all checks before this line
3407
1167
  return d_dtype->getName();
3408
  ////////
3409
  CVC4_API_TRY_CATCH_END;
3410
}
3411
3412
6895
size_t Datatype::getNumConstructors() const
3413
{
3414
  CVC4_API_TRY_CATCH_BEGIN;
3415
6895
  CVC4_API_CHECK_NOT_NULL;
3416
  //////// all checks before this line
3417
6895
  return d_dtype->getNumConstructors();
3418
  ////////
3419
  CVC4_API_TRY_CATCH_END;
3420
}
3421
3422
12
bool Datatype::isParametric() const
3423
{
3424
  CVC4_API_TRY_CATCH_BEGIN;
3425
12
  CVC4_API_CHECK_NOT_NULL;
3426
  //////// all checks before this line
3427
12
  return d_dtype->isParametric();
3428
  ////////
3429
  CVC4_API_TRY_CATCH_END;
3430
}
3431
3432
1158
bool Datatype::isCodatatype() const
3433
{
3434
  CVC4_API_TRY_CATCH_BEGIN;
3435
1158
  CVC4_API_CHECK_NOT_NULL;
3436
  //////// all checks before this line
3437
1158
  return d_dtype->isCodatatype();
3438
  ////////
3439
  CVC4_API_TRY_CATCH_END;
3440
}
3441
3442
8
bool Datatype::isTuple() const
3443
{
3444
  CVC4_API_TRY_CATCH_BEGIN;
3445
8
  CVC4_API_CHECK_NOT_NULL;
3446
  //////// all checks before this line
3447
8
  return d_dtype->isTuple();
3448
  ////////
3449
  CVC4_API_TRY_CATCH_END;
3450
}
3451
3452
6
bool Datatype::isRecord() const
3453
{
3454
  CVC4_API_TRY_CATCH_BEGIN;
3455
6
  CVC4_API_CHECK_NOT_NULL;
3456
  //////// all checks before this line
3457
6
  return d_dtype->isRecord();
3458
  ////////
3459
  CVC4_API_TRY_CATCH_END;
3460
}
3461
3462
14
bool Datatype::isFinite() const
3463
{
3464
  CVC4_API_TRY_CATCH_BEGIN;
3465
14
  CVC4_API_CHECK_NOT_NULL;
3466
  //////// all checks before this line
3467
14
  return d_dtype->isFinite();
3468
  ////////
3469
  CVC4_API_TRY_CATCH_END;
3470
}
3471
3472
1154
bool Datatype::isWellFounded() const
3473
{
3474
  CVC4_API_TRY_CATCH_BEGIN;
3475
1154
  CVC4_API_CHECK_NOT_NULL;
3476
  //////// all checks before this line
3477
1154
  return d_dtype->isWellFounded();
3478
  ////////
3479
  CVC4_API_TRY_CATCH_END;
3480
}
3481
18
bool Datatype::hasNestedRecursion() const
3482
{
3483
  CVC4_API_TRY_CATCH_BEGIN;
3484
18
  CVC4_API_CHECK_NOT_NULL;
3485
  //////// all checks before this line
3486
18
  return d_dtype->hasNestedRecursion();
3487
  ////////
3488
  CVC4_API_TRY_CATCH_END;
3489
}
3490
3491
bool Datatype::isNull() const
3492
{
3493
  CVC4_API_TRY_CATCH_BEGIN;
3494
  CVC4_API_CHECK_NOT_NULL;
3495
  //////// all checks before this line
3496
  return isNullHelper();
3497
  ////////
3498
  CVC4_API_TRY_CATCH_END;
3499
}
3500
3501
std::string Datatype::toString() const
3502
{
3503
  CVC4_API_TRY_CATCH_BEGIN;
3504
  CVC4_API_CHECK_NOT_NULL;
3505
  //////// all checks before this line
3506
  return d_dtype->getName();
3507
  ////////
3508
  CVC4_API_TRY_CATCH_END;
3509
}
3510
3511
Datatype::const_iterator Datatype::begin() const
3512
{
3513
  return Datatype::const_iterator(d_solver, *d_dtype, true);
3514
}
3515
3516
Datatype::const_iterator Datatype::end() const
3517
{
3518
  return Datatype::const_iterator(d_solver, *d_dtype, false);
3519
}
3520
3521
1474
DatatypeConstructor Datatype::getConstructorForName(
3522
    const std::string& name) const
3523
{
3524
1474
  bool foundCons = false;
3525
1474
  size_t index = 0;
3526
2942
  for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
3527
  {
3528
2938
    if ((*d_dtype)[i].getName() == name)
3529
    {
3530
1470
      index = i;
3531
1470
      foundCons = true;
3532
1470
      break;
3533
    }
3534
  }
3535
1474
  if (!foundCons)
3536
  {
3537
8
    std::stringstream snames;
3538
4
    snames << "{ ";
3539
12
    for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
3540
    {
3541
8
      snames << (*d_dtype)[i].getName() << " ";
3542
    }
3543
4
    snames << "}";
3544
20
    CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
3545
16
                              << getName() << " exists, among " << snames.str();
3546
  }
3547
1470
  return DatatypeConstructor(d_solver, (*d_dtype)[index]);
3548
}
3549
3550
Datatype::const_iterator::const_iterator(const Solver* slv,
3551
                                         const CVC4::DType& dtype,
3552
                                         bool begin)
3553
    : d_solver(slv), d_int_ctors(&dtype.getConstructors())
3554
{
3555
  const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
3556
      dtype.getConstructors();
3557
  for (const std::shared_ptr<DTypeConstructor>& c : cons)
3558
  {
3559
    /* Can not use emplace_back here since constructor is private. */
3560
    d_ctors.push_back(DatatypeConstructor(d_solver, *c.get()));
3561
  }
3562
  d_idx = begin ? 0 : cons.size();
3563
}
3564
3565
Datatype::const_iterator::const_iterator()
3566
    : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
3567
{
3568
}
3569
3570
Datatype::const_iterator& Datatype::const_iterator::operator=(
3571
    const Datatype::const_iterator& it)
3572
{
3573
  d_solver = it.d_solver;
3574
  d_int_ctors = it.d_int_ctors;
3575
  d_ctors = it.d_ctors;
3576
  d_idx = it.d_idx;
3577
  return *this;
3578
}
3579
3580
const DatatypeConstructor& Datatype::const_iterator::operator*() const
3581
{
3582
  return d_ctors[d_idx];
3583
}
3584
3585
const DatatypeConstructor* Datatype::const_iterator::operator->() const
3586
{
3587
  return &d_ctors[d_idx];
3588
}
3589
3590
Datatype::const_iterator& Datatype::const_iterator::operator++()
3591
{
3592
  ++d_idx;
3593
  return *this;
3594
}
3595
3596
Datatype::const_iterator Datatype::const_iterator::operator++(int)
3597
{
3598
  Datatype::const_iterator it(*this);
3599
  ++d_idx;
3600
  return it;
3601
}
3602
3603
bool Datatype::const_iterator::operator==(
3604
    const Datatype::const_iterator& other) const
3605
{
3606
  return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx;
3607
}
3608
3609
bool Datatype::const_iterator::operator!=(
3610
    const Datatype::const_iterator& other) const
3611
{
3612
  return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
3613
}
3614
3615
16190
bool Datatype::isNullHelper() const { return d_dtype == nullptr; }
3616
3617
/* -------------------------------------------------------------------------- */
3618
/* Grammar                                                                    */
3619
/* -------------------------------------------------------------------------- */
3620
3621
Grammar::Grammar()
3622
    : d_solver(nullptr),
3623
      d_sygusVars(),
3624
      d_ntSyms(),
3625
      d_ntsToTerms(0),
3626
      d_allowConst(),
3627
      d_allowVars(),
3628
      d_isResolved(false)
3629
{
3630
}
3631
3632
303
Grammar::Grammar(const Solver* slv,
3633
                 const std::vector<Term>& sygusVars,
3634
303
                 const std::vector<Term>& ntSymbols)
3635
    : d_solver(slv),
3636
      d_sygusVars(sygusVars),
3637
      d_ntSyms(ntSymbols),
3638
      d_ntsToTerms(ntSymbols.size()),
3639
      d_allowConst(),
3640
      d_allowVars(),
3641
303
      d_isResolved(false)
3642
{
3643
961
  for (Term ntsymbol : d_ntSyms)
3644
  {
3645
658
    d_ntsToTerms.emplace(ntsymbol, std::vector<Term>());
3646
  }
3647
303
}
3648
3649
2675
void Grammar::addRule(const Term& ntSymbol, const Term& rule)
3650
{
3651
  CVC4_API_TRY_CATCH_BEGIN;
3652
2677
  CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
3653
2
                                   "it as an argument to synthFun/synthInv";
3654
2673
  CVC4_API_CHECK_TERM(ntSymbol);
3655
2671
  CVC4_API_CHECK_TERM(rule);
3656
2671
  CVC4_API_ARG_CHECK_EXPECTED(
3657
      d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
3658
      << "ntSymbol to be one of the non-terminal symbols given in the "
3659
2
         "predeclaration";
3660
2669
  CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType())
3661
2
      << "Expected ntSymbol and rule to have the same sort";
3662
  //////// all checks before this line
3663
2665
  d_ntsToTerms[ntSymbol].push_back(rule);
3664
  ////////
3665
  CVC4_API_TRY_CATCH_END;
3666
2665
}
3667
3668
12
void Grammar::addRules(const Term& ntSymbol, const std::vector<Term>& rules)
3669
{
3670
  CVC4_API_TRY_CATCH_BEGIN;
3671
14
  CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
3672
2
                                   "it as an argument to synthFun/synthInv";
3673
10
  CVC4_API_CHECK_TERM(ntSymbol);
3674
8
  CVC4_API_CHECK_TERMS_WITH_SORT(rules, ntSymbol.getSort());
3675
6
  CVC4_API_ARG_CHECK_EXPECTED(
3676
      d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
3677
      << "ntSymbol to be one of the non-terminal symbols given in the "
3678
2
         "predeclaration";
3679
  //////// all checks before this line
3680
4
  d_ntsToTerms[ntSymbol].insert(
3681
2
      d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend());
3682
  ////////
3683
  CVC4_API_TRY_CATCH_END;
3684
2
}
3685
3686
40
void Grammar::addAnyConstant(const Term& ntSymbol)
3687
{
3688
  CVC4_API_TRY_CATCH_BEGIN;
3689
42
  CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
3690
2
                                   "it as an argument to synthFun/synthInv";
3691
38
  CVC4_API_CHECK_TERM(ntSymbol);
3692
38
  CVC4_API_ARG_CHECK_EXPECTED(
3693
      d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
3694
      << "ntSymbol to be one of the non-terminal symbols given in the "
3695
2
         "predeclaration";
3696
  //////// all checks before this line
3697
34
  d_allowConst.insert(ntSymbol);
3698
  ////////
3699
  CVC4_API_TRY_CATCH_END;
3700
34
}
3701
3702
32
void Grammar::addAnyVariable(const Term& ntSymbol)
3703
{
3704
  CVC4_API_TRY_CATCH_BEGIN;
3705
34
  CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
3706
2
                                   "it as an argument to synthFun/synthInv";
3707
30
  CVC4_API_CHECK_TERM(ntSymbol);
3708
30
  CVC4_API_ARG_CHECK_EXPECTED(
3709
      d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
3710
      << "ntSymbol to be one of the non-terminal symbols given in the "
3711
2
         "predeclaration";
3712
  //////// all checks before this line
3713
26
  d_allowVars.insert(ntSymbol);
3714
  ////////
3715
  CVC4_API_TRY_CATCH_END;
3716
26
}
3717
3718
/**
3719
 * this function concatinates the outputs of calling f on each element between
3720
 * first and last, seperated by sep.
3721
 * @param first the beginning of the range
3722
 * @param last the end of the range
3723
 * @param f the function to call on each element in the range, its output must
3724
 *          be overloaded for operator<<
3725
 * @param sep the string to add between successive calls to f
3726
 */
3727
template <typename Iterator, typename Function>
3728
std::string join(Iterator first, Iterator last, Function f, std::string sep)
3729
{
3730
  std::stringstream ss;
3731
  Iterator i = first;
3732
3733
  if (i != last)
3734
  {
3735
    ss << f(*i);
3736
    ++i;
3737
  }
3738
3739
  while (i != last)
3740
  {
3741
    ss << sep << f(*i);
3742
    ++i;
3743
  }
3744
3745
  return ss.str();
3746
}
3747
3748
std::string Grammar::toString() const
3749
{
3750
  CVC4_API_TRY_CATCH_BEGIN;
3751
  //////// all checks before this line
3752
  std::stringstream ss;
3753
  ss << "  ("  // pre-declaration
3754
     << join(
3755
            d_ntSyms.cbegin(),
3756
            d_ntSyms.cend(),
3757
            [](const Term& t) {
3758
              std::stringstream s;
3759
              s << '(' << t << ' ' << t.getSort() << ')';
3760
              return s.str();
3761
            },
3762
            " ")
3763
     << ")\n  ("  // grouped rule listing
3764
     << join(
3765
            d_ntSyms.cbegin(),
3766
            d_ntSyms.cend(),
3767
            [this](const Term& t) {
3768
              bool allowConst = d_allowConst.find(t) != d_allowConst.cend(),
3769
                   allowVars = d_allowVars.find(t) != d_allowVars.cend();
3770
              const std::vector<Term>& rules = d_ntsToTerms.at(t);
3771
              std::stringstream s;
3772
              s << '(' << t << ' ' << t.getSort() << " ("
3773
                << (allowConst ? "(Constant " + t.getSort().toString() + ")"
3774
                               : "")
3775
                << (allowConst && allowVars ? " " : "")
3776
                << (allowVars ? "(Var " + t.getSort().toString() + ")" : "")
3777
                << ((allowConst || allowVars) && !rules.empty() ? " " : "")
3778
                << join(
3779
                       rules.cbegin(),
3780
                       rules.cend(),
3781
                       [](const Term& rule) { return rule.toString(); },
3782
                       " ")
3783
                << "))";
3784
              return s.str();
3785
            },
3786
            "\n   ")
3787
     << ')';
3788
3789
  return ss.str();
3790
  ////////
3791
  CVC4_API_TRY_CATCH_END;
3792
}
3793
3794
290
Sort Grammar::resolve()
3795
{
3796
  CVC4_API_TRY_CATCH_BEGIN;
3797
  //////// all checks before this line
3798
3799
290
  d_isResolved = true;
3800
3801
580
  Term bvl;
3802
3803
290
  if (!d_sygusVars.empty())
3804
  {
3805
248
    bvl = Term(
3806
        d_solver,
3807
744
        d_solver->getNodeManager()->mkNode(
3808
496
            CVC4::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars)));
3809
  }
3810
3811
580
  std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
3812
3813
931
  for (Term ntsymbol : d_ntSyms)
3814
  {
3815
    // make the unresolved type, used for referencing the final version of
3816
    // the ntsymbol's datatype
3817
641
    ntsToUnres[ntsymbol] =
3818
1282
        Sort(d_solver, d_solver->getNodeManager()->mkSort(ntsymbol.toString()));
3819
  }
3820
3821
580
  std::vector<CVC4::DType> datatypes;
3822
580
  std::set<TypeNode> unresTypes;
3823
3824
290
  datatypes.reserve(d_ntSyms.size());
3825
3826
931
  for (const Term& ntSym : d_ntSyms)
3827
  {
3828
    // make the datatype, which encodes terms generated by this non-terminal
3829
1282
    DatatypeDecl dtDecl(d_solver, ntSym.toString());
3830
3831
3299
    for (const Term& consTerm : d_ntsToTerms[ntSym])
3832
    {
3833
2658
      addSygusConstructorTerm(dtDecl, consTerm, ntsToUnres);
3834
    }
3835
3836
641
    if (d_allowVars.find(ntSym) != d_allowVars.cend())
3837
    {
3838
22
      addSygusConstructorVariables(dtDecl,
3839
44
                                   Sort(d_solver, ntSym.d_node->getType()));
3840
    }
3841
3842
641
    bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
3843
1282
    TypeNode btt = ntSym.d_node->getType();
3844
641
    dtDecl.d_dtype->setSygus(btt, *bvl.d_node, aci, false);
3845
3846
    // We can be in a case where the only rule specified was (Variable T)
3847
    // and there are no variables of type T, in which case this is a bogus
3848
    // grammar. This results in the error below.
3849
641
    CVC4_API_CHECK(dtDecl.d_dtype->getNumConstructors() != 0)
3850
        << "Grouped rule listing for " << *dtDecl.d_dtype
3851
        << " produced an empty rule list";
3852
3853
641
    datatypes.push_back(*dtDecl.d_dtype);
3854
641
    unresTypes.insert(*ntsToUnres[ntSym].d_type);
3855
  }
3856
3857
  std::vector<TypeNode> datatypeTypes =
3858
290
      d_solver->getNodeManager()->mkMutualDatatypeTypes(
3859
580
          datatypes, unresTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
3860
3861
  // return is the first datatype
3862
580
  return Sort(d_solver, datatypeTypes[0]);
3863
  ////////
3864
  CVC4_API_TRY_CATCH_END;
3865
}
3866
3867
2658
void Grammar::addSygusConstructorTerm(
3868
    DatatypeDecl& dt,
3869
    const Term& term,
3870
    const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
3871
{
3872
  CVC4_API_TRY_CATCH_BEGIN;
3873
2658
  CVC4_API_CHECK_DTDECL(dt);
3874
2658
  CVC4_API_CHECK_TERM(term);
3875
2658
  CVC4_API_CHECK_TERMS_MAP(ntsToUnres);
3876
  //////// all checks before this line
3877
3878
  // At this point, we should know that dt is well founded, and that its
3879
  // builtin sygus operators are well-typed.
3880
  // Now, purify each occurrence of a non-terminal symbol in term, replace by
3881
  // free variables. These become arguments to constructors. Notice we must do
3882
  // a tree traversal in this function, since unique paths to the same term
3883
  // should be treated as distinct terms.
3884
  // Notice that let expressions are forbidden in the input syntax of term, so
3885
  // this does not lead to exponential behavior with respect to input size.
3886
5316
  std::vector<Term> args;
3887
5316
  std::vector<Sort> cargs;
3888
5316
  Term op = purifySygusGTerm(term, args, cargs, ntsToUnres);
3889
5316
  std::stringstream ssCName;
3890
2658
  ssCName << op.getKind();
3891
2658
  if (!args.empty())
3892
  {
3893
    Term lbvl =
3894
1470
        Term(d_solver,
3895
4410
             d_solver->getNodeManager()->mkNode(CVC4::kind::BOUND_VAR_LIST,
3896
5880
                                                Term::termVectorToNodes(args)));
3897
    // its operator is a lambda
3898
1470
    op = Term(d_solver,
3899
5880
              d_solver->getNodeManager()->mkNode(
3900
2940
                  CVC4::kind::LAMBDA, *lbvl.d_node, *op.d_node));
3901
  }
3902
5316
  std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs);
3903
2658
  dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
3904
  ////////
3905
  CVC4_API_TRY_CATCH_END;
3906
2658
}
3907
3908
5590
Term Grammar::purifySygusGTerm(
3909
    const Term& term,
3910
    std::vector<Term>& args,
3911
    std::vector<Sort>& cargs,
3912
    const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
3913
{
3914
  CVC4_API_TRY_CATCH_BEGIN;
3915
5590
  CVC4_API_CHECK_TERM(term);
3916
5590
  CVC4_API_CHECK_TERMS(args);
3917
5590
  CVC4_API_CHECK_SORTS(cargs);
3918
5590
  CVC4_API_CHECK_TERMS_MAP(ntsToUnres);
3919
  //////// all checks before this line
3920
3921
  std::unordered_map<Term, Sort, TermHashFunction>::const_iterator itn =
3922
5590
      ntsToUnres.find(term);
3923
5590
  if (itn != ntsToUnres.cend())
3924
  {
3925
    Term ret =
3926
2802
        Term(d_solver,
3927
8406
             d_solver->getNodeManager()->mkBoundVar(term.d_node->getType()));
3928
2802
    args.push_back(ret);
3929
2802
    cargs.push_back(itn->second);
3930
2802
    return ret;
3931
  }
3932
5576
  std::vector<Term> pchildren;
3933
2788
  bool childChanged = false;
3934
5720
  for (unsigned i = 0, nchild = term.d_node->getNumChildren(); i < nchild; i++)
3935
  {
3936
    Term ptermc = purifySygusGTerm(
3937
5864
        Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres);
3938
2932
    pchildren.push_back(ptermc);
3939
2932
    childChanged = childChanged || *ptermc.d_node != (*term.d_node)[i];
3940
  }
3941
2788
  if (!childChanged)
3942
  {
3943
1336
    return term;
3944
  }
3945
3946
2904
  Node nret;
3947
3948
1452
  if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
3949
  {
3950
    // it's an indexed operator so we should provide the op
3951
454
    NodeBuilder<> nb(term.d_node->getKind());
3952
227
    nb << term.d_node->getOperator();
3953
227
    nb.append(Term::termVectorToNodes(pchildren));
3954
227
    nret = nb.constructNode();
3955
  }
3956
  else
3957
  {
3958
2450
    nret = d_solver->getNodeManager()->mkNode(
3959
2450
        term.d_node->getKind(), Term::termVectorToNodes(pchildren));
3960
  }
3961
3962
1452
  return Term(d_solver, nret);
3963
  ////////
3964
  CVC4_API_TRY_CATCH_END;
3965
}
3966
3967
22
void Grammar::addSygusConstructorVariables(DatatypeDecl& dt,
3968
                                           const Sort& sort) const
3969
{
3970
  CVC4_API_TRY_CATCH_BEGIN;
3971
22
  CVC4_API_CHECK_DTDECL(dt);
3972
22
  CVC4_API_CHECK_SORT(sort);
3973
  //////// all checks before this line
3974
3975
  // each variable of appropriate type becomes a sygus constructor in dt.
3976
102
  for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++)
3977
  {
3978
160
    Term v = d_sygusVars[i];
3979
80
    if (v.d_node->getType() == *sort.d_type)
3980
    {
3981
128
      std::stringstream ss;
3982
64
      ss << v;
3983
128
      std::vector<TypeNode> cargs;
3984
64
      dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs);
3985
    }
3986
  }
3987
  ////////
3988
  CVC4_API_TRY_CATCH_END;
3989
22
}
3990
3991
std::ostream& operator<<(std::ostream& out, const Grammar& grammar)
3992
{
3993
  return out << grammar.toString();
3994
}
3995
3996
/* -------------------------------------------------------------------------- */
3997
/* Rounding Mode for Floating Points                                          */
3998
/* -------------------------------------------------------------------------- */
3999
4000
const static std::
4001
    unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction>
4002
8895
        s_rmodes{
4003
            {ROUND_NEAREST_TIES_TO_EVEN,
4004
             CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN},
4005
            {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE},
4006
            {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_NEGATIVE},
4007
            {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO},
4008
            {ROUND_NEAREST_TIES_TO_AWAY,
4009
             CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY},
4010
        };
4011
4012
const static std::unordered_map<CVC4::RoundingMode,
4013
                                RoundingMode,
4014
                                CVC4::RoundingModeHashFunction>
4015
8895
    s_rmodes_internal{
4016
        {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN,
4017
         ROUND_NEAREST_TIES_TO_EVEN},
4018
        {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE},
4019
        {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE},
4020
        {CVC4::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO},
4021
        {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
4022
         ROUND_NEAREST_TIES_TO_AWAY},
4023
    };
4024
4025
58079
size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
4026
{
4027
58079
  return size_t(rm);
4028
}
4029
4030
/* -------------------------------------------------------------------------- */
4031
/* Solver                                                                     */
4032
/* -------------------------------------------------------------------------- */
4033
4034
6122
Solver::Solver(Options* opts)
4035
{
4036
6121
  d_nodeMgr.reset(new NodeManager());
4037
6122
  d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), opts));
4038
6120
  d_smtEngine->setSolver(this);
4039
6120
  Options& o = d_smtEngine->getOptions();
4040
21237
  d_rng.reset(new Random(o[options::seed]));
4041
#if CVC4_STATISTICS_ON
4042
6120
  d_stats.reset(new Statistics());
4043
6120
  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
4044
6120
  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_vars);
4045
6120
  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_terms);
4046
#endif
4047
6120
}
4048
4049
6099
Solver::~Solver() {}
4050
4051
/* Helpers and private functions                                              */
4052
/* -------------------------------------------------------------------------- */
4053
4054
68584931
NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
4055
4056
3263366
void Solver::increment_term_stats(Kind kind) const
4057
{
4058
#ifdef CVC4_STATISTICS_ON
4059
3263366
  d_stats->d_terms << kind;
4060
#endif
4061
3263366
}
4062
4063
229717
void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const
4064
{
4065
#ifdef CVC4_STATISTICS_ON
4066
459434
  const TypeNode tn = sort.getTypeNode();
4067
229717
  TypeConstant tc = tn.getKind() == CVC4::kind::TYPE_CONSTANT
4068
229717
                        ? tn.getConst<TypeConstant>()
4069
229717
                        : LAST_TYPE;
4070
229717
  if (is_var)
4071
  {
4072
59338
    d_stats->d_vars << tc;
4073
  }
4074
  else
4075
  {
4076
170379
    d_stats->d_consts << tc;
4077
  }
4078
#endif
4079
229717
}
4080
4081
/* Split out to avoid nested API calls (problematic with API tracing).        */
4082
/* .......................................................................... */
4083
4084
template <typename T>
4085
595764
Term Solver::mkValHelper(T t) const
4086
{
4087
  //////// all checks before this line
4088
1191528
  Node res = getNodeManager()->mkConst(t);
4089
595764
  (void)res.getType(true); /* kick off type checking */
4090
1191526
  return Term(this, res);
4091
}
4092
4093
376127
Term Solver::mkRealFromStrHelper(const std::string& s) const
4094
{
4095
  //////// all checks before this line
4096
  try
4097
  {
4098
376127
    CVC4::Rational r = s.find('/') != std::string::npos
4099
                           ? CVC4::Rational(s)
4100
752230
                           : CVC4::Rational::fromDecimal(s);
4101
752206
    return mkValHelper<CVC4::Rational>(r);
4102
  }
4103
48
  catch (const std::invalid_argument& e)
4104
  {
4105
    /* Catch to throw with a more meaningful error message. To be caught in
4106
     * enclosing CVC4_API_TRY_CATCH_* block to throw CVC4ApiException. */
4107
48
    std::stringstream message;
4108
24
    message << "Cannot construct Real or Int from string argument '" << s << "'"
4109
24
            << std::endl;
4110
24
    throw std::invalid_argument(message.str());
4111
  }
4112
}
4113
4114
25
Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
4115
{
4116
25
  CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
4117
  //////// all checks before this line
4118
21
  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
4119
}
4120
4121
5751
Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const
4122
{
4123
5751
  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
4124
5751
  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base)
4125
2
      << "base 2, 10, or 16";
4126
  //////// all checks before this line
4127
5747
  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
4128
}
4129
4130
93716
Term Solver::mkBVFromStrHelper(uint32_t size,
4131
                               const std::string& s,
4132
                               uint32_t base) const
4133
{
4134
93716
  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
4135
93716
  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base)
4136
      << "base 2, 10, or 16";
4137
  //////// all checks before this line
4138
4139
187432
  Integer val(s, base);
4140
4141
93716
  if (val.strictlyNegative())
4142
  {
4143
8
    CVC4_API_CHECK(val >= -Integer("2", 10).pow(size - 1))
4144
2
        << "Overflow in bitvector construction (specified bitvector size "
4145
2
        << size << " too small to hold value " << s << ")";
4146
  }
4147
  else
4148
  {
4149
93712
    CVC4_API_CHECK(val.modByPow2(size) == val)
4150
2
        << "Overflow in bitvector construction (specified bitvector size "
4151
2
        << size << " too small to hold value " << s << ")";
4152
  }
4153
4154
187424
  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
4155
}
4156
4157
22
Term Solver::mkCharFromStrHelper(const std::string& s) const
4158
{
4159
28
  CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
4160
                     == std::string::npos
4161
                 && s.size() <= 5 && s.size() > 0)
4162
6
      << "Unexpected string for hexadecimal character " << s;
4163
16
  uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
4164
16
  CVC4_API_CHECK(val < String::num_codes())
4165
      << "Not a valid code point for hexadecimal character " << s;
4166
  //////// all checks before this line
4167
32
  std::vector<unsigned> cpts;
4168
16
  cpts.push_back(val);
4169
32
  return mkValHelper<CVC4::String>(CVC4::String(cpts));
4170
}
4171
4172
119
Term Solver::getValueHelper(const Term& term) const
4173
{
4174
  // Note: Term is checked in the caller to avoid double checks
4175
  //////// all checks before this line
4176
232
  Node value = d_smtEngine->getValue(*term.d_node);
4177
226
  Term res = Term(this, value);
4178
  // May need to wrap in real cast so that user know this is a real.
4179
226
  TypeNode tn = (*term.d_node).getType();
4180
113
  if (!tn.isInteger() && value.getType().isInteger())
4181
  {
4182
12
    return ensureRealSort(res);
4183
  }
4184
101
  return res;
4185
}
4186
4187
3691
Sort Solver::mkTupleSortHelper(const std::vector<Sort>& sorts) const
4188
{
4189
  // Note: Sorts are checked in the caller to avoid double checks
4190
  //////// all checks before this line
4191
7382
  std::vector<TypeNode> typeNodes = Sort::sortVectorToTypeNodes(sorts);
4192
7382
  return Sort(this, getNodeManager()->mkTupleType(typeNodes));
4193
}
4194
4195
1429
Term Solver::mkTermFromKind(Kind kind) const
4196
{
4197
1433
  CVC4_API_KIND_CHECK_EXPECTED(
4198
      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
4199
4
      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
4200
  //////// all checks before this line
4201
2854
  Node res;
4202
1427
  if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
4203
  {
4204
4
    CVC4::Kind k = extToIntKind(kind);
4205
4
    Assert(isDefinedIntKind(k));
4206
4
    res = d_nodeMgr->mkNode(k, std::vector<Node>());
4207
  }
4208
  else
4209
  {
4210
1423
    Assert(kind == PI);
4211
1423
    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
4212
  }
4213
1427
  (void)res.getType(true); /* kick off type checking */
4214
1427
  increment_term_stats(kind);
4215
2854
  return Term(this, res);
4216
}
4217
4218
3261963
Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
4219
{
4220
  // Note: Kind and children are checked in the caller to avoid double checks
4221
  //////// all checks before this line
4222
4223
6523926
  std::vector<Node> echildren = Term::termVectorToNodes(children);
4224
3261963
  CVC4::Kind k = extToIntKind(kind);
4225
6523926
  Node res;
4226
3261963
  if (echildren.size() > 2)
4227
  {
4228
624621
    if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
4229
624123
        || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF)
4230
    {
4231
      // left-associative, but CVC4 internally only supports 2 args
4232
724
      res = d_nodeMgr->mkLeftAssociative(k, echildren);
4233
    }
4234
623897
    else if (kind == IMPLIES)
4235
    {
4236
      // right-associative, but CVC4 internally only supports 2 args
4237
      res = d_nodeMgr->mkRightAssociative(k, echildren);
4238
    }
4239
623897
    else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ
4240
623183
             || kind == GEQ)
4241
    {
4242
      // "chainable", but CVC4 internally only supports 2 args
4243
721
      res = d_nodeMgr->mkChain(k, echildren);
4244
    }
4245
623176
    else if (kind::isAssociative(k))
4246
    {
4247
      // mkAssociative has special treatment for associative operators with lots
4248
      // of children
4249
171889
      res = d_nodeMgr->mkAssociative(k, echildren);
4250
    }
4251
    else
4252
    {
4253
      // default case, must check kind
4254
451287
      checkMkTerm(kind, children.size());
4255
451287
      res = d_nodeMgr->mkNode(k, echildren);
4256
    }
4257
  }
4258
2637342
  else if (kind::isAssociative(k))
4259
  {
4260
    // associative case, same as above
4261
828555
    res = d_nodeMgr->mkAssociative(k, echildren);
4262
  }
4263
  else
4264
  {
4265
    // default case, same as above
4266
1808787
    checkMkTerm(kind, children.size());
4267
1808779
    if (kind == api::SINGLETON)
4268
    {
4269
      // the type of the term is the same as the type of the internal node
4270
      // see Term::getSort()
4271
864
      TypeNode type = children[0].d_node->getType();
4272
      // Internally NodeManager::mkSingleton needs a type argument
4273
      // to construct a singleton, since there is no difference between
4274
      // integers and reals (both are Rationals).
4275
      // At the API, mkReal and mkInteger are different and therefore the
4276
      // element type can be used safely here.
4277
432
      res = getNodeManager()->mkSingleton(type, *children[0].d_node);
4278
    }
4279
1808347
    else if (kind == api::MK_BAG)
4280
    {
4281
      // the type of the term is the same as the type of the internal node
4282
      // see Term::getSort()
4283
66
      TypeNode type = children[0].d_node->getType();
4284
      // Internally NodeManager::mkBag needs a type argument
4285
      // to construct a bag, since there is no difference between
4286
      // integers and reals (both are Rationals).
4287
      // At the API, mkReal and mkInteger are different and therefore the
4288
      // element type can be used safely here.
4289
99
      res = getNodeManager()->mkBag(
4290
66
          type, *children[0].d_node, *children[1].d_node);
4291
    }
4292
    else
4293
    {
4294
1808314
      res = d_nodeMgr->mkNode(k, echildren);
4295
    }
4296
  }
4297
4298
3261939
  (void)res.getType(true); /* kick off type checking */
4299
3261939
  increment_term_stats(kind);
4300
6523878
  return Term(this, res);
4301
}
4302
4303
82403
Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const
4304
{
4305
  // Note: Op and children are checked in the caller to avoid double checks
4306
82403
  checkMkTerm(op.d_kind, children.size());
4307
  //////// all checks before this line
4308
4309
82393
  if (!op.isIndexedHelper())
4310
  {
4311
4
    return mkTermHelper(op.d_kind, children);
4312
  }
4313
4314
82389
  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4315
164778
  std::vector<Node> echildren = Term::termVectorToNodes(children);
4316
4317
164778
  NodeBuilder<> nb(int_kind);
4318
82389
  nb << *op.d_node;
4319
82389
  nb.append(echildren);
4320
164771
  Node res = nb.constructNode();
4321
4322
82382
  (void)res.getType(true); /* kick off type checking */
4323
82382
  return Term(this, res);
4324
}
4325
4326
903
std::vector<Sort> Solver::mkDatatypeSortsInternal(
4327
    const std::vector<DatatypeDecl>& dtypedecls,
4328
    const std::set<Sort>& unresolvedSorts) const
4329
{
4330
  // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
4331
  //       double checks
4332
  //////// all checks before this line
4333
4334
1806
  std::vector<CVC4::DType> datatypes;
4335
2090
  for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
4336
  {
4337
1187
    datatypes.push_back(dtypedecls[i].getDatatype());
4338
  }
4339
4340
1806
  std::set<TypeNode> utypes = Sort::sortSetToTypeNodes(unresolvedSorts);
4341
  std::vector<CVC4::TypeNode> dtypes =
4342
1806
      getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
4343
903
  std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes);
4344
1806
  return retTypes;
4345
}
4346
4347
569
Term Solver::synthFunHelper(const std::string& symbol,
4348
                            const std::vector<Term>& boundVars,
4349
                            const Sort& sort,
4350
                            bool isInv,
4351
                            Grammar* grammar) const
4352
{
4353
  // Note: boundVars, sort and grammar are checked in the caller to avoid
4354
  //       double checks.
4355
1138
  std::vector<TypeNode> varTypes;
4356
1830
  for (const auto& bv : boundVars)
4357
  {
4358
1265
    if (grammar)
4359
    {
4360
924
      CVC4_API_CHECK(grammar->d_ntSyms[0].d_node->getType() == *sort.d_type)
4361
4
          << "Invalid Start symbol for grammar, Expected Start's sort to be "
4362
4
          << *sort.d_type << " but found "
4363
464
          << grammar->d_ntSyms[0].d_node->getType();
4364
    }
4365
1261
    varTypes.push_back(bv.d_node->getType());
4366
  }
4367
  //////// all checks before this line
4368
4369
624
  TypeNode funType = varTypes.empty() ? *sort.d_type
4370
                                      : getNodeManager()->mkFunctionType(
4371
1189
                                          varTypes, *sort.d_type);
4372
4373
1130
  Node fun = getNodeManager()->mkBoundVar(symbol, funType);
4374
565
  (void)fun.getType(true); /* kick off type checking */
4375
4376
1130
  std::vector<Node> bvns = Term::termVectorToNodes(boundVars);
4377
4378
845
  d_smtEngine->declareSynthFun(
4379
      fun,
4380
845
      grammar == nullptr ? funType : *grammar->resolve().d_type,
4381
      isInv,
4382
      bvns);
4383
4384
1130
  return Term(this, fun);
4385
}
4386
4387
22344
Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
4388
{
4389
  // Note: Term and sort are checked in the caller to avoid double checks
4390
22348
  CVC4_API_CHECK(term.getSort() == sort
4391
                 || (term.getSort().isInteger() && sort.isReal()))
4392
4
      << "Expected conversion from Int to Real";
4393
  //////// all checks before this line
4394
4395
44680
  Sort t = term.getSort();
4396
22340
  if (term.getSort() == sort)
4397
  {
4398
22338
    return term;
4399
  }
4400
4401
  // Integers are reals, too
4402
2
  Assert(t.isReal());
4403
4
  Term res = term;
4404
2
  if (t.isInteger())
4405
  {
4406
    // Must cast to Real to ensure correct type is passed to parametric type
4407
    // constructors. We do this cast using division with 1. This has the
4408
    // advantage wrt using TO_REAL since (constant) division is always included
4409
    // in the theory.
4410
2
    res = Term(this,
4411
8
               d_nodeMgr->mkNode(extToIntKind(DIVISION),
4412
2
                                 *res.d_node,
4413
4
                                 d_nodeMgr->mkConst(CVC4::Rational(1))));
4414
  }
4415
2
  Assert(res.getSort() == sort);
4416
2
  return res;
4417
}
4418
4419
22458
Term Solver::ensureRealSort(const Term& t) const
4420
{
4421
22458
  Assert(this == t.d_solver);
4422
22458
  CVC4_API_ARG_CHECK_EXPECTED(
4423
      t.getSort() == getIntegerSort() || t.getSort() == getRealSort(),
4424
      " an integer or real term");
4425
  // Note: Term is checked in the caller to avoid double checks
4426
  //////// all checks before this line
4427
22458
  if (t.getSort() == getIntegerSort())
4428
  {
4429
44126
    Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node);
4430
22063
    return Term(this, n);
4431
  }
4432
395
  return t;
4433
}
4434
4435
353782
bool Solver::isValidInteger(const std::string& s) const
4436
{
4437
  //////// all checks before this line
4438
353782
  if (s.length() == 0)
4439
  {
4440
    // string should not be empty
4441
6
    return false;
4442
  }
4443
4444
353776
  size_t index = 0;
4445
353776
  if (s[index] == '-')
4446
  {
4447
27
    if (s.length() == 1)
4448
    {
4449
      // negative integers should contain at least one digit
4450
2
      return false;
4451
    }
4452
25
    index = 1;
4453
  }
4454
4455
353774
  if (s[index] == '0' && s.length() > (index + 1))
4456
  {
4457
    // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
4458
    // digits not starting with 0. So integers like 001, 000 are not allowed
4459
12
    return false;
4460
  }
4461
4462
  // all remaining characters should be decimal digits
4463
1172550
  for (; index < s.length(); ++index)
4464
  {
4465
409440
    if (!std::isdigit(s[index]))
4466
    {
4467
46
      return false;
4468
    }
4469
  }
4470
4471
353716
  return true;
4472
}
4473
4474
/* Helpers for mkTerm checks.                                                 */
4475
/* .......................................................................... */
4476
4477
2342481
void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
4478
{
4479
2342481
  CVC4_API_KIND_CHECK(kind);
4480
2342481
  Assert(isDefinedIntKind(extToIntKind(kind)));
4481
2342481
  const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind));
4482
2342481
  CVC4_API_KIND_CHECK_EXPECTED(
4483
      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
4484
      kind)
4485
      << "Only operator-style terms are created with mkTerm(), "
4486
         "to create variables, constants and values see mkVar(), mkConst() "
4487
         "and the respective theory-specific functions to create values, "
4488
         "e.g., mkBitVector().";
4489
4685028
  CVC4_API_KIND_CHECK_EXPECTED(
4490
      nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
4491
2342547
      << "Terms with kind " << kindToString(kind) << " must have at least "
4492
22
      << minArity(kind) << " children and at most " << maxArity(kind)
4493
22
      << " children (the one under construction has " << nchildren << ")";
4494
2342459
}
4495
4496
/* Solver Configuration                                                       */
4497
/* -------------------------------------------------------------------------- */
4498
4499
8
bool Solver::supportsFloatingPoint() const
4500
{
4501
  CVC4_API_TRY_CATCH_BEGIN;
4502
  //////// all checks before this line
4503
8
  return Configuration::isBuiltWithSymFPU();
4504
  ////////
4505
  CVC4_API_TRY_CATCH_END;
4506
}
4507
4508
/* Sorts Handling                                                             */
4509
/* -------------------------------------------------------------------------- */
4510
4511
2730
Sort Solver::getNullSort(void) const
4512
{
4513
5460
  NodeManagerScope scope(getNodeManager());
4514
  CVC4_API_TRY_CATCH_BEGIN;
4515
  //////// all checks before this line
4516
5460
  return Sort(this, TypeNode());
4517
  ////////
4518
  CVC4_API_TRY_CATCH_END;
4519
}
4520
4521
14697
Sort Solver::getBooleanSort(void) const
4522
{
4523
29394
  NodeManagerScope scope(getNodeManager());
4524
  CVC4_API_TRY_CATCH_BEGIN;
4525
  //////// all checks before this line
4526
29394
  return Sort(this, getNodeManager()->booleanType());
4527
  ////////
4528
  CVC4_API_TRY_CATCH_END;
4529
}
4530
4531
404806
Sort Solver::getIntegerSort(void) const
4532
{
4533
809612
  NodeManagerScope scope(getNodeManager());
4534
  CVC4_API_TRY_CATCH_BEGIN;
4535
  //////// all checks before this line
4536
809612
  return Sort(this, getNodeManager()->integerType());
4537
  ////////
4538
  CVC4_API_TRY_CATCH_END;
4539
}
4540
4541
24849
Sort Solver::getRealSort(void) const
4542
{
4543
49698
  NodeManagerScope scope(getNodeManager());
4544
  CVC4_API_TRY_CATCH_BEGIN;
4545
  //////// all checks before this line
4546
49698
  return Sort(this, getNodeManager()->realType());
4547
  ////////
4548
  CVC4_API_TRY_CATCH_END;
4549
}
4550
4551
1728
Sort Solver::getRegExpSort(void) const
4552
{
4553
3456
  NodeManagerScope scope(getNodeManager());
4554
  CVC4_API_TRY_CATCH_BEGIN;
4555
  //////// all checks before this line
4556
3456
  return Sort(this, getNodeManager()->regExpType());
4557
  ////////
4558
  CVC4_API_TRY_CATCH_END;
4559
}
4560
4561
1756
Sort Solver::getStringSort(void) const
4562
{
4563
3512
  NodeManagerScope scope(getNodeManager());
4564
  CVC4_API_TRY_CATCH_BEGIN;
4565
  //////// all checks before this line
4566
3512
  return Sort(this, getNodeManager()->stringType());
4567
  ////////
4568
  CVC4_API_TRY_CATCH_END;
4569
}
4570
4571
1364
Sort Solver::getRoundingModeSort(void) const
4572
{
4573
2728
  NodeManagerScope scope(getNodeManager());
4574
  CVC4_API_TRY_CATCH_BEGIN;
4575
1364
  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
4576
      << "Expected CVC4 to be compiled with SymFPU support";
4577
  //////// all checks before this line
4578
2728
  return Sort(this, getNodeManager()->roundingModeType());
4579
  ////////
4580
  CVC4_API_TRY_CATCH_END;
4581
}
4582
4583
/* Create sorts ------------------------------------------------------- */
4584
4585
2217
Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const
4586
{
4587
4434
  NodeManagerScope scope(getNodeManager());
4588
  CVC4_API_TRY_CATCH_BEGIN;
4589
2217
  CVC4_API_SOLVER_CHECK_SORT(indexSort);
4590
2215
  CVC4_API_SOLVER_CHECK_SORT(elemSort);
4591
  //////// all checks before this line
4592
  return Sort(
4593
4430
      this, getNodeManager()->mkArrayType(*indexSort.d_type, *elemSort.d_type));
4594
  ////////
4595
  CVC4_API_TRY_CATCH_END;
4596
}
4597
4598
16334
Sort Solver::mkBitVectorSort(uint32_t size) const
4599
{
4600
32668
  NodeManagerScope scope(getNodeManager());
4601
  CVC4_API_TRY_CATCH_BEGIN;
4602
16334
  CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
4603
  //////// all checks before this line
4604
32664
  return Sort(this, getNodeManager()->mkBitVectorType(size));
4605
  ////////
4606
  CVC4_API_TRY_CATCH_END;
4607
}
4608
4609
5594
Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
4610
{
4611
11188
  NodeManagerScope scope(getNodeManager());
4612