1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of inference enumeration. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/inference_id.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
#include "util/rational.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
namespace theory { |
23 |
|
|
24 |
|
const char* toString(InferenceId i) |
25 |
|
{ |
26 |
|
switch (i) |
27 |
|
{ |
28 |
|
case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE"; |
29 |
|
case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT"; |
30 |
|
case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX"; |
31 |
|
case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ"; |
32 |
|
case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER"; |
33 |
|
case InferenceId::ARITH_CONF_TRICHOTOMY: return "ARITH_CONF_TRICHOTOMY"; |
34 |
|
case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER"; |
35 |
|
case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX"; |
36 |
|
case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX"; |
37 |
|
case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ"; |
38 |
|
case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL"; |
39 |
|
case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR"; |
40 |
|
case InferenceId::ARITH_APPROX_CUT: return "ARITH_APPROX_CUT"; |
41 |
|
case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA"; |
42 |
|
case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT"; |
43 |
|
case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION"; |
44 |
|
case InferenceId::ARITH_UNATE: return "ARITH_UNATE"; |
45 |
|
case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL"; |
46 |
|
case InferenceId::ARITH_SPLIT_FOR_NL_MODEL: |
47 |
|
return "ARITH_SPLIT_FOR_NL_MODEL"; |
48 |
|
case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; |
49 |
|
case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA: |
50 |
|
return "ARITH_PP_ELIM_OPERATORS_LEMMA"; |
51 |
|
case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE"; |
52 |
|
case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: |
53 |
|
return "ARITH_NL_SHARED_TERM_VALUE_SPLIT"; |
54 |
|
case InferenceId::ARITH_NL_CM_QUADRATIC_EQ: |
55 |
|
return "ARITH_NL_CM_QUADRATIC_EQ"; |
56 |
|
case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO"; |
57 |
|
case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN"; |
58 |
|
case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON"; |
59 |
|
case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS"; |
60 |
|
case InferenceId::ARITH_NL_INFER_BOUNDS_NT: |
61 |
|
return "ARITH_NL_INFER_BOUNDS_NT"; |
62 |
|
case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR"; |
63 |
|
case InferenceId::ARITH_NL_RES_INFER_BOUNDS: |
64 |
|
return "ARITH_NL_RES_INFER_BOUNDS"; |
65 |
|
case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE"; |
66 |
|
case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG"; |
67 |
|
case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE"; |
68 |
|
case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND"; |
69 |
|
case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY"; |
70 |
|
case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT"; |
71 |
|
case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT"; |
72 |
|
case InferenceId::ARITH_NL_IAND_INIT_REFINE: |
73 |
|
return "ARITH_NL_IAND_INIT_REFINE"; |
74 |
|
case InferenceId::ARITH_NL_IAND_VALUE_REFINE: |
75 |
|
return "ARITH_NL_IAND_VALUE_REFINE"; |
76 |
|
case InferenceId::ARITH_NL_IAND_SUM_REFINE: |
77 |
|
return "ARITH_NL_IAND_SUM_REFINE"; |
78 |
|
case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: |
79 |
|
return "ARITH_NL_IAND_BITWISE_REFINE"; |
80 |
|
case InferenceId::ARITH_NL_POW2_INIT_REFINE: |
81 |
|
return "ARITH_NL_POW2_INIT_REFINE"; |
82 |
|
case InferenceId::ARITH_NL_POW2_VALUE_REFINE: |
83 |
|
return "ARITH_NL_POW2_VALUE_REFINE"; |
84 |
|
case InferenceId::ARITH_NL_POW2_MONOTONE_REFINE: |
85 |
|
return "ARITH_NL_POW2_MONOTONE_REFINE"; |
86 |
|
case InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE: |
87 |
|
return "ARITH_NL_POW2_TRIVIAL_CASE_REFINE"; |
88 |
|
case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; |
89 |
|
case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: |
90 |
|
return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; |
91 |
|
case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT"; |
92 |
|
case InferenceId::ARITH_NL_ICP_PROPAGATION: |
93 |
|
return "ARITH_NL_ICP_PROPAGATION"; |
94 |
|
|
95 |
|
case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT"; |
96 |
|
case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; |
97 |
|
case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; |
98 |
|
case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA"; |
99 |
|
|
100 |
|
case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT"; |
101 |
|
case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT"; |
102 |
|
case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG"; |
103 |
|
case InferenceId::BAG_EQUALITY: return "BAG_EQUALITY"; |
104 |
|
case InferenceId::BAG_DISEQUALITY: return "BAG_DISEQUALITY"; |
105 |
|
case InferenceId::BAG_EMPTY: return "BAG_EMPTY"; |
106 |
|
case InferenceId::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT"; |
107 |
|
case InferenceId::BAG_UNION_MAX: return "BAG_UNION_MAX"; |
108 |
|
case InferenceId::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN"; |
109 |
|
case InferenceId::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT"; |
110 |
|
case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE"; |
111 |
|
case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL"; |
112 |
|
|
113 |
|
case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; |
114 |
|
case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: |
115 |
|
return "BV_BITBLAST_EAGER_LEMMA"; |
116 |
|
case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA: |
117 |
|
return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA"; |
118 |
|
case InferenceId::BV_LAYERED_CONFLICT: return "BV_LAYERED_CONFLICT"; |
119 |
|
case InferenceId::BV_LAYERED_LEMMA: return "BV_LAYERED_LEMMA"; |
120 |
|
case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA"; |
121 |
|
case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE"; |
122 |
|
|
123 |
|
case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY"; |
124 |
|
case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF"; |
125 |
|
case InferenceId::DATATYPES_INST: return "DATATYPES_INST"; |
126 |
|
case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT"; |
127 |
|
case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT"; |
128 |
|
case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH"; |
129 |
|
case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL"; |
130 |
|
case InferenceId::DATATYPES_CLASH_CONFLICT: |
131 |
|
return "DATATYPES_CLASH_CONFLICT"; |
132 |
|
case InferenceId::DATATYPES_TESTER_CONFLICT: |
133 |
|
return "DATATYPES_TESTER_CONFLICT"; |
134 |
|
case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT: |
135 |
|
return "DATATYPES_TESTER_MERGE_CONFLICT"; |
136 |
|
case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR"; |
137 |
|
case InferenceId::DATATYPES_REC_SINGLETON_EQ: |
138 |
|
return "DATATYPES_REC_SINGLETON_EQ"; |
139 |
|
case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ: |
140 |
|
return "DATATYPES_REC_SINGLETON_FORCE_DEQ"; |
141 |
|
case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE"; |
142 |
|
case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS"; |
143 |
|
case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO"; |
144 |
|
case InferenceId::DATATYPES_SYGUS_SYM_BREAK: |
145 |
|
return "DATATYPES_SYGUS_SYM_BREAK"; |
146 |
|
case InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK: |
147 |
|
return "DATATYPES_SYGUS_CDEP_SYM_BREAK"; |
148 |
|
case InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK: |
149 |
|
return "DATATYPES_SYGUS_ENUM_SYM_BREAK"; |
150 |
|
case InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK: |
151 |
|
return "DATATYPES_SYGUS_SIMPLE_SYM_BREAK"; |
152 |
|
case InferenceId::DATATYPES_SYGUS_FAIR_SIZE: |
153 |
|
return "DATATYPES_SYGUS_FAIR_SIZE"; |
154 |
|
case InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT: |
155 |
|
return "DATATYPES_SYGUS_FAIR_SIZE_CONFLICT"; |
156 |
|
case InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC: |
157 |
|
return "DATATYPES_SYGUS_VAR_AGNOSTIC"; |
158 |
|
case InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION: |
159 |
|
return "DATATYPES_SYGUS_SIZE_CORRECTION"; |
160 |
|
case InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION: |
161 |
|
return "DATATYPES_SYGUS_VALUE_CORRECTION"; |
162 |
|
case InferenceId::DATATYPES_SYGUS_MT_BOUND: |
163 |
|
return "DATATYPES_SYGUS_MT_BOUND"; |
164 |
|
case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS"; |
165 |
|
|
166 |
|
case InferenceId::FP_PREPROCESS: return "FP_PREPROCESS"; |
167 |
|
case InferenceId::FP_EQUATE_TERM: return "FP_EQUATE_TERM"; |
168 |
|
case InferenceId::FP_REGISTER_TERM: return "FP_REGISTER_TERM"; |
169 |
|
|
170 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING: |
171 |
|
return "QUANTIFIERS_INST_E_MATCHING"; |
172 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE: |
173 |
|
return "QUANTIFIERS_INST_E_MATCHING_SIMPLE"; |
174 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT: |
175 |
|
return "QUANTIFIERS_INST_E_MATCHING_MT"; |
176 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL: |
177 |
|
return "QUANTIFIERS_INST_E_MATCHING_MTL"; |
178 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO: |
179 |
|
return "QUANTIFIERS_INST_E_MATCHING_HO"; |
180 |
|
case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN: |
181 |
|
return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN"; |
182 |
|
case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT: |
183 |
|
return "QUANTIFIERS_INST_CBQI_CONFLICT"; |
184 |
|
case InferenceId::QUANTIFIERS_INST_CBQI_PROP: |
185 |
|
return "QUANTIFIERS_INST_CBQI_PROP"; |
186 |
|
case InferenceId::QUANTIFIERS_INST_FMF_EXH: |
187 |
|
return "QUANTIFIERS_INST_FMF_EXH"; |
188 |
|
case InferenceId::QUANTIFIERS_INST_FMF_FMC: |
189 |
|
return "QUANTIFIERS_INST_FMF_FMC"; |
190 |
|
case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH: |
191 |
|
return "QUANTIFIERS_INST_FMF_FMC_EXH"; |
192 |
|
case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI"; |
193 |
|
case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI"; |
194 |
|
case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM"; |
195 |
|
case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL"; |
196 |
|
case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; |
197 |
|
case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG"; |
198 |
|
case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX"; |
199 |
|
case InferenceId::QUANTIFIERS_CEGQI_CEX_AUX: |
200 |
|
return "QUANTIFIERS_CEGQI_CEX_AUX"; |
201 |
|
case InferenceId::QUANTIFIERS_CEGQI_NESTED_QE: |
202 |
|
return "QUANTIFIERS_CEGQI_NESTED_QE"; |
203 |
|
case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP: |
204 |
|
return "QUANTIFIERS_CEGQI_CEX_DEP"; |
205 |
|
case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA: |
206 |
|
return "QUANTIFIERS_CEGQI_VTS_LB_DELTA"; |
207 |
|
case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA: |
208 |
|
return "QUANTIFIERS_CEGQI_VTS_UB_DELTA"; |
209 |
|
case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF: |
210 |
|
return "QUANTIFIERS_CEGQI_VTS_LB_INF"; |
211 |
|
case InferenceId::QUANTIFIERS_SYQI_CEX: return "QUANTIFIERS_SYQI_CEX"; |
212 |
|
case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD: |
213 |
|
return "QUANTIFIERS_SYQI_EVAL_UNFOLD"; |
214 |
|
case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC: |
215 |
|
return "QUANTIFIERS_SYGUS_QE_PREPROC"; |
216 |
|
case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT: |
217 |
|
return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT"; |
218 |
|
case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT: |
219 |
|
return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT"; |
220 |
|
case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT: |
221 |
|
return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT"; |
222 |
|
case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA: |
223 |
|
return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA"; |
224 |
|
case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT"; |
225 |
|
case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE"; |
226 |
|
case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ: |
227 |
|
return "QUANTIFIERS_REDUCE_ALPHA_EQ"; |
228 |
|
case InferenceId::QUANTIFIERS_HO_MATCH_PRED: |
229 |
|
return "QUANTIFIERS_HO_MATCH_PRED"; |
230 |
|
case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE: |
231 |
|
return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE"; |
232 |
|
|
233 |
|
case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; |
234 |
|
case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; |
235 |
|
case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO"; |
236 |
|
case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF"; |
237 |
|
case InferenceId::SEP_EMP: return "SEP_EMP"; |
238 |
|
case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION"; |
239 |
|
case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION"; |
240 |
|
case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT"; |
241 |
|
case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP"; |
242 |
|
case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK"; |
243 |
|
case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA"; |
244 |
|
case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; |
245 |
|
case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; |
246 |
|
|
247 |
|
case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT"; |
248 |
|
case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; |
249 |
|
case InferenceId::SETS_DEQ: return "SETS_DEQ"; |
250 |
|
case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE"; |
251 |
|
case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT"; |
252 |
|
case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM"; |
253 |
|
case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT"; |
254 |
|
case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ"; |
255 |
|
case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT"; |
256 |
|
case InferenceId::SETS_PROXY: return "SETS_PROXY"; |
257 |
|
case InferenceId::SETS_PROXY_SINGLETON: return "SETS_PROXY_SINGLETON"; |
258 |
|
case InferenceId::SETS_SINGLETON_EQ: return "SETS_SINGLETON_EQ"; |
259 |
|
case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE"; |
260 |
|
case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2"; |
261 |
|
case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV"; |
262 |
|
case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE"; |
263 |
|
case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY"; |
264 |
|
case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE"; |
265 |
|
case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL"; |
266 |
|
case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP"; |
267 |
|
case InferenceId::SETS_CARD_GRAPH_EMP_PARENT: |
268 |
|
return "SETS_CARD_GRAPH_EMP_PARENT"; |
269 |
|
case InferenceId::SETS_CARD_GRAPH_EQ_PARENT: |
270 |
|
return "SETS_CARD_GRAPH_EQ_PARENT"; |
271 |
|
case InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2: |
272 |
|
return "SETS_CARD_GRAPH_EQ_PARENT_2"; |
273 |
|
case InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON: |
274 |
|
return "SETS_CARD_GRAPH_PARENT_SINGLETON"; |
275 |
|
case InferenceId::SETS_CARD_MINIMAL: return "SETS_CARD_MINIMAL"; |
276 |
|
case InferenceId::SETS_CARD_NEGATIVE_MEMBER: |
277 |
|
return "SETS_CARD_NEGATIVE_MEMBER"; |
278 |
|
case InferenceId::SETS_CARD_POSITIVE: return "SETS_CARD_POSITIVE"; |
279 |
|
case InferenceId::SETS_CARD_UNIV_SUPERSET: return "SETS_CARD_UNIV_SUPERSET"; |
280 |
|
case InferenceId::SETS_CARD_UNIV_TYPE: return "SETS_CARD_UNIV_TYPE"; |
281 |
|
case InferenceId::SETS_RELS_IDENTITY_DOWN: return "SETS_RELS_IDENTITY_DOWN"; |
282 |
|
case InferenceId::SETS_RELS_IDENTITY_UP: return "SETS_RELS_IDENTITY_UP"; |
283 |
|
case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE"; |
284 |
|
case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN: |
285 |
|
return "SETS_RELS_JOIN_IMAGE_DOWN"; |
286 |
|
case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1"; |
287 |
|
case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2"; |
288 |
|
case InferenceId::SETS_RELS_PRODUCE_COMPOSE: |
289 |
|
return "SETS_RELS_PRODUCE_COMPOSE"; |
290 |
|
case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT"; |
291 |
|
case InferenceId::SETS_RELS_TCLOSURE_FWD: return "SETS_RELS_TCLOSURE_FWD"; |
292 |
|
case InferenceId::SETS_RELS_TCLOSURE_UP: return "SETS_RELS_TCLOSURE_UP"; |
293 |
|
case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ"; |
294 |
|
case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV"; |
295 |
|
case InferenceId::SETS_RELS_TUPLE_REDUCTION: |
296 |
|
return "SETS_RELS_TUPLE_REDUCTION"; |
297 |
|
|
298 |
|
case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S"; |
299 |
|
case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE"; |
300 |
|
case InferenceId::STRINGS_I_CONST_CONFLICT: |
301 |
|
return "STRINGS_I_CONST_CONFLICT"; |
302 |
|
case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM"; |
303 |
|
case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ"; |
304 |
|
case InferenceId::STRINGS_UNIT_CONST_CONFLICT: |
305 |
|
return "STRINGS_UNIT_CONST_CONFLICT"; |
306 |
|
case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ"; |
307 |
|
case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP"; |
308 |
|
case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY"; |
309 |
|
case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E"; |
310 |
|
case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE"; |
311 |
|
case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST"; |
312 |
|
case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY"; |
313 |
|
case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP"; |
314 |
|
case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ"; |
315 |
|
case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN"; |
316 |
|
case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF"; |
317 |
|
case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP"; |
318 |
|
case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY"; |
319 |
|
case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ"; |
320 |
|
case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST"; |
321 |
|
case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP"; |
322 |
|
case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP"; |
323 |
|
case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP"; |
324 |
|
case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT"; |
325 |
|
case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP"; |
326 |
|
case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST"; |
327 |
|
case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR"; |
328 |
|
case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP"; |
329 |
|
case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT"; |
330 |
|
case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM"; |
331 |
|
case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN"; |
332 |
|
case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM"; |
333 |
|
case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT: |
334 |
|
return "STRINGS_DEQ_DISL_EMP_SPLIT"; |
335 |
|
case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT: |
336 |
|
return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT"; |
337 |
|
case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT: |
338 |
|
return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT"; |
339 |
|
case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ"; |
340 |
|
case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT: |
341 |
|
return "STRINGS_DEQ_DISL_STRINGS_SPLIT"; |
342 |
|
case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ"; |
343 |
|
case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP"; |
344 |
|
case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP"; |
345 |
|
case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY"; |
346 |
|
case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ"; |
347 |
|
case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT"; |
348 |
|
case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS"; |
349 |
|
case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG"; |
350 |
|
case InferenceId::STRINGS_RE_INTER_INCLUDE: |
351 |
|
return "STRINGS_RE_INTER_INCLUDE"; |
352 |
|
case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF"; |
353 |
|
case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER"; |
354 |
|
case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA"; |
355 |
|
case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF"; |
356 |
|
case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE"; |
357 |
|
case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF"; |
358 |
|
case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N"; |
359 |
|
case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D"; |
360 |
|
case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N"; |
361 |
|
case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW"; |
362 |
|
case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS"; |
363 |
|
case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE"; |
364 |
|
case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL"; |
365 |
|
case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS"; |
366 |
|
case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION"; |
367 |
|
case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT"; |
368 |
|
case InferenceId::STRINGS_REGISTER_TERM_ATOMIC: |
369 |
|
return "STRINGS_REGISTER_TERM_ATOMIC"; |
370 |
|
case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM"; |
371 |
|
case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT"; |
372 |
|
|
373 |
|
case InferenceId::UF_BREAK_SYMMETRY: return "UF_BREAK_SYMMETRY"; |
374 |
|
case InferenceId::UF_CARD_CLIQUE: return "UF_CARD_CLIQUE"; |
375 |
|
case InferenceId::UF_CARD_COMBINED: return "UF_CARD_COMBINED"; |
376 |
|
case InferenceId::UF_CARD_ENFORCE_NEGATIVE: return "UF_CARD_ENFORCE_NEGATIVE"; |
377 |
|
case InferenceId::UF_CARD_EQUIV: return "UF_CARD_EQUIV"; |
378 |
|
case InferenceId::UF_CARD_MONOTONE_COMBINED: return "UF_CARD_MONOTONE_COMBINED"; |
379 |
|
case InferenceId::UF_CARD_SIMPLE_CONFLICT: return "UF_CARD_SIMPLE_CONFLICT"; |
380 |
|
case InferenceId::UF_CARD_SPLIT: return "UF_CARD_SPLIT"; |
381 |
|
|
382 |
|
case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE"; |
383 |
|
case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM"; |
384 |
|
case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY"; |
385 |
|
case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE"; |
386 |
|
case InferenceId::UF_HO_MODEL_EXTENSIONALITY: |
387 |
|
return "UF_HO_MODEL_EXTENSIONALITY"; |
388 |
|
|
389 |
|
default: return "?"; |
390 |
|
} |
391 |
|
} |
392 |
|
|
393 |
|
std::ostream& operator<<(std::ostream& out, InferenceId i) |
394 |
|
{ |
395 |
|
out << toString(i); |
396 |
|
return out; |
397 |
|
} |
398 |
|
|
399 |
8994 |
Node mkInferenceIdNode(InferenceId i) |
400 |
|
{ |
401 |
8994 |
return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i))); |
402 |
|
} |
403 |
|
|
404 |
|
} // namespace theory |
405 |
29280 |
} // namespace cvc5 |