Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The proof manager of the SMT engine.
11 : : */
12 : :
13 : : #include "smt/proof_manager.h"
14 : :
15 : : #include "expr/subtype_elim_node_converter.h"
16 : : #include "options/base_options.h"
17 : : #include "options/main_options.h"
18 : : #include "options/smt_options.h"
19 : : #include "proof/alethe/alethe_node_converter.h"
20 : : #include "proof/alethe/alethe_post_processor.h"
21 : : #include "proof/alethe/alethe_printer.h"
22 : : #include "proof/dot/dot_printer.h"
23 : : #include "proof/eo/eo_printer.h"
24 : : #include "proof/lfsc/lfsc_post_processor.h"
25 : : #include "proof/lfsc/lfsc_printer.h"
26 : : #include "proof/proof_checker.h"
27 : : #include "proof/proof_node_algorithm.h"
28 : : #include "proof/proof_node_manager.h"
29 : : #include "rewriter/rewrite_db.h"
30 : : #include "smt/assertions.h"
31 : : #include "smt/difficulty_post_processor.h"
32 : : #include "smt/env.h"
33 : : #include "smt/preprocess_proof_generator.h"
34 : : #include "smt/proof_logger.h"
35 : : #include "smt/proof_post_processor.h"
36 : : #include "smt/smt_solver.h"
37 : :
38 : : using namespace cvc5::internal::rewriter;
39 : : namespace cvc5::internal {
40 : : namespace smt {
41 : :
42 : 15170 : PfManager::PfManager(Env& env)
43 : : : EnvObj(env),
44 : 15170 : d_rewriteDb(nullptr),
45 : 15170 : d_pchecker(nullptr),
46 : 15170 : d_pnm(nullptr),
47 : 15170 : d_pfpp(nullptr),
48 : 15170 : d_pppg(nullptr),
49 : 15170 : d_finalCb(env),
50 : 45510 : d_finalizer(env, d_finalCb)
51 : : {
52 : : // construct the rewrite db only if DSL rewrites are enabled
53 : 15170 : if (options().proof.proofGranularityMode
54 : : == options::ProofGranularityMode::DSL_REWRITE
55 [ + + ][ - + ]: 15170 : || options().proof.proofGranularityMode
[ + + ]
56 : : == options::ProofGranularityMode::DSL_REWRITE_STRICT)
57 : : {
58 : 6764 : d_rewriteDb.reset(new RewriteDb(nodeManager()));
59 : : // maybe output rare rules?
60 : 6764 : bool isNormalOut = isOutputOn(OutputTag::RARE_DB);
61 : 6764 : bool isExpertOut = isOutputOn(OutputTag::RARE_DB_EXPERT);
62 [ + - ][ - + ]: 6764 : if (isNormalOut || isExpertOut)
63 : : {
64 [ - - ]: 0 : if (options().proof.proofFormatMode != options::ProofFormatMode::CPC)
65 : : {
66 [ - - ]: 0 : Warning()
67 : : << "WARNING: Assuming --proof-format=cpc when printing the RARE "
68 : 0 : "database with -o rare-db(-expert)"
69 : 0 : << std::endl;
70 : : }
71 : 0 : proof::EoNodeConverter atp(nodeManager());
72 : 0 : proof::EoPrinter eop(d_env, atp, d_rewriteDb.get());
73 : : const std::map<ProofRewriteRule, RewriteProofRule>& rules =
74 : 0 : d_rewriteDb->getAllRules();
75 [ - - ]: 0 : for (const std::pair<const ProofRewriteRule, RewriteProofRule>& r : rules)
76 : : {
77 : : // only output if the signature level is what we want
78 : 0 : Level l = r.second.getSignatureLevel();
79 [ - - ][ - - ]: 0 : if (l == Level::NORMAL && isNormalOut)
80 : : {
81 : 0 : std::ostream& os = output(OutputTag::RARE_DB);
82 : 0 : eop.printDslRule(os, r.first);
83 : 0 : }
84 [ - - ][ - - ]: 0 : else if (l == Level::EXPERT && isExpertOut)
85 : : {
86 : 0 : std::ostream& os = output(OutputTag::RARE_DB_EXPERT);
87 : 0 : eop.printDslRule(os, r.first);
88 : : }
89 : : }
90 : 0 : }
91 : : }
92 : :
93 : : // enable the proof checker and the proof node manager
94 : 15170 : d_pchecker.reset(
95 : 15170 : new ProofChecker(statisticsRegistry(),
96 : 15170 : options().proof.proofCheck,
97 : 15170 : static_cast<uint32_t>(options().proof.proofPedantic),
98 : 15170 : d_rewriteDb.get()));
99 : 30340 : d_pnm.reset(new ProofNodeManager(env.getNodeManager(),
100 : 15170 : env.getOptions(),
101 : 15170 : env.getRewriter(),
102 : 15170 : d_pchecker.get()));
103 : : // Now, initialize the proof postprocessor with the environment.
104 : : // By default the post-processor will update all assumptions, which
105 : : // can lead to SCOPE subproofs of the form
106 : : // A
107 : : // ...
108 : : // B1 B2
109 : : // ... ...
110 : : // ------------
111 : : // C
112 : : // ------------- SCOPE [B1, B2]
113 : : // B1 ^ B2 => C
114 : : //
115 : : // where A is an available assumption from outside the scope (note
116 : : // that B1 was an assumption of this SCOPE subproof but since it could
117 : : // be inferred from A, it was updated). This shape is problematic for
118 : : // the Alethe reconstruction, so we disable the update of scoped
119 : : // assumptions (which would disable the update of B1 in this case).
120 : 15170 : d_pfpp = std::make_unique<ProofPostprocess>(
121 : : env,
122 : 15170 : d_rewriteDb.get(),
123 : 30340 : options().proof.proofFormatMode != options::ProofFormatMode::ALETHE);
124 : :
125 : : // add rules to eliminate here
126 : 15170 : if (options().proof.proofGranularityMode
127 [ + + ]: 15170 : != options::ProofGranularityMode::MACRO)
128 : : {
129 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_EQ_INTRO);
130 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_INTRO);
131 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_ELIM);
132 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_TRANSFORM);
133 : : // Alethe does not require chain multiset resolution to be expanded,
134 : : // LFSC requires it to be expanded.
135 : 8700 : if ((options().proof.proofFormatMode != options::ProofFormatMode::ALETHE
136 [ + - ]: 6810 : && !options().proof.proofChainMRes)
137 [ + + ][ + + ]: 15510 : || options().proof.proofFormatMode == options::ProofFormatMode::LFSC)
[ + + ]
138 : : {
139 : 1930 : d_pfpp->setEliminateRule(ProofRule::CHAIN_M_RESOLUTION);
140 : : }
141 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_ARITH_SCALE_SUM_UB);
142 : 8700 : if (options().proof.proofGranularityMode
143 [ + - ]: 8700 : != options::ProofGranularityMode::REWRITE)
144 : : {
145 : 8700 : d_pfpp->setEliminateRule(ProofRule::SUBS);
146 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_REWRITE);
147 : : // if in a DSL rewrite mode
148 : 8700 : if (options().proof.proofGranularityMode
149 [ + + ]: 8700 : != options::ProofGranularityMode::THEORY_REWRITE)
150 : : {
151 : : // this eliminates theory rewriting steps with finer-grained DSL rules
152 : 6764 : d_pfpp->setEliminateAllTrustedRules();
153 : : }
154 : : }
155 : : // theory-specific lazy proof reconstruction
156 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_STRING_INFERENCE);
157 : 8700 : d_pfpp->setEliminateRule(ProofRule::MACRO_BV_BITBLAST);
158 : : // we only try to eliminate TRUST if not macro level
159 : 8700 : d_pfpp->setEliminateRule(ProofRule::TRUST);
160 : : }
161 : 15170 : d_false = nodeManager()->mkConst(false);
162 : :
163 : 15170 : d_pppg = std::make_unique<PreprocessProofGenerator>(
164 : 15170 : d_env, userContext(), "smt::PreprocessProofGenerator");
165 : 15170 : }
166 : :
167 : 30339 : PfManager::~PfManager() {}
168 : :
169 : : // TODO: Remove in favor of `std::erase_if` with C++ 20+ (see cvc5-wishues#137).
170 : : template <class T, class Alloc, class Pred>
171 : 10588 : constexpr typename std::vector<T, Alloc>::size_type erase_if(
172 : : std::vector<T, Alloc>& c, Pred pred)
173 : : {
174 : : typename std::vector<T, Alloc>::iterator it =
175 : 10588 : std::remove_if(c.begin(), c.end(), pred);
176 : 10588 : typename std::vector<T, Alloc>::size_type r = std::distance(it, c.end());
177 : 10588 : c.erase(it, c.end());
178 : 10588 : return r;
179 : : }
180 : :
181 : 0 : void PfManager::startProofLogging(std::ostream& out, Assertions& as)
182 : : {
183 : : // by default, CPC proof logger
184 : 0 : d_plog.reset(new ProofLoggerCpc(d_env, out, this, as));
185 : 0 : }
186 : :
187 : 11330 : std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
188 : : std::shared_ptr<ProofNode> pfn, Assertions& as, ProofScopeMode scopeMode)
189 : : {
190 : : // Note this assumes that connectProofToAssertions is only called once per
191 : : // unsat response. This method would need to cache its result otherwise.
192 [ + - ]: 22660 : Trace("smt-proof")
193 : 11330 : << "SolverEngine::connectProofToAssertions(): get proof body...\n";
194 : :
195 [ - + ]: 11330 : if (TraceIsOn("smt-proof-debug"))
196 : : {
197 [ - - ]: 0 : Trace("smt-proof-debug")
198 : 0 : << "SolverEngine::connectProofToAssertions(): Proof node for false:\n";
199 [ - - ]: 0 : Trace("smt-proof-debug") << *pfn.get() << std::endl;
200 [ - - ]: 0 : Trace("smt-proof-debug") << "=====" << std::endl;
201 : : }
202 : 11330 : std::vector<Node> assertions;
203 : 11330 : getAssertions(as, assertions);
204 : :
205 [ - + ]: 11330 : if (TraceIsOn("smt-proof"))
206 : : {
207 [ - - ]: 0 : Trace("smt-proof")
208 : 0 : << "SolverEngine::connectProofToAssertions(): get free assumptions..."
209 : 0 : << std::endl;
210 : 0 : std::vector<Node> fassumps;
211 : 0 : expr::getFreeAssumptions(pfn.get(), fassumps);
212 [ - - ]: 0 : Trace("smt-proof") << "SolverEngine::connectProofToAssertions(): initial "
213 : 0 : "free assumptions are:\n";
214 [ - - ]: 0 : for (const Node& a : fassumps)
215 : : {
216 [ - - ]: 0 : Trace("smt-proof") << "- " << a << std::endl;
217 : : }
218 : :
219 [ - - ]: 0 : Trace("smt-proof")
220 : 0 : << "SolverEngine::connectProofToAssertions(): assertions are:\n";
221 [ - - ]: 0 : for (const Node& n : assertions)
222 : : {
223 [ - - ]: 0 : Trace("smt-proof") << "- " << n << std::endl;
224 : : }
225 [ - - ]: 0 : Trace("smt-proof") << "=====" << std::endl;
226 : 0 : }
227 : :
228 [ + - ]: 22660 : Trace("smt-proof")
229 : 11330 : << "SolverEngine::connectProofToAssertions(): postprocess...\n";
230 [ - + ][ - + ]: 11330 : Assert(d_pfpp != nullptr);
[ - - ]
231 : : // Note that in incremental mode, we cannot set assertions here, as it
232 : : // permits the postprocessor to merge subproofs at a higher user context
233 : : // level into proofs that are used in a lower user context level.
234 [ + + ]: 11330 : if (!options().base.incrementalSolving)
235 : : {
236 : 10230 : d_pfpp->setAssertions(assertions, false);
237 : : }
238 [ + - ]: 11330 : d_pfpp->process(pfn, d_pppg.get());
239 : :
240 [ + + ][ + - ]: 11330 : switch (scopeMode)
241 : : {
242 : 36 : case ProofScopeMode::NONE:
243 : : {
244 : 36 : return pfn;
245 : : }
246 : : // Now make the final scope(s), which ensure(s) that the only open leaves
247 : : // of the proof are the assertions (and definitions). If we are pruning
248 : : // the input, we will try to minimize the used assertions (and definitions).
249 : 6000 : case ProofScopeMode::UNIFIED:
250 : : {
251 [ + - ]: 12000 : Trace("smt-proof") << "SolverEngine::connectProofToAssertions(): make "
252 : 6000 : "unified scope...\n";
253 : : return d_pnm->mkScope(
254 : 6000 : pfn, assertions, true, options().proof.proofPruneInput);
255 : : }
256 : 5294 : case ProofScopeMode::DEFINITIONS_AND_ASSERTIONS:
257 : : {
258 [ + - ]: 10588 : Trace("smt-proof")
259 : 5294 : << "SolverEngine::connectProofToAssertions(): make split scope...\n";
260 : : // To support proof pruning for nested scopes, we need to:
261 : : // 1. Minimize assertions of closed unified scope.
262 : 5294 : std::vector<Node> unifiedAssertions;
263 : 5294 : getAssertions(as, unifiedAssertions);
264 : : Pf pf = d_pnm->mkScope(
265 : 10588 : pfn, unifiedAssertions, true, options().proof.proofPruneInput);
266 : : // if this is violated, there is unsoundness since we have shown
267 : : // false that does not depend on the input.
268 [ - + ][ - + ]: 5294 : AlwaysAssert(pf->getRule() == ProofRule::SCOPE);
[ - - ]
269 : : // 2. Extract minimum unified assertions from the scope node.
270 : 5294 : std::unordered_set<Node> minUnifiedAssertions;
271 : 5294 : minUnifiedAssertions.insert(pf->getArguments().cbegin(),
272 : 5294 : pf->getArguments().cend());
273 : : // 3. Split those assertions into minimized definitions and assertions.
274 : 5294 : std::vector<Node> minDefinitions;
275 : 5294 : std::vector<Node> minAssertions;
276 : 5294 : getDefinitionsAndAssertions(as, minDefinitions, minAssertions);
277 : 98668 : std::function<bool(Node)> predicate = [&minUnifiedAssertions](Node n) {
278 : 49334 : return minUnifiedAssertions.find(n) == minUnifiedAssertions.cend();
279 : 5294 : };
280 : 5294 : erase_if(minDefinitions, predicate);
281 : 5294 : erase_if(minAssertions, predicate);
282 : : // 4. Extract proof from unified scope and encapsulate it with split
283 : : // scopes introducing minimized definitions and assertions.
284 : 5294 : return d_pnm->mkNode(
285 : : ProofRule::SCOPE,
286 : : {d_pnm->mkNode(ProofRule::SCOPE, pf->getChildren(), minAssertions)},
287 : 10588 : minDefinitions);
288 : 5294 : }
289 : 0 : default: Unreachable();
290 : : }
291 : 11330 : }
292 : :
293 : 2505 : void PfManager::checkFinalProof(std::shared_ptr<ProofNode> pfn)
294 : : {
295 : : // take stats and check pedantic
296 : 2505 : d_finalCb.initializeUpdate();
297 : 2505 : d_finalizer.process(pfn);
298 : :
299 : 2505 : std::stringstream serr;
300 : 2505 : bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
301 [ - + ]: 2505 : if (wasPedanticFailure)
302 : : {
303 : 0 : AlwaysAssert(!wasPedanticFailure)
304 : 0 : << "ProofPostprocess::process: pedantic failure:" << std::endl
305 : 0 : << serr.str();
306 : : }
307 : 2505 : }
308 : :
309 : 5319 : void PfManager::printProof(std::ostream& out,
310 : : std::shared_ptr<ProofNode> fp,
311 : : options::ProofFormatMode mode,
312 : : ProofScopeMode scopeMode,
313 : : const std::map<Node, std::string>& assertionNames)
314 : : {
315 [ + - ]: 5319 : Trace("smt-proof") << "PfManager::printProof: start " << mode << std::endl;
316 : : // We don't want to invalidate the proof nodes in fp, since these may be
317 : : // reused in further check-sat calls, or they may be used again if the
318 : : // user asks for the proof again (in non-incremental mode). We don't need to
319 : : // clone if the printing below does not modify the proof, which is the case
320 : : // for proof formats Eunoia and NONE.
321 [ + + ]: 5319 : if (mode != options::ProofFormatMode::CPC
322 [ + + ]: 3527 : && mode != options::ProofFormatMode::NONE)
323 : : {
324 : 3483 : fp = fp->clone();
325 : : }
326 : :
327 : : // according to the proof format, post process and print the proof node
328 [ - + ]: 5319 : if (mode == options::ProofFormatMode::DOT)
329 : : {
330 : 0 : proof::DotPrinter dotPrinter(d_env);
331 : 0 : dotPrinter.print(out, fp.get());
332 : 0 : }
333 [ + + ]: 5319 : else if (mode == options::ProofFormatMode::CPC)
334 : : {
335 : 1792 : proof::EoNodeConverter atp(nodeManager());
336 : 1792 : proof::EoPrinter eop(d_env, atp, d_rewriteDb.get());
337 : 1792 : eop.print(out, fp, scopeMode);
338 : 1792 : }
339 [ + + ]: 3527 : else if (mode == options::ProofFormatMode::ALETHE)
340 : : {
341 : 1734 : options::ProofCheckMode oldMode = options().proof.proofCheck;
342 : 1734 : d_pnm->getChecker()->setProofCheckMode(options::ProofCheckMode::NONE);
343 : : proof::AletheNodeConverter anc(nodeManager(),
344 : 3468 : options().proof.proofAletheDefineSkolems,
345 : 1734 : options().proof.proofAletheTesting);
346 : 1734 : proof::AletheProofPostprocess vpfpp(d_env, anc);
347 [ + + ]: 1734 : if (vpfpp.process(fp))
348 : : {
349 : 476 : proof::AletheProofPrinter vpp(d_env, anc);
350 : 476 : vpp.print(out, fp, assertionNames);
351 : 476 : }
352 : : else
353 : : {
354 : 1258 : out << "(error " << vpfpp.getError() << ")";
355 : : }
356 : 1734 : d_pnm->getChecker()->setProofCheckMode(oldMode);
357 : 1734 : }
358 [ + + ]: 1793 : else if (mode == options::ProofFormatMode::LFSC)
359 : : {
360 [ - + ][ - + ]: 1749 : Assert(fp->getRule() == ProofRule::SCOPE);
[ - - ]
361 : 1749 : proof::LfscNodeConverter ltp(nodeManager());
362 : 1749 : proof::LfscProofPostprocess lpp(d_env, ltp);
363 : 1749 : lpp.process(fp);
364 : 1749 : proof::LfscPrinter lp(d_env, ltp, d_rewriteDb.get());
365 : 1749 : lp.print(out, fp.get());
366 : 1749 : }
367 : : else
368 : : {
369 : : // otherwise, print using default printer
370 : : // we call the printing method explicitly because we may want to print the
371 : : // final proof node with conclusions
372 : 44 : fp->printDebug(out, options().proof.proofPrintConclusion);
373 : : }
374 : 5319 : }
375 : :
376 : 19 : void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
377 : : Assertions& as)
378 : : {
379 [ + - ]: 19 : Trace("difficulty-proc") << "Translate difficulty start" << std::endl;
380 [ + - ]: 19 : Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl;
381 [ + + ]: 19 : if (dmap.empty())
382 : : {
383 : 6 : return;
384 : : }
385 : 15 : std::map<Node, Node> dmapp;
386 [ + - ]: 15 : Trace("difficulty-proc") << "Get ppAsserts" << std::endl;
387 : 15 : std::vector<Node> ppAsserts;
388 : 15 : SubtypeElimNodeConverter senc(nodeManager());
389 [ + + ]: 54 : for (const std::pair<const Node, Node>& ppa : dmap)
390 : : {
391 : 39 : Node assertion = ppa.first;
392 : : // proof may eliminate mixed arithmetic from the assertion
393 [ + - ]: 39 : if (options().proof.proofElimSubtypes)
394 : : {
395 : 39 : assertion = senc.convert(ppa.first);
396 : : }
397 : 39 : dmapp[assertion] = ppa.second;
398 [ + - ]: 78 : Trace("difficulty") << " preprocess difficulty: " << assertion << " for "
399 : 39 : << ppa.first << std::endl;
400 : : // The difficulty manager should only report difficulty for preprocessed
401 : : // assertions, or we will get an open proof below. This is ensured
402 : : // internally by the difficuly manager.
403 : 39 : ppAsserts.push_back(ppa.first);
404 : 39 : }
405 : 15 : dmap.clear();
406 [ + - ]: 15 : Trace("difficulty-proc") << "Make SAT refutation" << std::endl;
407 : : // assume a SAT refutation from all input assertions that were marked
408 : : // as having a difficulty
409 : 30 : CDProof cdp(d_env);
410 : 15 : Node fnode = nodeManager()->mkConst(false);
411 : 15 : cdp.addStep(fnode, ProofRule::SAT_REFUTATION, ppAsserts, {});
412 : 15 : std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
413 [ + - ]: 15 : Trace("difficulty-proc") << "Get final proof" << std::endl;
414 : 15 : std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, as);
415 [ + - ]: 15 : Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl;
416 : : // We are typically a SCOPE here, although if we are not, then the proofs
417 : : // have no free assumptions. If this is the case, then the only difficulty
418 : : // was incremented on auxiliary lemmas added during preprocessing. Since
419 : : // there are no dependencies, then the difficulty map is empty.
420 [ + + ]: 15 : if (fpf->getRule() != ProofRule::SCOPE)
421 : : {
422 : 2 : return;
423 : : }
424 : 13 : fpf = fpf->getChildren()[0];
425 : : // analyze proof
426 [ - + ][ - + ]: 13 : Assert(fpf->getRule() == ProofRule::SAT_REFUTATION);
[ - - ]
427 : 13 : const std::vector<std::shared_ptr<ProofNode>>& children = fpf->getChildren();
428 : 13 : DifficultyPostprocessCallback dpc;
429 : 13 : ProofNodeUpdater dpnu(d_env, dpc);
430 [ + - ]: 13 : Trace("difficulty-proc") << "Compute accumulated difficulty" << std::endl;
431 : : // For each child of SAT_REFUTATION, we increment the difficulty on all
432 : : // "source" free assumptions (see DifficultyPostprocessCallback) by the
433 : : // difficulty of the preprocessed assertion.
434 [ + + ]: 50 : for (const std::shared_ptr<ProofNode>& c : children)
435 : : {
436 : 37 : Node res = c->getResult();
437 : 37 : Assert(dmapp.find(res) != dmapp.end())
438 : 0 : << "Could not find assumption " << res;
439 [ + - ]: 37 : Trace("difficulty-debug") << " process: " << res << std::endl;
440 [ + - ]: 37 : Trace("difficulty-debug") << " .dvalue: " << dmapp[res] << std::endl;
441 [ + - ]: 37 : Trace("difficulty-debug") << " ..proof: " << *c.get() << std::endl;
442 [ - + ]: 37 : if (!dpc.setCurrentDifficulty(dmapp[res]))
443 : : {
444 : 0 : continue;
445 : : }
446 : 37 : dpnu.process(c);
447 [ + - ]: 37 : }
448 : : // get the accumulated difficulty map from the callback
449 : 13 : dpc.getDifficultyMap(nodeManager(), dmap);
450 [ + - ]: 13 : Trace("difficulty-proc") << "Translate difficulty end" << std::endl;
451 [ + + ][ + + ]: 27 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ]
452 : :
453 : 0 : ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
454 : :
455 : 15182 : ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
456 : :
457 : 21199 : ProofLogger* PfManager::getProofLogger() const { return d_plog.get(); }
458 : :
459 : 0 : rewriter::RewriteDb* PfManager::getRewriteDatabase() const
460 : : {
461 : 0 : return d_rewriteDb.get();
462 : : }
463 : :
464 : 15185 : PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
465 : : {
466 : 15185 : return d_pppg.get();
467 : : }
468 : :
469 : 16624 : void PfManager::getAssertions(Assertions& as, std::vector<Node>& assertions)
470 : : {
471 : : // note that the assertion list is always available
472 : 16624 : const context::CDList<Node>& al = as.getAssertionList();
473 [ + + ]: 159711 : for (const Node& a : al)
474 : : {
475 : 143087 : assertions.push_back(a);
476 : : }
477 : 16624 : }
478 : :
479 : 5294 : void PfManager::getDefinitionsAndAssertions(Assertions& as,
480 : : std::vector<Node>& definitions,
481 : : std::vector<Node>& assertions)
482 : : {
483 : 5294 : const context::CDList<Node>& defs = as.getAssertionListDefinitions();
484 [ + + ]: 6964 : for (const Node& d : defs)
485 : : {
486 : : // Keep treating (mutually) recursive functions as declarations +
487 : : // assertions.
488 [ + - ]: 1670 : if (d.getKind() == Kind::EQUAL)
489 : : {
490 : 1670 : definitions.push_back(d);
491 : : }
492 : : }
493 : 5294 : const context::CDList<Node>& asserts = as.getAssertionList();
494 [ + + ]: 54628 : for (const Node& a : asserts)
495 : : {
496 : 49334 : if (std::find(definitions.cbegin(), definitions.cend(), a)
497 [ + + ]: 98668 : == definitions.cend())
498 : : {
499 : 47664 : assertions.push_back(a);
500 : : }
501 : : }
502 : 5294 : }
503 : :
504 : : } // namespace smt
505 : : } // namespace cvc5::internal
|
