1 |
11169956 |
static const std::vector<std::string> Trace_tags = { |
2 |
|
#if defined(CVC5_TRACING) |
3 |
|
"SolverState::collectBagsAndCountTerms", |
4 |
|
"aeq", |
5 |
|
"aeq-debug", |
6 |
|
"aeq-debug2", |
7 |
|
"ag-miniscope", |
8 |
|
"ag-miniscope-debug", |
9 |
|
"alethe-proof", |
10 |
|
"alpha-eq", |
11 |
|
"apply-substs", |
12 |
|
"arith-check", |
13 |
|
"arith-ee", |
14 |
|
"arith-eq-solver", |
15 |
|
"arith-eq-solver-debug", |
16 |
|
"arith-inf-manager", |
17 |
|
"arith-logic", |
18 |
|
"arith-pfee", |
19 |
|
"arith-rewrite", |
20 |
|
"arith-tf-rewrite", |
21 |
|
"arith-tf-rewrite-debug", |
22 |
|
"arith::forceNewBasis", |
23 |
|
"arith::infman", |
24 |
|
"arith::model", |
25 |
|
"arith::updateMany", |
26 |
|
"array-type-enum", |
27 |
|
"arrays", |
28 |
|
"arrays-addinstore", |
29 |
|
"arrays-cri", |
30 |
|
"arrays-crl", |
31 |
|
"arrays-ind", |
32 |
|
"arrays-infer", |
33 |
|
"arrays-info", |
34 |
|
"arrays-lem", |
35 |
|
"arrays-merge", |
36 |
|
"arrays-mergei", |
37 |
|
"arrays-models", |
38 |
|
"arrays-postrewrite", |
39 |
|
"arrays-prerewrite", |
40 |
|
"arrays::collectModelInfo", |
41 |
|
"arraysuf", |
42 |
|
"assert-pipeline", |
43 |
|
"assert-pipeline-debug", |
44 |
|
"assertions::post-ackermann", |
45 |
|
"assertions::post-apply-substs", |
46 |
|
"assertions::post-bool-to-bv", |
47 |
|
"assertions::post-bv-eager-atoms", |
48 |
|
"assertions::post-bv-gauss", |
49 |
|
"assertions::post-bv-to-bool", |
50 |
|
"assertions::post-bv-to-int", |
51 |
|
"assertions::post-everything", |
52 |
|
"assertions::post-ext-rew-pre", |
53 |
|
"assertions::post-foreign-theory-rewrite", |
54 |
|
"assertions::post-fun-def-fmf", |
55 |
|
"assertions::post-global-negate", |
56 |
|
"assertions::post-ho-elim", |
57 |
|
"assertions::post-int-to-bv", |
58 |
|
"assertions::post-ite-removal", |
59 |
|
"assertions::post-ite-simp", |
60 |
|
"assertions::post-learned-rewrite", |
61 |
|
"assertions::post-miplib-trick", |
62 |
|
"assertions::post-nl-ext-purify", |
63 |
|
"assertions::post-non-clausal-simp", |
64 |
|
"assertions::post-pseudo-boolean-processor", |
65 |
|
"assertions::post-quantifiers-preprocess", |
66 |
|
"assertions::post-real-to-int", |
67 |
|
"assertions::post-repeat-simplify", |
68 |
|
"assertions::post-rewrite", |
69 |
|
"assertions::post-sep-skolem-emp", |
70 |
|
"assertions::post-simplify", |
71 |
|
"assertions::post-sort-inference", |
72 |
|
"assertions::post-static-learning", |
73 |
|
"assertions::post-strings-eager-pp", |
74 |
|
"assertions::post-sygus-infer", |
75 |
|
"assertions::post-synth-rr", |
76 |
|
"assertions::post-theory-preprocess", |
77 |
|
"assertions::post-theory-rewrite-eq", |
78 |
|
"assertions::post-unconstrained-simplifier", |
79 |
|
"assertions::pre-ackermann", |
80 |
|
"assertions::pre-apply-substs", |
81 |
|
"assertions::pre-bool-to-bv", |
82 |
|
"assertions::pre-bv-eager-atoms", |
83 |
|
"assertions::pre-bv-gauss", |
84 |
|
"assertions::pre-bv-to-bool", |
85 |
|
"assertions::pre-bv-to-int", |
86 |
|
"assertions::pre-everything", |
87 |
|
"assertions::pre-ext-rew-pre", |
88 |
|
"assertions::pre-foreign-theory-rewrite", |
89 |
|
"assertions::pre-fun-def-fmf", |
90 |
|
"assertions::pre-global-negate", |
91 |
|
"assertions::pre-ho-elim", |
92 |
|
"assertions::pre-int-to-bv", |
93 |
|
"assertions::pre-ite-removal", |
94 |
|
"assertions::pre-ite-simp", |
95 |
|
"assertions::pre-learned-rewrite", |
96 |
|
"assertions::pre-miplib-trick", |
97 |
|
"assertions::pre-nl-ext-purify", |
98 |
|
"assertions::pre-non-clausal-simp", |
99 |
|
"assertions::pre-pseudo-boolean-processor", |
100 |
|
"assertions::pre-quantifiers-preprocess", |
101 |
|
"assertions::pre-real-to-int", |
102 |
|
"assertions::pre-repeat-simplify", |
103 |
|
"assertions::pre-rewrite", |
104 |
|
"assertions::pre-sep-skolem-emp", |
105 |
|
"assertions::pre-simplify", |
106 |
|
"assertions::pre-sort-inference", |
107 |
|
"assertions::pre-static-learning", |
108 |
|
"assertions::pre-strings-eager-pp", |
109 |
|
"assertions::pre-sygus-infer", |
110 |
|
"assertions::pre-synth-rr", |
111 |
|
"assertions::pre-theory-preprocess", |
112 |
|
"assertions::pre-theory-rewrite-eq", |
113 |
|
"assertions::pre-unconstrained-simplifier", |
114 |
|
"auto-gen-trigger", |
115 |
|
"auto-gen-trigger-debug", |
116 |
|
"auto-gen-trigger-debug2", |
117 |
|
"auto-gen-trigger-partial", |
118 |
|
"bag-type-enum", |
119 |
|
"bags-check", |
120 |
|
"bags-eqc", |
121 |
|
"bags-evaluate", |
122 |
|
"bags-model", |
123 |
|
"bags-rewrite", |
124 |
|
"bags::BagSolver::postCheck", |
125 |
|
"bags::InferInfo::process", |
126 |
|
"bags::TheoryBags::postCheck", |
127 |
|
"bags::TheoryBags::preRegisterTerm", |
128 |
|
"bint-engine", |
129 |
|
"bool-pfcheck", |
130 |
|
"bound-inf", |
131 |
|
"bound-int", |
132 |
|
"bound-int-debug", |
133 |
|
"bound-int-lemma", |
134 |
|
"bound-int-rsi", |
135 |
|
"bound-int-rsi-debug", |
136 |
|
"bound-int-var", |
137 |
|
"bound-int-warn", |
138 |
|
"builtin-pfcheck", |
139 |
|
"builtin-pfcheck-debug", |
140 |
|
"builtin-rewrite", |
141 |
|
"builtin-rewrite-debug", |
142 |
|
"builtin-rewrite-debug2", |
143 |
|
"bv-gauss-elim", |
144 |
|
"bv-invert", |
145 |
|
"bv-invert-debug", |
146 |
|
"bv-to-bool", |
147 |
|
"bv-to-int-debug", |
148 |
|
"cad::lazard", |
149 |
|
"canon-term-debug", |
150 |
|
"cdcac", |
151 |
|
"cdcac::projection", |
152 |
|
"cdproof", |
153 |
|
"cdproof-debug", |
154 |
|
"cegis", |
155 |
|
"cegis-rl", |
156 |
|
"cegis-sample", |
157 |
|
"cegis-sample-debug", |
158 |
|
"cegis-sample-debug2", |
159 |
|
"cegis-unif", |
160 |
|
"cegis-unif-enum", |
161 |
|
"cegis-unif-enum-debug", |
162 |
|
"cegis-unif-enum-lemma", |
163 |
|
"cegis-unif-lemma", |
164 |
|
"cegqi", |
165 |
|
"cegqi-arith-bound", |
166 |
|
"cegqi-arith-bound-inf", |
167 |
|
"cegqi-arith-bound2", |
168 |
|
"cegqi-arith-debug", |
169 |
|
"cegqi-arith-debug2", |
170 |
|
"cegqi-bound2", |
171 |
|
"cegqi-bv", |
172 |
|
"cegqi-bv-debug", |
173 |
|
"cegqi-bv-nl", |
174 |
|
"cegqi-bv-pp", |
175 |
|
"cegqi-bv-pp-debug2", |
176 |
|
"cegqi-bv-skvinv", |
177 |
|
"cegqi-bv-skvinv-debug", |
178 |
|
"cegqi-ce-atoms", |
179 |
|
"cegqi-check", |
180 |
|
"cegqi-debug", |
181 |
|
"cegqi-debug2", |
182 |
|
"cegqi-dt-debug", |
183 |
|
"cegqi-engine", |
184 |
|
"cegqi-gn", |
185 |
|
"cegqi-gn-debug", |
186 |
|
"cegqi-inst", |
187 |
|
"cegqi-inst-debug", |
188 |
|
"cegqi-inst-debug2", |
189 |
|
"cegqi-inv", |
190 |
|
"cegqi-inv-auto-unfold", |
191 |
|
"cegqi-inv-debug", |
192 |
|
"cegqi-inv-debug2", |
193 |
|
"cegqi-lemma", |
194 |
|
"cegqi-mv", |
195 |
|
"cegqi-nested-qe", |
196 |
|
"cegqi-nested-qe-debug", |
197 |
|
"cegqi-proc", |
198 |
|
"cegqi-proc-debug", |
199 |
|
"cegqi-qep", |
200 |
|
"cegqi-quant", |
201 |
|
"cegqi-quant-debug", |
202 |
|
"cegqi-refine", |
203 |
|
"cegqi-refine-debug", |
204 |
|
"cegqi-reg", |
205 |
|
"cegqi-sol-debug", |
206 |
|
"cegqi-warn", |
207 |
|
"check-abduct", |
208 |
|
"check-interpol", |
209 |
|
"check-model", |
210 |
|
"check-synth-sol", |
211 |
|
"circuit-prop", |
212 |
|
"clause-split-debug", |
213 |
|
"cnf", |
214 |
|
"cnf-steps", |
215 |
|
"combineTheories", |
216 |
|
"cond-var-split-debug", |
217 |
|
"conjecture-count", |
218 |
|
"context_mm", |
219 |
|
"cr-filter", |
220 |
|
"cr-filter-debug", |
221 |
|
"crf-match", |
222 |
|
"crf-match-debug", |
223 |
|
"csi-sol", |
224 |
|
"datatypes", |
225 |
|
"datatypes-cg", |
226 |
|
"datatypes-check", |
227 |
|
"datatypes-cycle-check", |
228 |
|
"datatypes-cycle-check2", |
229 |
|
"datatypes-debug", |
230 |
|
"datatypes-force-assign", |
231 |
|
"datatypes-infer", |
232 |
|
"datatypes-infer-debug", |
233 |
|
"datatypes-init", |
234 |
|
"datatypes-merge", |
235 |
|
"datatypes-prereg", |
236 |
|
"datatypes-proc", |
237 |
|
"datatypes-rewrite", |
238 |
|
"datatypes-rewrite-debug", |
239 |
|
"datatypes-wrong-sel", |
240 |
|
"dec-manager", |
241 |
|
"dec-manager-debug", |
242 |
|
"dec-strategy-debug", |
243 |
|
"decision", |
244 |
|
"decision-init", |
245 |
|
"decision-node", |
246 |
|
"decision::jh", |
247 |
|
"decision::jh::ite", |
248 |
|
"decision::jh::skolems", |
249 |
|
"diff-man", |
250 |
|
"difficulty", |
251 |
|
"difficulty-debug", |
252 |
|
"dt-card", |
253 |
|
"dt-cdt", |
254 |
|
"dt-cdt-debug", |
255 |
|
"dt-cg", |
256 |
|
"dt-cg-debug", |
257 |
|
"dt-cg-pair", |
258 |
|
"dt-cg-summary", |
259 |
|
"dt-cmi", |
260 |
|
"dt-cmi-cdt-debug", |
261 |
|
"dt-cmi-debug", |
262 |
|
"dt-collapse-sel", |
263 |
|
"dt-conflict", |
264 |
|
"dt-entail", |
265 |
|
"dt-enum-nn", |
266 |
|
"dt-expand", |
267 |
|
"dt-ipc", |
268 |
|
"dt-lemma-debug", |
269 |
|
"dt-model", |
270 |
|
"dt-model-debug", |
271 |
|
"dt-nconst", |
272 |
|
"dt-nconst-debug", |
273 |
|
"dt-rewrite-match", |
274 |
|
"dt-rewrite-project", |
275 |
|
"dt-shared-sel", |
276 |
|
"dt-singleton", |
277 |
|
"dt-split", |
278 |
|
"dt-split-debug", |
279 |
|
"dt-sygus", |
280 |
|
"dt-sygus-debug", |
281 |
|
"dt-sygus-fv", |
282 |
|
"dt-sygus-util", |
283 |
|
"dt-tester", |
284 |
|
"dt-tester-debug", |
285 |
|
"dt-wf", |
286 |
|
"dtsygus-gen-debug", |
287 |
|
"dtview", |
288 |
|
"dtview::command", |
289 |
|
"dtview::conflict", |
290 |
|
"dtview::prop", |
291 |
|
"dump-proof-error", |
292 |
|
"dyn-rewrite", |
293 |
|
"dyn-rewrite-debug", |
294 |
|
"ee-central", |
295 |
|
"eem-central", |
296 |
|
"ensureLiteral", |
297 |
|
"eq-exp", |
298 |
|
"eqproof-conv", |
299 |
|
"evaluator", |
300 |
|
"ex-infer", |
301 |
|
"ex-infer-debug", |
302 |
|
"example-cache", |
303 |
|
"ext-rew-bcp", |
304 |
|
"ext-rew-bcp-debug", |
305 |
|
"ext-rew-eqchain", |
306 |
|
"ext-rew-eqres", |
307 |
|
"ext-rew-factoring", |
308 |
|
"ext-rew-ite", |
309 |
|
"extt-debug", |
310 |
|
"extt-lemma", |
311 |
|
"extt-nred", |
312 |
|
"fd-eval", |
313 |
|
"fd-eval-debug", |
314 |
|
"fd-eval-debug2", |
315 |
|
"filter-instances", |
316 |
|
"final-pf-hole", |
317 |
|
"fm-debug", |
318 |
|
"fm-relevant", |
319 |
|
"fm-relevant-debug", |
320 |
|
"fmc", |
321 |
|
"fmc-cover-simplify", |
322 |
|
"fmc-debug", |
323 |
|
"fmc-debug-inst", |
324 |
|
"fmc-debug3", |
325 |
|
"fmc-eval", |
326 |
|
"fmc-exh", |
327 |
|
"fmc-exh-debug", |
328 |
|
"fmc-if-process", |
329 |
|
"fmc-inst", |
330 |
|
"fmc-model", |
331 |
|
"fmc-model-debug", |
332 |
|
"fmc-model-func", |
333 |
|
"fmc-model-simplify", |
334 |
|
"fmc-simplify", |
335 |
|
"fmc-test-inst", |
336 |
|
"fmc-uf-debug", |
337 |
|
"fmc-uf-entry", |
338 |
|
"fmc-uf-process", |
339 |
|
"fmc-warn", |
340 |
|
"fmf-consistent", |
341 |
|
"fmf-exh-inst", |
342 |
|
"fmf-exh-inst-debug", |
343 |
|
"fmf-fun-def", |
344 |
|
"fmf-fun-def-debug", |
345 |
|
"fmf-fun-def-debug2", |
346 |
|
"fmf-fun-def-rewrite", |
347 |
|
"fmf-incomplete", |
348 |
|
"fmf-model-complete", |
349 |
|
"fmf-uf-process-debug", |
350 |
|
"fmf-warn", |
351 |
|
"fp", |
352 |
|
"fp-abstraction", |
353 |
|
"fp-collectModelInfo", |
354 |
|
"fp-expandDefinition", |
355 |
|
"fp-ppRewrite", |
356 |
|
"fp-preRegisterTerm", |
357 |
|
"fp-refineAbstraction", |
358 |
|
"fp-registerTerm", |
359 |
|
"fp-rewrite", |
360 |
|
"fp-type", |
361 |
|
"fp-wordBlastTerm", |
362 |
|
"fs-engine", |
363 |
|
"functions", |
364 |
|
"gmc-count", |
365 |
|
"ho-elim-assert", |
366 |
|
"ho-elim-ax", |
367 |
|
"ho-elim-ll", |
368 |
|
"ho-elim-visit", |
369 |
|
"ho-quant", |
370 |
|
"ho-quant-trigger", |
371 |
|
"ho-quant-trigger-debug", |
372 |
|
"ho-unif-debug", |
373 |
|
"ho-unif-debug2", |
374 |
|
"iand", |
375 |
|
"iand-check", |
376 |
|
"iand-lemma", |
377 |
|
"iand-mv", |
378 |
|
"im", |
379 |
|
"infer-manager", |
380 |
|
"inst", |
381 |
|
"inst-add-debug", |
382 |
|
"inst-add-debug2", |
383 |
|
"inst-alg", |
384 |
|
"inst-alg-debug", |
385 |
|
"inst-alg-rd", |
386 |
|
"inst-assert", |
387 |
|
"inst-debug", |
388 |
|
"inst-engine", |
389 |
|
"inst-engine-debug", |
390 |
|
"inst-exp-fail", |
391 |
|
"inst-level-debug", |
392 |
|
"inst-level-debug2", |
393 |
|
"inst-match-gen", |
394 |
|
"inst-match-gen-warn", |
395 |
|
"inst-per-quant", |
396 |
|
"inst-per-quant-round", |
397 |
|
"int-blaster", |
398 |
|
"int-blaster-debug", |
399 |
|
"int-to-bv-debug", |
400 |
|
"integers", |
401 |
|
"internal-rep-debug", |
402 |
|
"internal-rep-select", |
403 |
|
"internal-rep-warn", |
404 |
|
"jh-assert", |
405 |
|
"jh-debug", |
406 |
|
"jh-process", |
407 |
|
"jh-stack", |
408 |
|
"jh-status", |
409 |
|
"justified", |
410 |
|
"lambda-const", |
411 |
|
"lazy-cdproof", |
412 |
|
"lazy-cdproof-debug", |
413 |
|
"lazy-cdproof-gen", |
414 |
|
"lazy-cdproofchain", |
415 |
|
"lazy-cdproofchain-debug", |
416 |
|
"lazy-trie-multi", |
417 |
|
"learned-rewrite", |
418 |
|
"learned-rewrite-arith-lit", |
419 |
|
"learned-rewrite-assert", |
420 |
|
"learned-rewrite-ll", |
421 |
|
"learned-rewrite-rr-debug", |
422 |
|
"lfsc-pp", |
423 |
|
"lfsc-pp-cong", |
424 |
|
"lfsc-pp-debug", |
425 |
|
"lfsc-pp-qcong", |
426 |
|
"lfsc-print-debug", |
427 |
|
"lfsc-print-debug2", |
428 |
|
"lfsc-term-process-debug", |
429 |
|
"lfsc-term-process-debug2", |
430 |
|
"libpoly::interval_connect", |
431 |
|
"limit", |
432 |
|
"macros", |
433 |
|
"macros-debug", |
434 |
|
"macros-debug2", |
435 |
|
"match-debug", |
436 |
|
"matching", |
437 |
|
"matching-debug2", |
438 |
|
"matching-fail", |
439 |
|
"matching-summary", |
440 |
|
"mkVar", |
441 |
|
"model-basis-term", |
442 |
|
"model-blocker", |
443 |
|
"model-blocker-debug", |
444 |
|
"model-build-aes", |
445 |
|
"model-builder", |
446 |
|
"model-builder-assertions", |
447 |
|
"model-builder-debug", |
448 |
|
"model-builder-debug2", |
449 |
|
"model-builder-fun", |
450 |
|
"model-builder-fun-debug", |
451 |
|
"model-builder-reps", |
452 |
|
"model-core", |
453 |
|
"model-engine", |
454 |
|
"model-engine-debug", |
455 |
|
"model-final", |
456 |
|
"multi-trigger", |
457 |
|
"multi-trigger-cache", |
458 |
|
"multi-trigger-cache-debug", |
459 |
|
"multi-trigger-cache2", |
460 |
|
"multi-trigger-debug", |
461 |
|
"multi-trigger-linear", |
462 |
|
"multi-trigger-linear-debug", |
463 |
|
"nconv-debug", |
464 |
|
"nconv-debug2", |
465 |
|
"nl-cad", |
466 |
|
"nl-cad-checker", |
467 |
|
"nl-ext", |
468 |
|
"nl-ext-assert-debug", |
469 |
|
"nl-ext-bound", |
470 |
|
"nl-ext-bound-debug", |
471 |
|
"nl-ext-bound-debug2", |
472 |
|
"nl-ext-bound-lemma", |
473 |
|
"nl-ext-checker", |
474 |
|
"nl-ext-cm", |
475 |
|
"nl-ext-cm-assert", |
476 |
|
"nl-ext-cm-debug", |
477 |
|
"nl-ext-cms", |
478 |
|
"nl-ext-cms-debug", |
479 |
|
"nl-ext-comp", |
480 |
|
"nl-ext-comp-debug", |
481 |
|
"nl-ext-comp-infer", |
482 |
|
"nl-ext-comp-lemma", |
483 |
|
"nl-ext-concavity", |
484 |
|
"nl-ext-constraint", |
485 |
|
"nl-ext-debug", |
486 |
|
"nl-ext-debug2", |
487 |
|
"nl-ext-exp", |
488 |
|
"nl-ext-exp-taylor", |
489 |
|
"nl-ext-factor", |
490 |
|
"nl-ext-lemma", |
491 |
|
"nl-ext-mindex", |
492 |
|
"nl-ext-mindex-debug", |
493 |
|
"nl-ext-model", |
494 |
|
"nl-ext-mono-factor", |
495 |
|
"nl-ext-mv", |
496 |
|
"nl-ext-mv-assert", |
497 |
|
"nl-ext-mv-debug", |
498 |
|
"nl-ext-mvo", |
499 |
|
"nl-ext-proc", |
500 |
|
"nl-ext-purify", |
501 |
|
"nl-ext-rbound", |
502 |
|
"nl-ext-rbound-debug", |
503 |
|
"nl-ext-rbound-lemma", |
504 |
|
"nl-ext-rbound-lemma-debug", |
505 |
|
"nl-ext-rlv", |
506 |
|
"nl-ext-sine", |
507 |
|
"nl-ext-tf", |
508 |
|
"nl-ext-tf-mono", |
509 |
|
"nl-ext-tf-mono-debug", |
510 |
|
"nl-ext-tftp", |
511 |
|
"nl-ext-tftp-debug", |
512 |
|
"nl-ext-tplanes", |
513 |
|
"nl-ext-zero-exp", |
514 |
|
"nl-icp", |
515 |
|
"nl-model", |
516 |
|
"nl-strategy", |
517 |
|
"nl-subs", |
518 |
|
"nl-trans", |
519 |
|
"nl-trans-checker", |
520 |
|
"nl-trans-lemma", |
521 |
|
"non-clausal-simplify", |
522 |
|
"options", |
523 |
|
"par-op", |
524 |
|
"parser", |
525 |
|
"parser-overloading", |
526 |
|
"parser-qid", |
527 |
|
"pf-process", |
528 |
|
"pf-process-debug", |
529 |
|
"pf::sat", |
530 |
|
"pfcheck", |
531 |
|
"pfcheck-strings-cprop", |
532 |
|
"pfee", |
533 |
|
"pfee-debug", |
534 |
|
"pfee-fact-gen", |
535 |
|
"pfee-proof", |
536 |
|
"pfee-proof-final", |
537 |
|
"pfgen", |
538 |
|
"pfnu-debug", |
539 |
|
"pfnu-debug2", |
540 |
|
"pnm", |
541 |
|
"pnm-scope", |
542 |
|
"poly::conversion", |
543 |
|
"pool-engine", |
544 |
|
"pool-inst", |
545 |
|
"pool-terms", |
546 |
|
"pow2", |
547 |
|
"pow2-check", |
548 |
|
"pow2-lemma", |
549 |
|
"pow2-mv", |
550 |
|
"pp-llm", |
551 |
|
"pre-sk", |
552 |
|
"preprocessing", |
553 |
|
"process-trigger", |
554 |
|
"proof-pedantic", |
555 |
|
"prop-proof-pp", |
556 |
|
"prop-proof-pp-debug", |
557 |
|
"properExplanation", |
558 |
|
"pushpop", |
559 |
|
"q-ext-rewrite", |
560 |
|
"q-ext-rewrite-apply", |
561 |
|
"q-ext-rewrite-debug", |
562 |
|
"q-ext-rewrite-debug2", |
563 |
|
"q-ext-rewrite-nf", |
564 |
|
"qcf-check", |
565 |
|
"qcf-check-debug", |
566 |
|
"qcf-check-unassign", |
567 |
|
"qcf-check2", |
568 |
|
"qcf-debug", |
569 |
|
"qcf-engine", |
570 |
|
"qcf-explain", |
571 |
|
"qcf-inst", |
572 |
|
"qcf-instance-check", |
573 |
|
"qcf-instance-check-debug", |
574 |
|
"qcf-invalid", |
575 |
|
"qcf-opt", |
576 |
|
"qcf-opt-debug", |
577 |
|
"qcf-qregister", |
578 |
|
"qcf-qregister-debug", |
579 |
|
"qcf-qregister-debug2", |
580 |
|
"qcf-qregister-summary", |
581 |
|
"qcf-qregister-vo", |
582 |
|
"qcf-tconstraint", |
583 |
|
"qcf-tconstraint-debug", |
584 |
|
"qcf-warn", |
585 |
|
"qstate-debug", |
586 |
|
"quant", |
587 |
|
"quant-attr", |
588 |
|
"quant-attr-debug", |
589 |
|
"quant-check-model", |
590 |
|
"quant-debug", |
591 |
|
"quant-dsplit", |
592 |
|
"quant-dsplit-debug", |
593 |
|
"quant-engine", |
594 |
|
"quant-engine-assert", |
595 |
|
"quant-engine-debug", |
596 |
|
"quant-engine-debug2", |
597 |
|
"quant-engine-ee", |
598 |
|
"quant-engine-ee-pre", |
599 |
|
"quant-engine-proc", |
600 |
|
"quant-engine-red", |
601 |
|
"quant-ho", |
602 |
|
"quant-init-debug", |
603 |
|
"quant-velim-bv", |
604 |
|
"quant-vts-debug", |
605 |
|
"quant-vts-warn", |
606 |
|
"quant-warn", |
607 |
|
"quantifiers-pre-rewrite", |
608 |
|
"quantifiers-prenex", |
609 |
|
"quantifiers-preprocess", |
610 |
|
"quantifiers-preprocess-debug", |
611 |
|
"quantifiers-presolve", |
612 |
|
"quantifiers-rewrite", |
613 |
|
"quantifiers-rewrite-debug", |
614 |
|
"quantifiers-rewrite-ite", |
615 |
|
"quantifiers-rewrite-ite-debug", |
616 |
|
"quantifiers-rewrite-term-debug2", |
617 |
|
"quantifiers-sk", |
618 |
|
"quantifiers-sk-debug", |
619 |
|
"quick-clique", |
620 |
|
"re-elim", |
621 |
|
"re-elim-debug", |
622 |
|
"real-as-int", |
623 |
|
"real-as-int-debug", |
624 |
|
"regexp-debug", |
625 |
|
"regexp-delta", |
626 |
|
"regexp-derive", |
627 |
|
"regexp-ext-rewrite", |
628 |
|
"regexp-ext-rewrite-debug", |
629 |
|
"regexp-fset", |
630 |
|
"regexp-int", |
631 |
|
"regexp-int-debug", |
632 |
|
"regexp-intersect", |
633 |
|
"regexp-intersect-node", |
634 |
|
"regexp-process", |
635 |
|
"rel-dom", |
636 |
|
"rel-dom-debug", |
637 |
|
"rel-manager", |
638 |
|
"relational-match-gen", |
639 |
|
"relational-trigger", |
640 |
|
"rels", |
641 |
|
"rels-debug", |
642 |
|
"rels-ee", |
643 |
|
"rels-eq", |
644 |
|
"rels-lemma", |
645 |
|
"rels-postrewrite", |
646 |
|
"rels-share", |
647 |
|
"reps-complete", |
648 |
|
"rewriter", |
649 |
|
"rewriter-proof", |
650 |
|
"rr-check", |
651 |
|
"rsi", |
652 |
|
"rsi-debug", |
653 |
|
"rtf-debug", |
654 |
|
"rtf-proof-debug", |
655 |
|
"sat-proof", |
656 |
|
"sat-proof-debug", |
657 |
|
"sat-proof-debug2", |
658 |
|
"sat-rlv-assert", |
659 |
|
"sel-trigger", |
660 |
|
"sel-trigger-debug", |
661 |
|
"sep", |
662 |
|
"sep-bound", |
663 |
|
"sep-check", |
664 |
|
"sep-conflict", |
665 |
|
"sep-eqc", |
666 |
|
"sep-inst", |
667 |
|
"sep-inst-debug", |
668 |
|
"sep-lemma", |
669 |
|
"sep-lemma-debug", |
670 |
|
"sep-model", |
671 |
|
"sep-postrewrite", |
672 |
|
"sep-pp", |
673 |
|
"sep-pp-debug", |
674 |
|
"sep-preprocess", |
675 |
|
"sep-prerewrite", |
676 |
|
"sep-process", |
677 |
|
"sep-process-debug", |
678 |
|
"sep-pto", |
679 |
|
"sep-pto-debug", |
680 |
|
"sep-rewrite", |
681 |
|
"sep-type", |
682 |
|
"sep-warn", |
683 |
|
"seq-array", |
684 |
|
"seq-array-debug", |
685 |
|
"sequences-postrewrite", |
686 |
|
"set-type-enum", |
687 |
|
"setp-model", |
688 |
|
"sets", |
689 |
|
"sets-assertion", |
690 |
|
"sets-card", |
691 |
|
"sets-card-debug", |
692 |
|
"sets-cdg", |
693 |
|
"sets-cg", |
694 |
|
"sets-cg-debug", |
695 |
|
"sets-cg-lemma", |
696 |
|
"sets-cg-pair", |
697 |
|
"sets-cg-summary", |
698 |
|
"sets-check", |
699 |
|
"sets-comprehension", |
700 |
|
"sets-cycle-debug", |
701 |
|
"sets-debug", |
702 |
|
"sets-debug2", |
703 |
|
"sets-deq", |
704 |
|
"sets-eqc", |
705 |
|
"sets-fact", |
706 |
|
"sets-incomplete", |
707 |
|
"sets-intro", |
708 |
|
"sets-isconst", |
709 |
|
"sets-lemma", |
710 |
|
"sets-mem", |
711 |
|
"sets-model", |
712 |
|
"sets-nf", |
713 |
|
"sets-nf-debug", |
714 |
|
"sets-pinfer", |
715 |
|
"sets-postrewrite", |
716 |
|
"sets-prop", |
717 |
|
"sets-prop-debug", |
718 |
|
"sets-rels-postrewrite", |
719 |
|
"sets-rewrite", |
720 |
|
"sets-rewrite-nf", |
721 |
|
"sets-state", |
722 |
|
"sg-cconj", |
723 |
|
"sg-cconj-debug", |
724 |
|
"sg-cconj-debug2", |
725 |
|
"sg-cconj-witness", |
726 |
|
"sg-conjecture", |
727 |
|
"sg-conjecture-debug", |
728 |
|
"sg-conjecture-debug2", |
729 |
|
"sg-engine", |
730 |
|
"sg-engine-debug", |
731 |
|
"sg-gen-consider-term", |
732 |
|
"sg-gen-consider-term-debug", |
733 |
|
"sg-gen-eqc", |
734 |
|
"sg-gen-tg-debug", |
735 |
|
"sg-gen-tg-debug2", |
736 |
|
"sg-gen-tg-match", |
737 |
|
"sg-gt-enum", |
738 |
|
"sg-gt-enum-debug", |
739 |
|
"sg-pat", |
740 |
|
"sg-pat-debug", |
741 |
|
"sg-pending", |
742 |
|
"sg-proc", |
743 |
|
"sg-proc-debug", |
744 |
|
"sg-rel-prop", |
745 |
|
"sg-rel-sig", |
746 |
|
"sg-rel-sig-debug", |
747 |
|
"sg-rel-term", |
748 |
|
"sg-rel-term-debug", |
749 |
|
"sg-stats", |
750 |
|
"sg-term-enum", |
751 |
|
"shared-solver", |
752 |
|
"sharing", |
753 |
|
"si-prt", |
754 |
|
"si-prt-debug", |
755 |
|
"simplify", |
756 |
|
"sk-defs", |
757 |
|
"sk-ind", |
758 |
|
"sk-ind-debug", |
759 |
|
"sk-manager", |
760 |
|
"sk-manager-debug", |
761 |
|
"sk-manager-skolem", |
762 |
|
"skolem-cache", |
763 |
|
"smt", |
764 |
|
"smt-debug", |
765 |
|
"smt-pppg", |
766 |
|
"smt-pppg-debug", |
767 |
|
"smt-proc", |
768 |
|
"smt-proof", |
769 |
|
"smt-proof-debug", |
770 |
|
"smt-proof-pp", |
771 |
|
"smt-proof-pp-debug", |
772 |
|
"smt-proof-pp-debug2", |
773 |
|
"smt-qe", |
774 |
|
"smt-qe-debug", |
775 |
|
"sort-infer-preprocess", |
776 |
|
"sort-inference", |
777 |
|
"sort-inference-debug", |
778 |
|
"sort-inference-debug2", |
779 |
|
"sort-inference-proc", |
780 |
|
"sort-inference-rewrite", |
781 |
|
"sort-inference-temp", |
782 |
|
"sort-inference-warn", |
783 |
|
"srs-input", |
784 |
|
"srs-input-debug", |
785 |
|
"strings-assert", |
786 |
|
"strings-base", |
787 |
|
"strings-base-debug", |
788 |
|
"strings-card", |
789 |
|
"strings-cg", |
790 |
|
"strings-cg-debug", |
791 |
|
"strings-cg-pair", |
792 |
|
"strings-check", |
793 |
|
"strings-check-debug", |
794 |
|
"strings-code-debug", |
795 |
|
"strings-conflict", |
796 |
|
"strings-csolver", |
797 |
|
"strings-cycle", |
798 |
|
"strings-debug", |
799 |
|
"strings-debug-model", |
800 |
|
"strings-dstrat-reg", |
801 |
|
"strings-eager-aconf", |
802 |
|
"strings-eager-aconf-debug", |
803 |
|
"strings-eager-pconf", |
804 |
|
"strings-eager-pconf-debug", |
805 |
|
"strings-ent-approx", |
806 |
|
"strings-ent-approx-debug", |
807 |
|
"strings-entail", |
808 |
|
"strings-entail-debug", |
809 |
|
"strings-entail-ms-ss", |
810 |
|
"strings-eqc", |
811 |
|
"strings-eqc-debug", |
812 |
|
"strings-error", |
813 |
|
"strings-exp-def", |
814 |
|
"strings-explain-prefix", |
815 |
|
"strings-explain-prefix-debug", |
816 |
|
"strings-extf", |
817 |
|
"strings-extf-debug", |
818 |
|
"strings-extf-infer", |
819 |
|
"strings-extf-list", |
820 |
|
"strings-ff", |
821 |
|
"strings-ff-debug", |
822 |
|
"strings-fmf", |
823 |
|
"strings-infer-debug", |
824 |
|
"strings-ipc", |
825 |
|
"strings-ipc-core", |
826 |
|
"strings-ipc-debug", |
827 |
|
"strings-ipc-deq", |
828 |
|
"strings-ipc-fail", |
829 |
|
"strings-ipc-len", |
830 |
|
"strings-ipc-prefix", |
831 |
|
"strings-ipc-pure-subs", |
832 |
|
"strings-ipc-re", |
833 |
|
"strings-ipc-red", |
834 |
|
"strings-lemma", |
835 |
|
"strings-lemma-debug", |
836 |
|
"strings-loop", |
837 |
|
"strings-lp", |
838 |
|
"strings-model", |
839 |
|
"strings-nf", |
840 |
|
"strings-nf-debug", |
841 |
|
"strings-pending", |
842 |
|
"strings-pending-debug", |
843 |
|
"strings-pfcheck", |
844 |
|
"strings-pfcheck-debug", |
845 |
|
"strings-postrewrite", |
846 |
|
"strings-ppr", |
847 |
|
"strings-preprocess", |
848 |
|
"strings-preprocess-debug", |
849 |
|
"strings-preregister", |
850 |
|
"strings-process", |
851 |
|
"strings-process-debug", |
852 |
|
"strings-red-lemma", |
853 |
|
"strings-regexp", |
854 |
|
"strings-regexp-cstre", |
855 |
|
"strings-regexp-nf", |
856 |
|
"strings-regexp-simpl", |
857 |
|
"strings-register", |
858 |
|
"strings-rewrite", |
859 |
|
"strings-rewrite-cbound", |
860 |
|
"strings-rewrite-debug", |
861 |
|
"strings-rewrite-debug2", |
862 |
|
"strings-rewrite-nf", |
863 |
|
"strings-solve", |
864 |
|
"strings-solve-debug", |
865 |
|
"strings-solve-debug-test", |
866 |
|
"strings-solve-debug2", |
867 |
|
"strings-subs", |
868 |
|
"strings-subs-proxy", |
869 |
|
"strings-warn", |
870 |
|
"subs-min", |
871 |
|
"sygus-abduct", |
872 |
|
"sygus-abduct-debug", |
873 |
|
"sygus-active-gen", |
874 |
|
"sygus-active-gen-debug", |
875 |
|
"sygus-ccore", |
876 |
|
"sygus-ccore-debug", |
877 |
|
"sygus-ccore-debug-sy", |
878 |
|
"sygus-ccore-init", |
879 |
|
"sygus-ccore-ref", |
880 |
|
"sygus-ccore-summary", |
881 |
|
"sygus-ccore-sy", |
882 |
|
"sygus-check-value", |
883 |
|
"sygus-cons-kind", |
884 |
|
"sygus-cref-eval", |
885 |
|
"sygus-cref-eval2", |
886 |
|
"sygus-cref-eval2-debug", |
887 |
|
"sygus-db", |
888 |
|
"sygus-db-canon", |
889 |
|
"sygus-db-debug", |
890 |
|
"sygus-engine", |
891 |
|
"sygus-engine-debug", |
892 |
|
"sygus-engine-rr", |
893 |
|
"sygus-enum", |
894 |
|
"sygus-enum-debug", |
895 |
|
"sygus-enum-debug2", |
896 |
|
"sygus-enum-exc", |
897 |
|
"sygus-enum-summary", |
898 |
|
"sygus-enum-terms", |
899 |
|
"sygus-eval-unfold", |
900 |
|
"sygus-eval-unfold-debug", |
901 |
|
"sygus-fair", |
902 |
|
"sygus-fair-debug", |
903 |
|
"sygus-gnorm", |
904 |
|
"sygus-grammar-def", |
905 |
|
"sygus-grammar-normalize", |
906 |
|
"sygus-grammar-normalize-build", |
907 |
|
"sygus-grammar-normalize-chain", |
908 |
|
"sygus-grammar-normalize-debug", |
909 |
|
"sygus-grammar-normalize-infer", |
910 |
|
"sygus-grammar-normalize-trie", |
911 |
|
"sygus-infer", |
912 |
|
"sygus-infer-debug", |
913 |
|
"sygus-inst", |
914 |
|
"sygus-inst-term", |
915 |
|
"sygus-interpol", |
916 |
|
"sygus-interpol-debug", |
917 |
|
"sygus-pbe", |
918 |
|
"sygus-pbe-cterm", |
919 |
|
"sygus-pbe-cterm-debug", |
920 |
|
"sygus-pbe-cterm-debug2", |
921 |
|
"sygus-pbe-debug", |
922 |
|
"sygus-pbe-dt", |
923 |
|
"sygus-pbe-enum", |
924 |
|
"sygus-pbe-sol", |
925 |
|
"sygus-process", |
926 |
|
"sygus-process-arg-deps", |
927 |
|
"sygus-qgen", |
928 |
|
"sygus-qgen-check", |
929 |
|
"sygus-qgen-check-debug", |
930 |
|
"sygus-qgen-debug", |
931 |
|
"sygus-rcons", |
932 |
|
"sygus-red", |
933 |
|
"sygus-red-debug", |
934 |
|
"sygus-repair-const", |
935 |
|
"sygus-repair-const-debug", |
936 |
|
"sygus-rr-debug", |
937 |
|
"sygus-rr-filter", |
938 |
|
"sygus-rr-sb", |
939 |
|
"sygus-rr-verify", |
940 |
|
"sygus-sample", |
941 |
|
"sygus-sample-debug", |
942 |
|
"sygus-sample-ev", |
943 |
|
"sygus-sample-grammar", |
944 |
|
"sygus-sample-str-alpha", |
945 |
|
"sygus-sb", |
946 |
|
"sygus-sb-check-value", |
947 |
|
"sygus-sb-debug", |
948 |
|
"sygus-sb-debug2", |
949 |
|
"sygus-sb-exc", |
950 |
|
"sygus-sb-fair", |
951 |
|
"sygus-sb-fair-debug", |
952 |
|
"sygus-sb-mexp", |
953 |
|
"sygus-sb-mexp-debug", |
954 |
|
"sygus-sb-simple", |
955 |
|
"sygus-sb-simple-debug", |
956 |
|
"sygus-sb-tp", |
957 |
|
"sygus-sb-warn", |
958 |
|
"sygus-si", |
959 |
|
"sygus-si-apply-subs-debug", |
960 |
|
"sygus-si-debug", |
961 |
|
"sygus-si-trivial-solve", |
962 |
|
"sygus-sol-implied", |
963 |
|
"sygus-strat-slearn", |
964 |
|
"sygus-sui-cache", |
965 |
|
"sygus-sui-cterm", |
966 |
|
"sygus-sui-cterm-debug", |
967 |
|
"sygus-sui-debug", |
968 |
|
"sygus-sui-dt", |
969 |
|
"sygus-sui-dt-debug", |
970 |
|
"sygus-sui-dt-igain", |
971 |
|
"sygus-sui-enum", |
972 |
|
"sygus-sui-enum-debug", |
973 |
|
"sygus-sui-enum-lemma", |
974 |
|
"sygus-type-cons", |
975 |
|
"sygus-unif", |
976 |
|
"sygus-unif-cond-pool", |
977 |
|
"sygus-unif-debug", |
978 |
|
"sygus-unif-debug2", |
979 |
|
"sygus-unif-dt", |
980 |
|
"sygus-unif-dt-debug", |
981 |
|
"sygus-unif-rl-dt", |
982 |
|
"sygus-unif-rl-purify", |
983 |
|
"sygus-unif-rl-purify-debug", |
984 |
|
"sygus-unif-rl-sep", |
985 |
|
"sygus-unif-rl-strat", |
986 |
|
"sygus-unif-sol", |
987 |
|
"sygus-unif-sol-debug", |
988 |
|
"sygus-unif-sol-sym", |
989 |
|
"sym-manager", |
990 |
|
"sym-manager-debug", |
991 |
|
"sym-table", |
992 |
|
"synth-stream-concrete", |
993 |
|
"synth-stream-concrete-debug", |
994 |
|
"synth-stream-concrete-debug2", |
995 |
|
"tconv-pf-gen", |
996 |
|
"tconv-pf-gen-debug", |
997 |
|
"tconv-pf-gen-debug-pf", |
998 |
|
"tconv-pf-gen-rewrite", |
999 |
|
"tconv-seq-pf-gen", |
1000 |
|
"tconv-seq-pf-gen-debug", |
1001 |
|
"tctx-debug", |
1002 |
|
"tdb", |
1003 |
|
"te-lemma", |
1004 |
|
"te-proof-debug", |
1005 |
|
"te-proof-exp", |
1006 |
|
"tepg-debug", |
1007 |
|
"term-db", |
1008 |
|
"term-db-debug", |
1009 |
|
"term-db-debug2", |
1010 |
|
"term-db-entail", |
1011 |
|
"term-db-enum", |
1012 |
|
"term-db-eval", |
1013 |
|
"term-db-lemma", |
1014 |
|
"theory", |
1015 |
|
"theory-check", |
1016 |
|
"theory-engine-entc", |
1017 |
|
"theory::assertToTheory", |
1018 |
|
"theory::assertions", |
1019 |
|
"theory::assertions-model", |
1020 |
|
"theory::assertions::fulleffort", |
1021 |
|
"theory::conflict", |
1022 |
|
"theory::internal", |
1023 |
|
"theory::lemma", |
1024 |
|
"theory::propagate", |
1025 |
|
"theory::restart", |
1026 |
|
"theory::solve", |
1027 |
|
"thm-db", |
1028 |
|
"thm-db-debug", |
1029 |
|
"thm-ee", |
1030 |
|
"thm-ee-add", |
1031 |
|
"thm-ee-debug", |
1032 |
|
"thm-ee-no-add", |
1033 |
|
"tpp", |
1034 |
|
"tpp-debug", |
1035 |
|
"tpp-debug2", |
1036 |
|
"trigger", |
1037 |
|
"trigger-active-sel-debug", |
1038 |
|
"trigger-debug", |
1039 |
|
"trigger-filter-instance", |
1040 |
|
"trigger-gt-lemma", |
1041 |
|
"trigger-warn", |
1042 |
|
"trust-subs", |
1043 |
|
"trust-subs-pf", |
1044 |
|
"uf", |
1045 |
|
"uf-exp-def", |
1046 |
|
"uf-ho", |
1047 |
|
"uf-ho-beta", |
1048 |
|
"uf-ho-debug", |
1049 |
|
"uf-ho-lemma", |
1050 |
|
"uf-pfcheck", |
1051 |
|
"uf-ss", |
1052 |
|
"uf-ss-assert", |
1053 |
|
"uf-ss-com-card", |
1054 |
|
"uf-ss-com-card-debug", |
1055 |
|
"uf-ss-debug", |
1056 |
|
"uf-ss-lemma", |
1057 |
|
"uf-ss-register", |
1058 |
|
"uf-ss-si", |
1059 |
|
"uf-ss-solver", |
1060 |
|
"uf-ss-split-si", |
1061 |
|
"uf-ss-state", |
1062 |
|
"uf-ss-warn", |
1063 |
|
"uf-type-enum", |
1064 |
|
"unc-simp", |
1065 |
|
"uninterpretedSorts-to-bv", |
1066 |
|
"unsat-core", |
1067 |
|
"user-pat", |
1068 |
|
"userpushpop", |
1069 |
|
"var-elim-bool", |
1070 |
|
"var-elim-dt", |
1071 |
|
"var-elim-ineq-debug", |
1072 |
|
"var-elim-quant", |
1073 |
|
"var-elim-quant-debug", |
1074 |
|
"var-trigger", |
1075 |
|
"var-trigger-debug", |
1076 |
|
"var-trigger-matching", |
1077 |
|
"witness-form", |
1078 |
|
#endif |
1079 |
11159575 |
}; |