1 |
3934399 |
static const std::vector<std::string> Debug_tags = { |
2 |
|
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) |
3 |
|
"CDInsertHashMap", |
4 |
|
"Constraint::sanityChecking", |
5 |
|
"TheoryArithPrivate::solveRealRelaxation", |
6 |
|
"TrailHashMap", |
7 |
|
"approx", |
8 |
|
"approx::", |
9 |
|
"approx::branch", |
10 |
|
"approx::checkCutOnPad", |
11 |
|
"approx::constraint", |
12 |
|
"approx::gmi", |
13 |
|
"approx::gmiCut", |
14 |
|
"approx::guessIsConstructable", |
15 |
|
"approx::lemmas", |
16 |
|
"approx::mir", |
17 |
|
"approx::mirCut", |
18 |
|
"approx::nodelog", |
19 |
|
"approx::replayAssert", |
20 |
|
"approx::replayLog", |
21 |
|
"approx::replayLogRec", |
22 |
|
"approx::soi", |
23 |
|
"approx::solveMIP", |
24 |
|
"approx::sumConstraints", |
25 |
|
"approx::vars", |
26 |
|
"arith", |
27 |
|
"arith-pfee", |
28 |
|
"arith::SOIConflict", |
29 |
|
"arith::approx::cuts", |
30 |
|
"arith::arithvar", |
31 |
|
"arith::asVectors", |
32 |
|
"arith::bb", |
33 |
|
"arith::bt", |
34 |
|
"arith::channel", |
35 |
|
"arith::collectModelInfo", |
36 |
|
"arith::conflict", |
37 |
|
"arith::cong", |
38 |
|
"arith::cong::notzero", |
39 |
|
"arith::congruenceManager", |
40 |
|
"arith::congruences", |
41 |
|
"arith::consistency", |
42 |
|
"arith::consistency::comitonconflict", |
43 |
|
"arith::consistency::final", |
44 |
|
"arith::consistency::initial", |
45 |
|
"arith::constraint", |
46 |
|
"arith::decomp", |
47 |
|
"arith::dio", |
48 |
|
"arith::dio::ex", |
49 |
|
"arith::dio::max", |
50 |
|
"arith::distinct::const", |
51 |
|
"arith::dual", |
52 |
|
"arith::ems", |
53 |
|
"arith::entailCheck", |
54 |
|
"arith::eq", |
55 |
|
"arith::error::mem", |
56 |
|
"arith::explain", |
57 |
|
"arith::findModel", |
58 |
|
"arith::focus", |
59 |
|
"arith::generateSOIConflict", |
60 |
|
"arith::greedyConflictSubsets", |
61 |
|
"arith::hasIntegerModel", |
62 |
|
"arith::importSolution", |
63 |
|
"arith::intbound", |
64 |
|
"arith::ite", |
65 |
|
"arith::ite::red", |
66 |
|
"arith::learned", |
67 |
|
"arith::lemma", |
68 |
|
"arith::negatedassumption", |
69 |
|
"arith::nf", |
70 |
|
"arith::normalize::external", |
71 |
|
"arith::notifySharedTerm", |
72 |
|
"arith::oldprop", |
73 |
|
"arith::pf::check", |
74 |
|
"arith::pf::externalExplainConflict", |
75 |
|
"arith::pf::tree", |
76 |
|
"arith::pivot", |
77 |
|
"arith::preprocess", |
78 |
|
"arith::preregister", |
79 |
|
"arith::presolve", |
80 |
|
"arith::print_assertions", |
81 |
|
"arith::print_model", |
82 |
|
"arith::prop", |
83 |
|
"arith::prop::pf", |
84 |
|
"arith::propagateRow", |
85 |
|
"arith::resolveOutPropagated", |
86 |
|
"arith::restart", |
87 |
|
"arith::rewriter", |
88 |
|
"arith::selectPrimalUpdate", |
89 |
|
"arith::simplex:row", |
90 |
|
"arith::solveInteger", |
91 |
|
"arith::static", |
92 |
|
"arith::subsumption", |
93 |
|
"arith::toSumNode", |
94 |
|
"arith::tracking", |
95 |
|
"arith::tracking::mid", |
96 |
|
"arith::tracking::post", |
97 |
|
"arith::tracking::pre", |
98 |
|
"arith::unate", |
99 |
|
"arith::unateFarkasSigns", |
100 |
|
"arith::update", |
101 |
|
"arith::update::select", |
102 |
|
"arith::value", |
103 |
|
"arith::weak", |
104 |
|
"array-types", |
105 |
|
"arrays", |
106 |
|
"arrays::propagate", |
107 |
|
"arrays::sharing", |
108 |
|
"arrays::weak", |
109 |
|
"assertions::post-ackermann", |
110 |
|
"assertions::post-apply-substs", |
111 |
|
"assertions::post-bool-to-bv", |
112 |
|
"assertions::post-bv-eager-atoms", |
113 |
|
"assertions::post-bv-gauss", |
114 |
|
"assertions::post-bv-to-bool", |
115 |
|
"assertions::post-bv-to-int", |
116 |
|
"assertions::post-ext-rew-pre", |
117 |
|
"assertions::post-foreign-theory-rewrite", |
118 |
|
"assertions::post-fun-def-fmf", |
119 |
|
"assertions::post-global-negate", |
120 |
|
"assertions::post-ho-elim", |
121 |
|
"assertions::post-int-to-bv", |
122 |
|
"assertions::post-ite-removal", |
123 |
|
"assertions::post-ite-simp", |
124 |
|
"assertions::post-learned-rewrite", |
125 |
|
"assertions::post-miplib-trick", |
126 |
|
"assertions::post-nl-ext-purify", |
127 |
|
"assertions::post-non-clausal-simp", |
128 |
|
"assertions::post-pseudo-boolean-processor", |
129 |
|
"assertions::post-quantifiers-preprocess", |
130 |
|
"assertions::post-real-to-int", |
131 |
|
"assertions::post-rewrite", |
132 |
|
"assertions::post-sep-skolem-emp", |
133 |
|
"assertions::post-sort-inference", |
134 |
|
"assertions::post-static-learning", |
135 |
|
"assertions::post-strings-eager-pp", |
136 |
|
"assertions::post-sygus-infer", |
137 |
|
"assertions::post-synth-rr", |
138 |
|
"assertions::post-theory-preprocess", |
139 |
|
"assertions::post-theory-rewrite-eq", |
140 |
|
"assertions::post-unconstrained-simplifier", |
141 |
|
"assertions::pre-ackermann", |
142 |
|
"assertions::pre-apply-substs", |
143 |
|
"assertions::pre-bool-to-bv", |
144 |
|
"assertions::pre-bv-eager-atoms", |
145 |
|
"assertions::pre-bv-gauss", |
146 |
|
"assertions::pre-bv-to-bool", |
147 |
|
"assertions::pre-bv-to-int", |
148 |
|
"assertions::pre-ext-rew-pre", |
149 |
|
"assertions::pre-foreign-theory-rewrite", |
150 |
|
"assertions::pre-fun-def-fmf", |
151 |
|
"assertions::pre-global-negate", |
152 |
|
"assertions::pre-ho-elim", |
153 |
|
"assertions::pre-int-to-bv", |
154 |
|
"assertions::pre-ite-removal", |
155 |
|
"assertions::pre-ite-simp", |
156 |
|
"assertions::pre-learned-rewrite", |
157 |
|
"assertions::pre-miplib-trick", |
158 |
|
"assertions::pre-nl-ext-purify", |
159 |
|
"assertions::pre-non-clausal-simp", |
160 |
|
"assertions::pre-pseudo-boolean-processor", |
161 |
|
"assertions::pre-quantifiers-preprocess", |
162 |
|
"assertions::pre-real-to-int", |
163 |
|
"assertions::pre-rewrite", |
164 |
|
"assertions::pre-sep-skolem-emp", |
165 |
|
"assertions::pre-sort-inference", |
166 |
|
"assertions::pre-static-learning", |
167 |
|
"assertions::pre-strings-eager-pp", |
168 |
|
"assertions::pre-sygus-infer", |
169 |
|
"assertions::pre-synth-rr", |
170 |
|
"assertions::pre-theory-preprocess", |
171 |
|
"assertions::pre-theory-rewrite-eq", |
172 |
|
"assertions::pre-unconstrained-simplifier", |
173 |
|
"bags", |
174 |
|
"bags-eq", |
175 |
|
"basicsAtBounds", |
176 |
|
"bitvector", |
177 |
|
"bitvector-bb", |
178 |
|
"bitvector-expandDefinition", |
179 |
|
"bitvector-rewrite", |
180 |
|
"bool-flatten", |
181 |
|
"bool-ite", |
182 |
|
"bool-to-bv", |
183 |
|
"builder", |
184 |
|
"bv-bitblast", |
185 |
|
"bv-bitblast-internal", |
186 |
|
"bv-rewrite", |
187 |
|
"bv-to-bool", |
188 |
|
"bva", |
189 |
|
"cand-gen-qe", |
190 |
|
"cdlist", |
191 |
|
"cdqueue", |
192 |
|
"cegqi-debug", |
193 |
|
"circuit-prop", |
194 |
|
"combineTheories", |
195 |
|
"conflict", |
196 |
|
"constraint::conflictCommit", |
197 |
|
"constraints::hsfp", |
198 |
|
"constraints::pf", |
199 |
|
"constraints::wffp", |
200 |
|
"constructInfeasiblityFunction", |
201 |
|
"context", |
202 |
|
"core", |
203 |
|
"cores", |
204 |
|
"current", |
205 |
|
"datatypes", |
206 |
|
"datatypes-labels", |
207 |
|
"datatypes-parametric", |
208 |
|
"decision", |
209 |
|
"decision::jh", |
210 |
|
"determineArithVar", |
211 |
|
"diamonds", |
212 |
|
"dio::push", |
213 |
|
"dio::pushInputConstraint", |
214 |
|
"dt", |
215 |
|
"dt-cdt-debug", |
216 |
|
"dt-enum", |
217 |
|
"dt-enum-debug", |
218 |
|
"dt-model-debug", |
219 |
|
"dualLike", |
220 |
|
"equality", |
221 |
|
"equality::backtrack", |
222 |
|
"equality::disequality", |
223 |
|
"equality::evaluation", |
224 |
|
"equality::extoperator", |
225 |
|
"equality::graph", |
226 |
|
"equality::internal", |
227 |
|
"equality::trigger", |
228 |
|
"equalsConstant", |
229 |
|
"error", |
230 |
|
"estimateWithCFE", |
231 |
|
"expand", |
232 |
|
"fmc-entry-trie", |
233 |
|
"fmf-full-check", |
234 |
|
"fmf-model-eval", |
235 |
|
"focusDownToJust", |
236 |
|
"focusDownToLastHalf", |
237 |
|
"foo", |
238 |
|
"fp-eq", |
239 |
|
"fp-rewrite", |
240 |
|
"fp-wordBlastTerm", |
241 |
|
"friendlyparser", |
242 |
|
"gaussianElimConstructTableRow", |
243 |
|
"gc", |
244 |
|
"gc:leaks", |
245 |
|
"getBestImpliedBound", |
246 |
|
"getCeiling", |
247 |
|
"getPropagatedLiterals", |
248 |
|
"getType", |
249 |
|
"glpk::loadVB", |
250 |
|
"guessCoefficientsConstructTableRow", |
251 |
|
"guessIsConstructable", |
252 |
|
"handleBorders", |
253 |
|
"includeBoundUpdate", |
254 |
|
"inst-engine", |
255 |
|
"inst-engine-debug", |
256 |
|
"inst-engine-phase-req", |
257 |
|
"inst-trigger", |
258 |
|
"integers", |
259 |
|
"integers::pf", |
260 |
|
"interactive", |
261 |
|
"intersectConstantIte", |
262 |
|
"isConst", |
263 |
|
"ite", |
264 |
|
"ite::atom", |
265 |
|
"ite::constantIteEqualsConstant", |
266 |
|
"ite::print-success", |
267 |
|
"ite::simpite", |
268 |
|
"limit", |
269 |
|
"logPivot", |
270 |
|
"macro::arith", |
271 |
|
"matrix", |
272 |
|
"minisat", |
273 |
|
"minisat::lemmas", |
274 |
|
"minisat::pop", |
275 |
|
"minisat::search", |
276 |
|
"miplib", |
277 |
|
"model", |
278 |
|
"model-getvalue", |
279 |
|
"model-getvalue-debug", |
280 |
|
"newproof::sat", |
281 |
|
"nf::tmp", |
282 |
|
"normal-form", |
283 |
|
"options", |
284 |
|
"paranoid:check_tableau", |
285 |
|
"parser", |
286 |
|
"parser-dt", |
287 |
|
"parser-extra", |
288 |
|
"parser-idt", |
289 |
|
"parser-param", |
290 |
|
"parser-sygus", |
291 |
|
"partial_model", |
292 |
|
"pb", |
293 |
|
"pbs::rewrites", |
294 |
|
"pf::arith", |
295 |
|
"pf::arith::explain", |
296 |
|
"pf::array", |
297 |
|
"pf::ee", |
298 |
|
"pipe", |
299 |
|
"polynomial", |
300 |
|
"preemptGetopt", |
301 |
|
"prop", |
302 |
|
"prop-explain", |
303 |
|
"prop-value", |
304 |
|
"prop::lemmas", |
305 |
|
"properConflict", |
306 |
|
"qcf-ccbe", |
307 |
|
"qcf-check-inst", |
308 |
|
"qcf-match", |
309 |
|
"qcf-match-debug", |
310 |
|
"qcf-match-debug2", |
311 |
|
"quantifiers-engine", |
312 |
|
"quantifiers-prereg", |
313 |
|
"quantifiers-presolve", |
314 |
|
"quantifiers::collectModelInfo", |
315 |
|
"queueConditions", |
316 |
|
"rationalToCfe", |
317 |
|
"recentlyViolated", |
318 |
|
"register", |
319 |
|
"register::internal", |
320 |
|
"relevant-trigger", |
321 |
|
"removeFixed", |
322 |
|
"rl", |
323 |
|
"sat::cryptominisat", |
324 |
|
"selectFocusImproving", |
325 |
|
"sep", |
326 |
|
"sep::propagate", |
327 |
|
"sets", |
328 |
|
"sets-checknormal", |
329 |
|
"sets-eq", |
330 |
|
"sets-proc", |
331 |
|
"shared-terms-database", |
332 |
|
"shared-terms-database::assert", |
333 |
|
"sharing", |
334 |
|
"simple-trigger", |
335 |
|
"simple-trigger-debug", |
336 |
|
"simplify", |
337 |
|
"smt", |
338 |
|
"soi::findModel", |
339 |
|
"soi::selectPrimalUpdate", |
340 |
|
"solveRealRelaxation", |
341 |
|
"sort", |
342 |
|
"speculativeUpdate", |
343 |
|
"strings", |
344 |
|
"strings-explain", |
345 |
|
"strings-presolve", |
346 |
|
"substitution", |
347 |
|
"substitution::internal", |
348 |
|
"tableau", |
349 |
|
"theory", |
350 |
|
"theory-bv", |
351 |
|
"theory-bv-pp-rewrite", |
352 |
|
"theory::assertions", |
353 |
|
"theory::atoms", |
354 |
|
"theory::bv::rewrite", |
355 |
|
"theory::conflict", |
356 |
|
"theory::explain", |
357 |
|
"theory::propagate", |
358 |
|
"theoryDecision", |
359 |
|
"tuprec", |
360 |
|
"tuprec-debug", |
361 |
|
"typecheck-idt", |
362 |
|
"typecheck-q", |
363 |
|
"uf", |
364 |
|
"uf-notify", |
365 |
|
"uf-ss", |
366 |
|
"uf-ss-check-region", |
367 |
|
"uf-ss-debug", |
368 |
|
"uf-ss-disequal", |
369 |
|
"uf-ss-region", |
370 |
|
"uf-ss-region-debug", |
371 |
|
"uf-ss-sat", |
372 |
|
"uf::sharing", |
373 |
|
"ufsymm", |
374 |
|
"ufsymm:clauses", |
375 |
|
"ufsymm:eq", |
376 |
|
"ufsymm:match", |
377 |
|
"ufsymm:norm", |
378 |
|
"ufsymm:p", |
379 |
|
"update", |
380 |
|
"updateAndSignal", |
381 |
|
#endif |
382 |
3924018 |
}; |