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 : : * Implementation of the proof manager for the PropPfManager.
11 : : */
12 : :
13 : : #include "prop/prop_proof_manager.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "options/base_options.h"
17 : : #include "options/main_options.h"
18 : : #include "printer/printer.h"
19 : : #include "proof/proof_ensure_closed.h"
20 : : #include "proof/proof_node_algorithm.h"
21 : : #include "proof/theory_proof_step_buffer.h"
22 : : #include "prop/cnf_stream.h"
23 : : #include "prop/minisat/sat_proof_manager.h"
24 : : #include "prop/prop_proof_manager.h"
25 : : #include "prop/sat_solver.h"
26 : : #include "prop/sat_solver_factory.h"
27 : : #include "smt/env.h"
28 : : #include "smt/logic_exception.h"
29 : : #include "smt/proof_logger.h"
30 : : #include "util/resource_manager.h"
31 : : #include "util/string.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace prop {
35 : :
36 : 20037 : PropPfManager::PropPfManager(Env& env,
37 : : CDCLTSatSolver* satSolver,
38 : : CnfStream& cnf,
39 : 20037 : const context::CDList<Node>& assumptions)
40 : : : EnvObj(env),
41 : 20037 : d_propProofs(userContext()),
42 : : // Since the ProofCnfStream performs no equality reasoning, there is no
43 : : // need to automatically add symmetry steps. Note that it is *safer* to
44 : : // forbid this, since adding symmetry steps when proof nodes are being
45 : : // updated may inadvertently generate cyclic proofs.
46 : : //
47 : : // This can happen for example if the proof cnf stream has a generator for
48 : : // (= a b), whose proof depends on symmetry applied to (= b a). It does
49 : : // not have a generator for (= b a). However if asked for a proof of the
50 : : // fact (= b a) (after having expanded the proof of (= a b)), since it has
51 : : // no generator for (= b a), a proof (= b a) can be generated via symmetry
52 : : // on the proof of (= a b). As a result, the assumption (= b a) would be
53 : : // assigned a proof with assumption (= b a). This breaks the invariant of
54 : : // the proof node manager of no cyclic proofs if the ASSUMPTION proof node
55 : : // of both the assumption (= b a) we are asking the proof for and the
56 : : // assumption (= b a) in the proof of (= a b) are the same.
57 : 40074 : d_proof(
58 : 20037 : env, nullptr, userContext(), "ProofCnfStream::LazyCDProof", false),
59 : 20037 : d_pfpp(new ProofPostprocess(env, &d_proof)),
60 : 20037 : d_pfCnfStream(env, cnf, this),
61 : 20037 : d_plog(nullptr),
62 : 20037 : d_satSolver(satSolver),
63 : 20037 : d_assertions(userContext()),
64 : 20037 : d_cnfStream(cnf),
65 : 20037 : d_assumptions(assumptions),
66 : 20037 : d_inputClauses(userContext()),
67 : 20037 : d_lemmaClauses(userContext()),
68 : 20037 : d_trackLemmaClauseIds(false),
69 : 20037 : d_lemmaClauseIds(userContext()),
70 : 20037 : d_lemmaClauseTimestamp(userContext()),
71 : 20037 : d_currLemmaId(theory::InferenceId::NONE),
72 : 20037 : d_satPm(nullptr),
73 : 20037 : d_uclIds(statisticsRegistry().registerHistogram<theory::InferenceId>(
74 : : "ppm::unsatCoreLemmaIds")),
75 : 20037 : d_uclSize(statisticsRegistry().registerInt("ppm::unsatCoreLemmaSize")),
76 : 60111 : d_numUcl(statisticsRegistry().registerInt("ppm::unsatCoreLemmaCalls"))
77 : : {
78 : : // Add trivial assumption. This is so that we can check that the prop engine's
79 : : // proof is closed, as the SAT solver's refutation proof may use True as an
80 : : // assumption even when True is not given as an assumption. An example is when
81 : : // a propagated literal has an empty explanation (i.e., it is a valid
82 : : // literal), which leads to adding True as its explanation, since for creating
83 : : // a learned clause we need at least two literals.
84 : 20037 : d_assertions.push_back(nodeManager()->mkConst(true));
85 : 20037 : d_trackLemmaClauseIds = isOutputOn(OutputTag::UNSAT_CORE_LEMMAS);
86 : 20037 : }
87 : :
88 : 345649 : void PropPfManager::ensureLiteral(TNode n) { d_pfCnfStream.ensureLiteral(n); }
89 : :
90 : 766191 : void PropPfManager::convertAndAssert(theory::InferenceId id,
91 : : TNode node,
92 : : bool negated,
93 : : bool removable,
94 : : bool input,
95 : : ProofGenerator* pg)
96 : : {
97 : 766191 : d_currLemmaId = id;
98 : 766191 : d_pfCnfStream.convertAndAssert(node, negated, removable, input, pg);
99 : 766191 : d_currLemmaId = theory::InferenceId::NONE;
100 : : // if input, register the assertion in the proof manager
101 [ + + ]: 766191 : if (input)
102 : : {
103 : 190279 : d_assertions.push_back(node);
104 : : }
105 : 766191 : }
106 : :
107 : 0 : void PropPfManager::registerAssertion(Node assertion)
108 : : {
109 : 0 : d_assertions.push_back(assertion);
110 : 0 : }
111 : :
112 : 7 : void PropPfManager::checkProof(const context::CDList<Node>& assertions)
113 : : {
114 [ + - ]: 14 : Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
115 : 7 : "proof of false is closed\n";
116 : 7 : std::shared_ptr<ProofNode> conflictProof = getProof(false);
117 [ - + ][ - + ]: 7 : Assert(conflictProof);
[ - - ]
118 : : // connect it with CNF proof
119 : 7 : d_pfpp->process(conflictProof);
120 : : // add given assertions d_assertions
121 [ + + ]: 19 : for (const Node& assertion : assertions)
122 : : {
123 : 12 : d_assertions.push_back(assertion);
124 : : }
125 : 7 : std::vector<Node> avec{d_assertions.begin(), d_assertions.end()};
126 : 7 : pfnEnsureClosedWrt(options(),
127 : : conflictProof.get(),
128 : : avec,
129 : : "sat-proof",
130 : : "PropPfManager::checkProof");
131 : 7 : }
132 : :
133 : 458 : std::vector<Node> PropPfManager::getUnsatCoreLemmas()
134 : : {
135 : 458 : std::vector<Node> usedLemmas;
136 : 458 : std::vector<Node> allLemmas = getLemmaClauses();
137 : : // compute the unsat core clauses, as below
138 : 458 : std::vector<Node> ucc = getUnsatCoreClauses();
139 [ + - ]: 916 : Trace("prop-pf") << "Compute unsat core lemmas from " << ucc.size()
140 : 458 : << " clauses (of " << allLemmas.size() << " lemmas)"
141 : 458 : << std::endl;
142 [ + - ]: 458 : Trace("prop-pf") << "lemmas: " << allLemmas << std::endl;
143 [ + - ]: 458 : Trace("prop-pf") << "uc: " << ucc << std::endl;
144 : : // filter to only those corresponding to lemmas
145 [ + + ]: 689 : for (const Node& lemma : allLemmas)
146 : : {
147 [ + - ]: 231 : if (std::find(ucc.begin(), ucc.end(), lemma) != ucc.end())
148 : : {
149 : 231 : usedLemmas.push_back(lemma);
150 : : }
151 : : }
152 [ - + ]: 458 : if (d_trackLemmaClauseIds)
153 : : {
154 : 0 : ++d_numUcl;
155 : : uint64_t timestamp;
156 [ - - ]: 0 : for (const Node& lemma : usedLemmas)
157 : : {
158 : 0 : d_uclIds << getInferenceIdFor(lemma, timestamp);
159 : 0 : ++d_uclSize;
160 : : }
161 : : }
162 : 916 : return usedLemmas;
163 : 458 : }
164 : :
165 : 0 : theory::InferenceId PropPfManager::getInferenceIdFor(const Node& lem,
166 : : uint64_t& timestamp) const
167 : : {
168 : : context::CDHashMap<Node, theory::InferenceId>::const_iterator it =
169 : 0 : d_lemmaClauseIds.find(lem);
170 [ - - ]: 0 : if (it != d_lemmaClauseIds.end())
171 : : {
172 : : context::CDHashMap<Node, uint64_t>::const_iterator itt =
173 : 0 : d_lemmaClauseTimestamp.find(lem);
174 [ - - ]: 0 : if (itt != d_lemmaClauseTimestamp.end())
175 : : {
176 : 0 : timestamp = itt->second;
177 : : }
178 : 0 : return it->second;
179 : : }
180 : 0 : return theory::InferenceId::NONE;
181 : : }
182 : 458 : std::vector<Node> PropPfManager::getUnsatCoreClauses()
183 : : {
184 : 458 : std::vector<Node> uc;
185 : : // if it has a proof
186 : 458 : std::shared_ptr<ProofNode> satPf = d_satSolver->getProof();
187 : : // Note that we currently assume that the proof is the standard way of
188 : : // communicating the unsat core of theory lemmas. If no proofs are
189 : : // available, then a trust step (e.g. SAT_REFUTATION) with free assumptions
190 : : // F1 ... Fn can be used to indicate that F1 ... Fn is the unsat core
191 [ - + ]: 458 : if (satPf == nullptr)
192 : : {
193 : 0 : std::stringstream ss;
194 : : ss << "ERROR: cannot get unsat core clauses when SAT solver is not proof "
195 : 0 : "producing.";
196 : 0 : throw LogicException(ss.str());
197 : 0 : }
198 : : // then, get the proof *without* connecting the CNF
199 : 458 : expr::getFreeAssumptions(satPf.get(), uc);
200 : 916 : return uc;
201 : 458 : }
202 : :
203 : 6 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getProofLeaves(
204 : : modes::ProofComponent pc)
205 : : {
206 [ + - ]: 12 : Trace("sat-proof") << "PropPfManager::getProofLeaves: Getting " << pc
207 : 6 : << " component proofs\n";
208 : 6 : std::vector<Node> fassumps;
209 [ + + ][ + - ]: 6 : Assert(pc == modes::ProofComponent::THEORY_LEMMAS
[ - + ][ - + ]
[ - - ]
210 : : || pc == modes::ProofComponent::PREPROCESS);
211 : : std::vector<std::shared_ptr<ProofNode>> pfs =
212 : 6 : pc == modes::ProofComponent::THEORY_LEMMAS ? getLemmaClausesProofs()
213 [ + + ]: 6 : : getInputClausesProofs();
214 : 6 : std::shared_ptr<ProofNode> satPf = getProof(false);
215 : 6 : std::vector<Node> satLeaves;
216 : 6 : expr::getFreeAssumptions(satPf.get(), satLeaves);
217 : 6 : std::vector<std::shared_ptr<ProofNode>> usedPfs;
218 [ + + ]: 33 : for (const std::shared_ptr<ProofNode>& pf : pfs)
219 : : {
220 : 27 : Node proven = pf->getResult();
221 [ + + ]: 27 : if (std::find(satLeaves.begin(), satLeaves.end(), proven) != satLeaves.end())
222 : : {
223 : 12 : usedPfs.push_back(pf);
224 : : }
225 : 27 : }
226 : 12 : return usedPfs;
227 : 6 : }
228 : :
229 : 9545 : std::shared_ptr<ProofNode> PropPfManager::getProof(bool connectCnf)
230 : : {
231 : 9545 : auto it = d_propProofs.find(connectCnf);
232 [ + + ]: 9545 : if (it != d_propProofs.end())
233 : : {
234 : 585 : return it->second;
235 : : }
236 : : // retrieve the SAT solver's refutation proof
237 [ + - ]: 8960 : Trace("sat-proof") << "PropPfManager::getProof: Getting proof of false\n";
238 : :
239 : : // get the proof based on the proof mode
240 : 8960 : options::PropProofMode pmode = options().proof.propProofMode;
241 : 8960 : std::shared_ptr<ProofNode> conflictProof;
242 : : // take proof from SAT solver as is
243 : 8960 : conflictProof = d_satSolver->getProof();
244 : :
245 [ - + ][ - + ]: 8960 : Assert(conflictProof);
[ - - ]
246 [ - + ]: 8960 : if (TraceIsOn("sat-proof"))
247 : : {
248 : 0 : std::vector<Node> fassumps;
249 : 0 : expr::getFreeAssumptions(conflictProof.get(), fassumps);
250 [ - - ]: 0 : Trace("sat-proof")
251 : 0 : << "PropPfManager::getProof: initial free assumptions are:\n";
252 [ - - ]: 0 : for (const Node& a : fassumps)
253 : : {
254 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
255 : : }
256 [ - - ]: 0 : Trace("sat-proof-debug")
257 : 0 : << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
258 [ - - ]: 0 : Trace("sat-proof")
259 : 0 : << "PropPfManager::getProof: Connecting with CNF proof\n";
260 : 0 : }
261 [ + + ]: 8960 : if (!connectCnf)
262 : : {
263 : 449 : d_propProofs[connectCnf] = conflictProof;
264 : 449 : return conflictProof;
265 : : }
266 : : // Must clone if we are using the original proof, since we don't want to
267 : : // modify the original SAT proof. Note that other propProofMode settings
268 : : // may also require cloning here.
269 [ + - ]: 8511 : if (pmode == options::PropProofMode::PROOF)
270 : : {
271 : 8511 : conflictProof = conflictProof->clone();
272 : : }
273 : : // connect it with CNF proof
274 : 8511 : d_pfpp->process(conflictProof);
275 [ - + ]: 8511 : if (TraceIsOn("sat-proof"))
276 : : {
277 : 0 : std::vector<Node> fassumps;
278 : 0 : expr::getFreeAssumptions(conflictProof.get(), fassumps);
279 [ - - ]: 0 : Trace("sat-proof")
280 : 0 : << "PropPfManager::getProof: new free assumptions are:\n";
281 [ - - ]: 0 : for (const Node& a : fassumps)
282 : : {
283 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
284 : : }
285 [ - - ]: 0 : Trace("sat-proof") << "PropPfManager::getProof: assertions are:\n";
286 [ - - ]: 0 : for (const Node& a : d_assertions)
287 : : {
288 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
289 : : }
290 [ - - ]: 0 : Trace("sat-proof-debug")
291 : 0 : << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
292 : 0 : }
293 : 8511 : d_propProofs[connectCnf] = conflictProof;
294 : 8511 : return conflictProof;
295 : 8960 : }
296 : :
297 : 3859046 : Node PropPfManager::normalizeAndRegister(TNode clauseNode,
298 : : bool input,
299 : : bool doNormalize)
300 : : {
301 : 3859046 : Node normClauseNode = clauseNode;
302 [ + + ]: 3859046 : if (doNormalize)
303 : : {
304 : 3718466 : TheoryProofStepBuffer psb;
305 : 3718466 : normClauseNode = psb.factorReorderElimDoubleNeg(clauseNode);
306 : 3718466 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
307 [ + + ]: 19598069 : for (const std::pair<Node, ProofStep>& step : steps)
308 : : {
309 : 15879603 : d_proof.addStep(step.first, step.second);
310 : : }
311 : 3718466 : }
312 : 3859046 : if (TraceIsOn("cnf") && normClauseNode != clauseNode)
313 : : {
314 [ - - ]: 0 : Trace("cnf") << push
315 : 0 : << "ProofCnfStream::normalizeAndRegister: steps to normalized "
316 : 0 : << normClauseNode << "\n"
317 : 0 : << pop;
318 : : }
319 [ + - ]: 7718092 : Trace("cnf-input") << "New clause: " << normClauseNode << " " << input
320 : 3859046 : << std::endl;
321 [ + + ]: 3859046 : if (input)
322 : : {
323 : 483111 : d_inputClauses.insert(normClauseNode);
324 : : }
325 : : else
326 : : {
327 : 3375935 : d_lemmaClauses.insert(normClauseNode);
328 [ - + ]: 3375935 : if (d_trackLemmaClauseIds)
329 : : {
330 : 0 : d_lemmaClauseIds[normClauseNode] = d_currLemmaId;
331 : 0 : uint64_t currTimestamp = d_env.getResourceManager()->getResource(
332 : 0 : Resource::TheoryFullCheckStep);
333 : 0 : d_lemmaClauseTimestamp[normClauseNode] = currTimestamp;
334 : : }
335 : : }
336 [ + + ]: 3859046 : if (d_satPm)
337 : : {
338 : 7717854 : d_satPm->registerSatAssumptions({normClauseNode});
339 : : }
340 : : // if proof logging, make the call now
341 [ - + ]: 3859046 : if (d_plog != nullptr)
342 : : {
343 [ - - ]: 0 : if (!input)
344 : : {
345 [ - - ]: 0 : if (d_env.isTheoryProofProducing())
346 : : {
347 : : // if theory proof producing, we get the proof to log
348 : 0 : std::shared_ptr<ProofNode> pfn = d_proof.getProofFor(normClauseNode);
349 : 0 : d_plog->logTheoryLemmaProof(pfn);
350 : 0 : }
351 : : else
352 : : {
353 : : // otherwise we just notify the clause
354 : 0 : d_plog->logTheoryLemma(normClauseNode);
355 : : }
356 : : }
357 : : }
358 : 3859046 : return normClauseNode;
359 : 0 : }
360 : :
361 : 26742 : void PropPfManager::presolve()
362 : : {
363 : : // get the proof logger now
364 : 26742 : d_plog = d_env.getProofLogger();
365 [ + - ]: 53484 : Trace("pf-log-debug") << "PropPfManager::presolve, plog="
366 : 26742 : << (d_plog != nullptr) << std::endl;
367 : 26742 : }
368 : :
369 : 21997 : void PropPfManager::logPreprocessing()
370 : : {
371 [ - + ]: 21997 : if (d_plog != nullptr)
372 : : {
373 : : // TODO (wishues #157): in incremental mode, only get the new assertions
374 : 0 : std::vector<std::shared_ptr<ProofNode>> icp = getInputClausesProofs();
375 [ - - ]: 0 : for (const Node& a : d_assumptions)
376 : : {
377 : 0 : icp.emplace_back(d_proof.getProofFor(a));
378 : : }
379 [ - - ]: 0 : Trace("pf-log-debug") << "PropPfManager::presolve, we have "
380 : 0 : << d_inputClauses.size() << " inputs and "
381 : 0 : << d_assumptions.size() << " assumptions"
382 : 0 : << std::endl;
383 : 0 : d_plog->logCnfPreprocessInputProofs(icp);
384 : 0 : }
385 : 21997 : }
386 : :
387 : 21649 : void PropPfManager::postsolve(SatValue result)
388 : : {
389 [ - + ]: 21649 : if (d_plog != nullptr)
390 : : {
391 [ - - ]: 0 : if (result == SAT_VALUE_FALSE)
392 : : {
393 [ - - ]: 0 : if (d_env.isSatProofProducing())
394 : : {
395 : : // if SAT proof producing, log the proof
396 : 0 : std::shared_ptr<ProofNode> satPf = getProof(true);
397 : 0 : d_plog->logSatRefutationProof(satPf);
398 : 0 : }
399 : : else
400 : : {
401 : : // otherwise just mark the refutation
402 : 0 : d_plog->logSatRefutation();
403 : : }
404 : : }
405 : : }
406 : 21649 : }
407 : :
408 : 250354 : LazyCDProof* PropPfManager::getCnfProof() { return &d_proof; }
409 : :
410 : 0 : std::vector<Node> PropPfManager::getInputClauses()
411 : : {
412 : 0 : std::vector<Node> cls;
413 [ - - ]: 0 : for (const Node& c : d_inputClauses)
414 : : {
415 : 0 : cls.push_back(c);
416 : 0 : }
417 : 0 : return cls;
418 : 0 : }
419 : :
420 : 458 : std::vector<Node> PropPfManager::getLemmaClauses()
421 : : {
422 : 458 : std::vector<Node> cls;
423 [ + + ]: 689 : for (const Node& c : d_lemmaClauses)
424 : : {
425 : 231 : cls.push_back(c);
426 : 231 : }
427 : 458 : return cls;
428 : 0 : }
429 : :
430 : 3 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getInputClausesProofs()
431 : : {
432 : 3 : std::vector<std::shared_ptr<ProofNode>> pfs;
433 [ + + ]: 30 : for (const Node& a : d_inputClauses)
434 : : {
435 : 27 : pfs.push_back(d_proof.getProofFor(a));
436 : 27 : }
437 : 3 : return pfs;
438 : 0 : }
439 : :
440 : 3 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getLemmaClausesProofs()
441 : : {
442 : 3 : std::vector<std::shared_ptr<ProofNode>> pfs;
443 [ - + ]: 3 : for (const Node& a : d_lemmaClauses)
444 : : {
445 : 0 : pfs.push_back(d_proof.getProofFor(a));
446 : 0 : }
447 : 3 : return pfs;
448 : 0 : }
449 : :
450 : 155831 : void PropPfManager::notifyExplainedPropagation(TrustNode trn)
451 : : {
452 : 155831 : Node proven = trn.getProven();
453 : : // If we are not producing proofs in the theory engine there is no need to
454 : : // keep track in d_proof of the clausification. We still need however to let
455 : : // the SAT proof manager know that this clause is an assumption.
456 : 155831 : bool proofLogging = trn.getGenerator() != nullptr;
457 [ + - ]: 311662 : Trace("cnf")
458 : 0 : << "PropPfManager::notifyExplainedPropagation: proven explanation"
459 : 155831 : << proven << ", proofLogging=" << proofLogging << "\n";
460 [ + + ]: 155831 : if (proofLogging)
461 : : {
462 [ - + ][ - + ]: 108526 : Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
[ - - ]
463 [ + - ]: 217052 : Trace("cnf-steps") << proven << " by explainPropagation "
464 [ - + ][ - - ]: 108526 : << trn.identifyGenerator() << std::endl;
465 : 108526 : d_proof.addLazyStep(proven,
466 : : trn.getGenerator(),
467 : : TrustId::NONE,
468 : : true,
469 : : "PropPfManager::notifyExplainedPropagation");
470 : : }
471 : : // since the propagation is added directly to the SAT solver via theoryProxy,
472 : : // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
473 : 155831 : NodeManager* nm = nodeManager();
474 : 155831 : Node clauseImpliesElim;
475 [ + + ]: 155831 : if (proofLogging)
476 : : {
477 : 108526 : clauseImpliesElim = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
478 [ + - ]: 217052 : Trace("cnf") << "PropPfManager::notifyExplainedPropagation: adding "
479 : 108526 : << ProofRule::IMPLIES_ELIM << " rule to conclude "
480 : 108526 : << clauseImpliesElim << "\n";
481 : 217052 : d_proof.addStep(clauseImpliesElim, ProofRule::IMPLIES_ELIM, {proven}, {});
482 : : }
483 : 155831 : Node clauseExp;
484 : : // need to eliminate AND
485 [ + + ]: 155831 : if (proven[0].getKind() == Kind::AND)
486 : : {
487 : 444417 : std::vector<Node> disjunctsAndNeg{proven[0]};
488 : 148139 : std::vector<Node> disjunctsRes;
489 [ + + ]: 1659070 : for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i)
490 : : {
491 : 1510931 : disjunctsAndNeg.push_back(proven[0][i].notNode());
492 : 1510931 : disjunctsRes.push_back(proven[0][i].notNode());
493 : : }
494 : 148139 : disjunctsRes.push_back(proven[1]);
495 : 148139 : clauseExp = nm->mkNode(Kind::OR, disjunctsRes);
496 [ + + ]: 148139 : if (proofLogging)
497 : : {
498 : : // add proof steps to convert into clause
499 : 103446 : Node clauseAndNeg = nm->mkNode(Kind::OR, disjunctsAndNeg);
500 : 206892 : d_proof.addStep(clauseAndNeg, ProofRule::CNF_AND_NEG, {}, {proven[0]});
501 : 517230 : d_proof.addStep(clauseExp,
502 : : ProofRule::RESOLUTION,
503 : : {clauseAndNeg, clauseImpliesElim},
504 : 103446 : {nm->mkConst(true), proven[0]});
505 : 103446 : }
506 : 148139 : }
507 : : else
508 : : {
509 : 7692 : clauseExp = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
510 : : }
511 : 155831 : d_currPropagationProcessed = normalizeAndRegister(clauseExp, false);
512 : : // If we are not logging the clausification, we need to add the clause, as *it
513 : : // will be saved in the SAT solver* (i.e., as clauseExp), as closed step in
514 : : // the d_proof, so that there are no non-input assumptions.
515 [ + + ]: 155831 : if (!proofLogging)
516 : : {
517 : 47305 : d_proof.addTrustedStep(clauseExp, TrustId::THEORY_LEMMA, {}, {});
518 : : }
519 : 155831 : }
520 : :
521 : 83 : Node PropPfManager::getLastExplainedPropagation() const
522 : : {
523 : 83 : return d_currPropagationProcessed;
524 : : }
525 : :
526 : 83 : void PropPfManager::resetLastExplainedPropagation()
527 : : {
528 : 83 : d_currPropagationProcessed = Node::null();
529 : 83 : }
530 : :
531 : : } // namespace prop
532 : : } // namespace cvc5::internal
|
