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