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