1 |
2646816 |
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 |
|
"bags", |
110 |
|
"bags-eq", |
111 |
|
"basicsAtBounds", |
112 |
|
"bitblast-queue", |
113 |
|
"bitvector", |
114 |
|
"bitvector-aig", |
115 |
|
"bitvector-bb", |
116 |
|
"bitvector-bitblast", |
117 |
|
"bitvector-eager", |
118 |
|
"bitvector-expandDefinition", |
119 |
|
"bitvector-model", |
120 |
|
"bitvector-preregister", |
121 |
|
"bitvector-rewrite", |
122 |
|
"bitvector::bitblaster", |
123 |
|
"bitvector::core", |
124 |
|
"bitvector::explain", |
125 |
|
"bitvector::propagate", |
126 |
|
"bitvector::sharing", |
127 |
|
"bool-flatten", |
128 |
|
"bool-ite", |
129 |
|
"bool-to-bv", |
130 |
|
"builder", |
131 |
|
"bv-abstraction", |
132 |
|
"bv-abstraction-dbg", |
133 |
|
"bv-abstraction-dgb", |
134 |
|
"bv-abstraction-gen", |
135 |
|
"bv-bitblast", |
136 |
|
"bv-bitblast-debug", |
137 |
|
"bv-bitblast-internal", |
138 |
|
"bv-bitblast-queue", |
139 |
|
"bv-core", |
140 |
|
"bv-core-model", |
141 |
|
"bv-equality-status", |
142 |
|
"bv-inequality", |
143 |
|
"bv-inequality-explain", |
144 |
|
"bv-inequality-internal", |
145 |
|
"bv-pp-rewrite", |
146 |
|
"bv-quick-xplain", |
147 |
|
"bv-rewrite", |
148 |
|
"bv-slicer-eq", |
149 |
|
"bv-substitution", |
150 |
|
"bv-subtheory-algebraic", |
151 |
|
"bv-subtheory-inequality", |
152 |
|
"bv-term-model", |
153 |
|
"bv-to-bool", |
154 |
|
"bva", |
155 |
|
"bvminisat", |
156 |
|
"bvminisat::explain", |
157 |
|
"bvminisat::search", |
158 |
|
"cand-gen-qe", |
159 |
|
"cdlist", |
160 |
|
"cdqueue", |
161 |
|
"cegqi-debug", |
162 |
|
"circuit-prop", |
163 |
|
"combineTheories", |
164 |
|
"conflict", |
165 |
|
"constraint::conflictCommit", |
166 |
|
"constraints::hsfp", |
167 |
|
"constraints::pf", |
168 |
|
"constraints::wffp", |
169 |
|
"constructInfeasiblityFunction", |
170 |
|
"context", |
171 |
|
"core", |
172 |
|
"cores", |
173 |
|
"current", |
174 |
|
"datatypes", |
175 |
|
"datatypes-labels", |
176 |
|
"datatypes-parametric", |
177 |
|
"datatypes-split", |
178 |
|
"decision", |
179 |
|
"decision::jh", |
180 |
|
"determineArithVar", |
181 |
|
"diamonds", |
182 |
|
"dio::push", |
183 |
|
"dio::pushInputConstraint", |
184 |
|
"dt", |
185 |
|
"dt-cdt-debug", |
186 |
|
"dt-enum", |
187 |
|
"dt-enum-debug", |
188 |
|
"dt-model-debug", |
189 |
|
"dualLike", |
190 |
|
"equality", |
191 |
|
"equality::backtrack", |
192 |
|
"equality::disequality", |
193 |
|
"equality::evaluation", |
194 |
|
"equality::extoperator", |
195 |
|
"equality::graph", |
196 |
|
"equality::internal", |
197 |
|
"equality::trigger", |
198 |
|
"equalsConstant", |
199 |
|
"error", |
200 |
|
"estimateWithCFE", |
201 |
|
"expand", |
202 |
|
"fmc-entry-trie", |
203 |
|
"fmf-full-check", |
204 |
|
"fmf-model-eval", |
205 |
|
"focusDownToJust", |
206 |
|
"focusDownToLastHalf", |
207 |
|
"foo", |
208 |
|
"fp-eq", |
209 |
|
"fp-rewrite", |
210 |
|
"fp-wordBlastTerm", |
211 |
|
"friendlyparser", |
212 |
|
"gaussianElimConstructTableRow", |
213 |
|
"gc", |
214 |
|
"gc:leaks", |
215 |
|
"getBestImpliedBound", |
216 |
|
"getCeiling", |
217 |
|
"getPropagatedLiterals", |
218 |
|
"getType", |
219 |
|
"glpk::loadVB", |
220 |
|
"guessCoefficientsConstructTableRow", |
221 |
|
"guessIsConstructable", |
222 |
|
"handleBorders", |
223 |
|
"includeBoundUpdate", |
224 |
|
"inst-engine", |
225 |
|
"inst-engine-debug", |
226 |
|
"inst-engine-phase-req", |
227 |
|
"inst-trigger", |
228 |
|
"integers", |
229 |
|
"integers::pf", |
230 |
|
"interactive", |
231 |
|
"intersectConstantIte", |
232 |
|
"isConst", |
233 |
|
"ite", |
234 |
|
"ite::atom", |
235 |
|
"ite::constantIteEqualsConstant", |
236 |
|
"ite::print-success", |
237 |
|
"ite::simpite", |
238 |
|
"limit", |
239 |
|
"logPivot", |
240 |
|
"macro::arith", |
241 |
|
"matrix", |
242 |
|
"minisat", |
243 |
|
"minisat::lemmas", |
244 |
|
"minisat::pop", |
245 |
|
"minisat::search", |
246 |
|
"miplib", |
247 |
|
"model", |
248 |
|
"model-getvalue", |
249 |
|
"model-getvalue-debug", |
250 |
|
"newproof::sat", |
251 |
|
"nf::tmp", |
252 |
|
"normal-form", |
253 |
|
"options", |
254 |
|
"paranoid:check_tableau", |
255 |
|
"parser", |
256 |
|
"parser-dt", |
257 |
|
"parser-extra", |
258 |
|
"parser-idt", |
259 |
|
"parser-param", |
260 |
|
"parser-sygus", |
261 |
|
"partial_model", |
262 |
|
"pb", |
263 |
|
"pbs::rewrites", |
264 |
|
"pf::arith", |
265 |
|
"pf::arith::explain", |
266 |
|
"pf::array", |
267 |
|
"pf::ee", |
268 |
|
"pipe", |
269 |
|
"polynomial", |
270 |
|
"preemptGetopt", |
271 |
|
"prop", |
272 |
|
"prop-explain", |
273 |
|
"prop-value", |
274 |
|
"prop::lemmas", |
275 |
|
"properConflict", |
276 |
|
"qcf-ccbe", |
277 |
|
"qcf-check-inst", |
278 |
|
"qcf-match", |
279 |
|
"qcf-match-debug", |
280 |
|
"qcf-match-debug2", |
281 |
|
"quantifiers-engine", |
282 |
|
"quantifiers-prereg", |
283 |
|
"quantifiers-presolve", |
284 |
|
"quantifiers::collectModelInfo", |
285 |
|
"queueConditions", |
286 |
|
"rationalToCfe", |
287 |
|
"recentlyViolated", |
288 |
|
"register", |
289 |
|
"register::internal", |
290 |
|
"relevant-trigger", |
291 |
|
"removeFixed", |
292 |
|
"rl", |
293 |
|
"sat::cryptominisat", |
294 |
|
"sat::minisat", |
295 |
|
"selectFocusImproving", |
296 |
|
"sep", |
297 |
|
"sep::propagate", |
298 |
|
"sets", |
299 |
|
"sets-checknormal", |
300 |
|
"sets-eq", |
301 |
|
"sets-proc", |
302 |
|
"shared-terms-database", |
303 |
|
"shared-terms-database::assert", |
304 |
|
"sharing", |
305 |
|
"simple-trigger", |
306 |
|
"simple-trigger-debug", |
307 |
|
"simplify", |
308 |
|
"smt", |
309 |
|
"soi::findModel", |
310 |
|
"soi::selectPrimalUpdate", |
311 |
|
"solveRealRelaxation", |
312 |
|
"sort", |
313 |
|
"speculativeUpdate", |
314 |
|
"strings", |
315 |
|
"strings-explain", |
316 |
|
"strings-presolve", |
317 |
|
"substitution", |
318 |
|
"substitution::internal", |
319 |
|
"tableau", |
320 |
|
"theory", |
321 |
|
"theory-bv", |
322 |
|
"theory::assertions", |
323 |
|
"theory::atoms", |
324 |
|
"theory::bv::rewrite", |
325 |
|
"theory::conflict", |
326 |
|
"theory::explain", |
327 |
|
"theory::propagate", |
328 |
|
"theoryDecision", |
329 |
|
"tuprec", |
330 |
|
"tuprec-debug", |
331 |
|
"typecheck-idt", |
332 |
|
"typecheck-q", |
333 |
|
"uf", |
334 |
|
"uf-notify", |
335 |
|
"uf-ss", |
336 |
|
"uf-ss-check-region", |
337 |
|
"uf-ss-debug", |
338 |
|
"uf-ss-disequal", |
339 |
|
"uf-ss-region", |
340 |
|
"uf-ss-region-debug", |
341 |
|
"uf-ss-sat", |
342 |
|
"uf::sharing", |
343 |
|
"ufsymm", |
344 |
|
"ufsymm:clauses", |
345 |
|
"ufsymm:eq", |
346 |
|
"ufsymm:match", |
347 |
|
"ufsymm:norm", |
348 |
|
"ufsymm:p", |
349 |
|
"update", |
350 |
|
"updateAndSignal", |
351 |
|
#endif |
352 |
2639232 |
}; |