GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/inference_id.cpp Lines: 1 290 0.3 %
Date: 2021-03-22 Branches: 2 223 0.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_id.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds
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 Implementation of inference enumeration.
13
 **/
14
15
#include "theory/inference_id.h"
16
17
#include <iostream>
18
19
namespace CVC4 {
20
namespace theory {
21
22
const char* toString(InferenceId i)
23
{
24
  switch (i)
25
  {
26
    case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
27
    case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA:
28
      return "ARITH_PP_ELIM_OPERATORS_LEMMA";
29
    case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
30
    case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
31
      return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
32
    case InferenceId::ARITH_NL_CM_QUADRATIC_EQ:
33
      return "ARITH_NL_CM_QUADRATIC_EQ";
34
    case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
35
    case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
36
    case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
37
    case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS";
38
    case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
39
      return "ARITH_NL_INFER_BOUNDS_NT";
40
    case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
41
    case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
42
      return "ARITH_NL_RES_INFER_BOUNDS";
43
    case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
44
    case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
45
    case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
46
    case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
47
    case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
48
    case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
49
    case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
50
    case InferenceId::ARITH_NL_IAND_INIT_REFINE:
51
      return "ARITH_NL_IAND_INIT_REFINE";
52
    case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
53
      return "ARITH_NL_IAND_VALUE_REFINE";
54
    case InferenceId::ARITH_NL_IAND_SUM_REFINE:
55
      return "ARITH_NL_IAND_SUM_REFINE";
56
    case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
57
      return "ARITH_NL_IAND_BITWISE_REFINE";
58
    case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
59
    case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
60
      return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
61
    case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
62
    case InferenceId::ARITH_NL_ICP_PROPAGATION:
63
      return "ARITH_NL_ICP_PROPAGATION";
64
65
    case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
66
    case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
67
    case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
68
    case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA";
69
70
    case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
71
    case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
72
    case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG";
73
    case InferenceId::BAG_EQUALITY: return "BAG_EQUALITY";
74
    case InferenceId::BAG_DISEQUALITY: return "BAG_DISEQUALITY";
75
    case InferenceId::BAG_EMPTY: return "BAG_EMPTY";
76
    case InferenceId::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT";
77
    case InferenceId::BAG_UNION_MAX: return "BAG_UNION_MAX";
78
    case InferenceId::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN";
79
    case InferenceId::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT";
80
    case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
81
    case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
82
83
    case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
84
    case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
85
    case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
86
    case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT";
87
    case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT";
88
    case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH";
89
    case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL";
90
    case InferenceId::DATATYPES_CLASH_CONFLICT:
91
      return "DATATYPES_CLASH_CONFLICT";
92
    case InferenceId::DATATYPES_TESTER_CONFLICT:
93
      return "DATATYPES_TESTER_CONFLICT";
94
    case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
95
      return "DATATYPES_TESTER_MERGE_CONFLICT";
96
    case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR";
97
    case InferenceId::DATATYPES_REC_SINGLETON_EQ:
98
      return "DATATYPES_REC_SINGLETON_EQ";
99
    case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ:
100
      return "DATATYPES_REC_SINGLETON_FORCE_DEQ";
101
    case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE";
102
    case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS";
103
    case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO";
104
    case InferenceId::DATATYPES_SYGUS_SYM_BREAK:
105
      return "DATATYPES_SYGUS_SYM_BREAK";
106
    case InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK:
107
      return "DATATYPES_SYGUS_CDEP_SYM_BREAK";
108
    case InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK:
109
      return "DATATYPES_SYGUS_ENUM_SYM_BREAK";
110
    case InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK:
111
      return "DATATYPES_SYGUS_SIMPLE_SYM_BREAK";
112
    case InferenceId::DATATYPES_SYGUS_FAIR_SIZE:
113
      return "DATATYPES_SYGUS_FAIR_SIZE";
114
    case InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT:
115
      return "DATATYPES_SYGUS_FAIR_SIZE_CONFLICT";
116
    case InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC:
117
      return "DATATYPES_SYGUS_VAR_AGNOSTIC";
118
    case InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION:
119
      return "DATATYPES_SYGUS_SIZE_CORRECTION";
120
    case InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION:
121
      return "DATATYPES_SYGUS_VALUE_CORRECTION";
122
    case InferenceId::DATATYPES_SYGUS_MT_BOUND:
123
      return "DATATYPES_SYGUS_MT_BOUND";
124
    case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
125
126
    case InferenceId::QUANTIFIERS_INST_E_MATCHING:
127
      return "QUANTIFIERS_INST_E_MATCHING";
128
    case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
129
      return "QUANTIFIERS_INST_E_MATCHING_SIMPLE";
130
    case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
131
      return "QUANTIFIERS_INST_E_MATCHING_MT";
132
    case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
133
      return "QUANTIFIERS_INST_E_MATCHING_MTL";
134
    case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
135
      return "QUANTIFIERS_INST_E_MATCHING_HO";
136
    case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
137
      return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
138
    case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
139
      return "QUANTIFIERS_INST_CBQI_CONFLICT";
140
    case InferenceId::QUANTIFIERS_INST_CBQI_PROP:
141
      return "QUANTIFIERS_INST_CBQI_PROP";
142
    case InferenceId::QUANTIFIERS_INST_FMF_EXH:
143
      return "QUANTIFIERS_INST_FMF_EXH";
144
    case InferenceId::QUANTIFIERS_INST_FMF_FMC:
145
      return "QUANTIFIERS_INST_FMF_FMC";
146
    case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH:
147
      return "QUANTIFIERS_INST_FMF_FMC_EXH";
148
    case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
149
    case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
150
    case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
151
    case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP:
152
      return "QUANTIFIERS_CEGQI_CEX_DEP";
153
    case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA:
154
      return "QUANTIFIERS_CEGQI_VTS_LB_DELTA";
155
    case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA:
156
      return "QUANTIFIERS_CEGQI_VTS_UB_DELTA";
157
    case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF:
158
      return "QUANTIFIERS_CEGQI_VTS_LB_INF";
159
    case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD:
160
      return "QUANTIFIERS_SYQI_EVAL_UNFOLD";
161
    case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC:
162
      return "QUANTIFIERS_SYGUS_QE_PREPROC";
163
    case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT:
164
      return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT";
165
    case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT:
166
      return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
167
    case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
168
      return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
169
    case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
170
      return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
171
    case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
172
    case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
173
      return "QUANTIFIERS_REDUCE_ALPHA_EQ";
174
175
    case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
176
    case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
177
    case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
178
    case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
179
    case InferenceId::SEP_EMP: return "SEP_EMP";
180
    case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
181
    case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
182
    case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";
183
    case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP";
184
    case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK";
185
    case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA";
186
    case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF";
187
    case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND";
188
189
    case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
190
    case InferenceId::SETS_DEQ: return "SETS_DEQ";
191
    case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE";
192
    case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
193
    case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
194
    case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";
195
    case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT";
196
    case InferenceId::SETS_PROXY: return "SETS_PROXY";
197
    case InferenceId::SETS_PROXY_SINGLETON: return "SETS_PROXY_SINGLETON";
198
    case InferenceId::SETS_SINGLETON_EQ: return "SETS_SINGLETON_EQ";
199
    case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE";
200
    case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2";
201
    case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV";
202
    case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE";
203
    case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE";
204
    case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL";
205
    case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP";
206
    case InferenceId::SETS_CARD_GRAPH_EMP_PARENT:
207
      return "SETS_CARD_GRAPH_EMP_PARENT";
208
    case InferenceId::SETS_CARD_GRAPH_EQ_PARENT:
209
      return "SETS_CARD_GRAPH_EQ_PARENT";
210
    case InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2:
211
      return "SETS_CARD_GRAPH_EQ_PARENT_2";
212
    case InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON:
213
      return "SETS_CARD_GRAPH_PARENT_SINGLETON";
214
    case InferenceId::SETS_CARD_MINIMAL: return "SETS_CARD_MINIMAL";
215
    case InferenceId::SETS_CARD_NEGATIVE_MEMBER:
216
      return "SETS_CARD_NEGATIVE_MEMBER";
217
    case InferenceId::SETS_CARD_POSITIVE: return "SETS_CARD_POSITIVE";
218
    case InferenceId::SETS_CARD_UNIV_SUPERSET: return "SETS_CARD_UNIV_SUPERSET";
219
    case InferenceId::SETS_CARD_UNIV_TYPE: return "SETS_CARD_UNIV_TYPE";
220
    case InferenceId::SETS_RELS_IDENTITY_DOWN: return "SETS_RELS_IDENTITY_DOWN";
221
    case InferenceId::SETS_RELS_IDENTITY_UP: return "SETS_RELS_IDENTITY_UP";
222
    case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE";
223
    case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN:
224
      return "SETS_RELS_JOIN_IMAGE_DOWN";
225
    case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
226
    case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
227
    case InferenceId::SETS_RELS_PRODUCE_COMPOSE:
228
      return "SETS_RELS_PRODUCE_COMPOSE";
229
    case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
230
    case InferenceId::SETS_RELS_TCLOSURE_FWD: return "SETS_RELS_TCLOSURE_FWD";
231
    case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ";
232
    case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV";
233
    case InferenceId::SETS_RELS_TUPLE_REDUCTION:
234
      return "SETS_RELS_TUPLE_REDUCTION";
235
236
    case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S";
237
    case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE";
238
    case InferenceId::STRINGS_I_CONST_CONFLICT:
239
      return "STRINGS_I_CONST_CONFLICT";
240
    case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM";
241
    case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ";
242
    case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
243
      return "STRINGS_UNIT_CONST_CONFLICT";
244
    case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ";
245
    case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP";
246
    case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY";
247
    case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E";
248
    case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE";
249
    case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST";
250
    case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY";
251
    case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP";
252
    case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ";
253
    case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN";
254
    case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF";
255
    case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP";
256
    case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY";
257
    case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ";
258
    case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST";
259
    case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP";
260
    case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP";
261
    case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP";
262
    case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT";
263
    case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP";
264
    case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST";
265
    case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR";
266
    case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP";
267
    case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT";
268
    case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM";
269
    case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN";
270
    case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM";
271
    case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
272
      return "STRINGS_DEQ_DISL_EMP_SPLIT";
273
    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
274
      return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
275
    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
276
      return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
277
    case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ";
278
    case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
279
      return "STRINGS_DEQ_DISL_STRINGS_SPLIT";
280
    case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
281
    case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
282
    case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
283
    case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY";
284
    case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
285
    case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
286
    case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS";
287
    case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG";
288
    case InferenceId::STRINGS_RE_INTER_INCLUDE:
289
      return "STRINGS_RE_INTER_INCLUDE";
290
    case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF";
291
    case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER";
292
    case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA";
293
    case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF";
294
    case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE";
295
    case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF";
296
    case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N";
297
    case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D";
298
    case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N";
299
    case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW";
300
    case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS";
301
    case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
302
    case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL";
303
    case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
304
    case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
305
    case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
306
    case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
307
      return "STRINGS_REGISTER_TERM_ATOMIC";
308
    case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
309
    case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
310
311
    case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
312
    case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
313
    case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
314
    case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
315
    case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
316
      return "UF_HO_MODEL_EXTENSIONALITY";
317
318
    default: return "?";
319
  }
320
}
321
322
std::ostream& operator<<(std::ostream& out, InferenceId i)
323
{
324
  out << toString(i);
325
  return out;
326
}
327
328
}  // namespace theory
329
26676
}  // namespace CVC4