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 : 20225 : PropPfManager::PropPfManager(Env& env,
37 : : CDCLTSatSolver* satSolver,
38 : : CnfStream& cnf,
39 : 20225 : const context::CDList<Node>& assumptions)
40 : : : EnvObj(env),
41 : 20225 : 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 : 40450 : d_proof(
58 : 20225 : env, nullptr, userContext(), "ProofCnfStream::LazyCDProof", false),
59 : 20225 : d_pfpp(new ProofPostprocess(env, &d_proof)),
60 : 20225 : d_pfCnfStream(env, cnf, this),
61 : 20225 : d_plog(nullptr),
62 : 20225 : d_satSolver(satSolver),
63 : 20225 : d_assertions(userContext()),
64 : 20225 : d_cnfStream(cnf),
65 : 20225 : d_assumptions(assumptions),
66 : 20225 : d_inputClauses(userContext()),
67 : 20225 : d_lemmaClauses(userContext()),
68 : 20225 : d_trackLemmaClauseIds(false),
69 : 20225 : d_lemmaClauseIds(userContext()),
70 : 20225 : d_lemmaClauseTimestamp(userContext()),
71 : 20225 : d_currLemmaId(theory::InferenceId::NONE),
72 : 20225 : d_satPm(nullptr),
73 : 20225 : d_uclIds(statisticsRegistry().registerHistogram<theory::InferenceId>(
74 : : "ppm::unsatCoreLemmaIds")),
75 : 20225 : d_uclSize(statisticsRegistry().registerInt("ppm::unsatCoreLemmaSize")),
76 : 60675 : 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 : 20225 : d_assertions.push_back(nodeManager()->mkConst(true));
85 : 20225 : d_trackLemmaClauseIds = isOutputOn(OutputTag::UNSAT_CORE_LEMMAS);
86 : 20225 : }
87 : :
88 : 351416 : void PropPfManager::ensureLiteral(TNode n) { d_pfCnfStream.ensureLiteral(n); }
89 : :
90 : 769581 : void PropPfManager::convertAndAssert(theory::InferenceId id,
91 : : TNode node,
92 : : bool negated,
93 : : bool removable,
94 : : bool input,
95 : : ProofGenerator* pg)
96 : : {
97 : 769581 : d_currLemmaId = id;
98 : 769581 : d_pfCnfStream.convertAndAssert(node, negated, removable, input, pg);
99 : 769581 : d_currLemmaId = theory::InferenceId::NONE;
100 : : // if input, register the assertion in the proof manager
101 [ + + ]: 769581 : if (input)
102 : : {
103 : 191392 : d_assertions.push_back(node);
104 : : }
105 : 769581 : }
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 [ + + ]: 42 : for (const std::shared_ptr<ProofNode>& pf : pfs)
219 : : {
220 : 36 : Node proven = pf->getResult();
221 : 36 : if (std::find(satLeaves.begin(), satLeaves.end(), proven)
222 [ + + ]: 72 : != satLeaves.end())
223 : : {
224 : 12 : usedPfs.push_back(pf);
225 : : }
226 : 36 : }
227 : 12 : return usedPfs;
228 : 6 : }
229 : :
230 : 9692 : std::shared_ptr<ProofNode> PropPfManager::getProof(bool connectCnf)
231 : : {
232 : 9692 : auto it = d_propProofs.find(connectCnf);
233 [ + + ]: 9692 : if (it != d_propProofs.end())
234 : : {
235 : 625 : return it->second;
236 : : }
237 : : // retrieve the SAT solver's refutation proof
238 [ + - ]: 9067 : Trace("sat-proof") << "PropPfManager::getProof: Getting proof of false\n";
239 : :
240 : : // get the proof based on the proof mode
241 : 9067 : options::PropProofMode pmode = options().proof.propProofMode;
242 : 9067 : std::shared_ptr<ProofNode> conflictProof;
243 : : // take proof from SAT solver as is
244 : 9067 : conflictProof = d_satSolver->getProof();
245 : :
246 [ - + ][ - + ]: 9067 : Assert(conflictProof);
[ - - ]
247 [ - + ]: 9067 : if (TraceIsOn("sat-proof"))
248 : : {
249 : 0 : std::vector<Node> fassumps;
250 : 0 : expr::getFreeAssumptions(conflictProof.get(), fassumps);
251 [ - - ]: 0 : Trace("sat-proof")
252 : 0 : << "PropPfManager::getProof: initial free assumptions are:\n";
253 [ - - ]: 0 : for (const Node& a : fassumps)
254 : : {
255 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
256 : : }
257 [ - - ]: 0 : Trace("sat-proof-debug")
258 : 0 : << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
259 [ - - ]: 0 : Trace("sat-proof")
260 : 0 : << "PropPfManager::getProof: Connecting with CNF proof\n";
261 : 0 : }
262 [ + + ]: 9067 : if (!connectCnf)
263 : : {
264 : 449 : d_propProofs[connectCnf] = conflictProof;
265 : 449 : return conflictProof;
266 : : }
267 : : // Must clone if we are using the original proof, since we don't want to
268 : : // modify the original SAT proof. Note that other propProofMode settings
269 : : // may also require cloning here.
270 [ + - ]: 8618 : if (pmode == options::PropProofMode::PROOF)
271 : : {
272 : 8618 : conflictProof = conflictProof->clone();
273 : : }
274 : : // connect it with CNF proof
275 : 8618 : d_pfpp->process(conflictProof);
276 [ - + ]: 8618 : if (TraceIsOn("sat-proof"))
277 : : {
278 : 0 : std::vector<Node> fassumps;
279 : 0 : expr::getFreeAssumptions(conflictProof.get(), fassumps);
280 [ - - ]: 0 : Trace("sat-proof")
281 : 0 : << "PropPfManager::getProof: new free assumptions are:\n";
282 [ - - ]: 0 : for (const Node& a : fassumps)
283 : : {
284 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
285 : : }
286 [ - - ]: 0 : Trace("sat-proof") << "PropPfManager::getProof: assertions are:\n";
287 [ - - ]: 0 : for (const Node& a : d_assertions)
288 : : {
289 [ - - ]: 0 : Trace("sat-proof") << "- " << a << "\n";
290 : : }
291 [ - - ]: 0 : Trace("sat-proof-debug")
292 : 0 : << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
293 : 0 : }
294 : 8618 : d_propProofs[connectCnf] = conflictProof;
295 : 8618 : return conflictProof;
296 : 9067 : }
297 : :
298 : 4059167 : Node PropPfManager::normalizeAndRegister(TNode clauseNode,
299 : : bool input,
300 : : bool doNormalize)
301 : : {
302 : 4059167 : Node normClauseNode = clauseNode;
303 [ + + ]: 4059167 : if (doNormalize)
304 : : {
305 : 3834287 : TheoryProofStepBuffer psb;
306 : 3834287 : normClauseNode = psb.factorReorderElimDoubleNeg(clauseNode);
307 : 3834287 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
308 [ + + ]: 20144055 : for (const std::pair<Node, ProofStep>& step : steps)
309 : : {
310 : 16309768 : d_proof.addStep(step.first, step.second);
311 : : }
312 : 3834287 : }
313 : 4059167 : if (TraceIsOn("cnf") && normClauseNode != clauseNode)
314 : : {
315 [ - - ]: 0 : Trace("cnf") << push
316 : 0 : << "ProofCnfStream::normalizeAndRegister: steps to normalized "
317 : 0 : << normClauseNode << "\n"
318 : 0 : << pop;
319 : : }
320 [ + - ]: 8118334 : Trace("cnf-input") << "New clause: " << normClauseNode << " " << input
321 : 4059167 : << std::endl;
322 [ + + ]: 4059167 : if (input)
323 : : {
324 : 558928 : d_inputClauses.insert(normClauseNode);
325 : : }
326 : : else
327 : : {
328 : 3500239 : d_lemmaClauses.insert(normClauseNode);
329 [ - + ]: 3500239 : if (d_trackLemmaClauseIds)
330 : : {
331 : 0 : d_lemmaClauseIds[normClauseNode] = d_currLemmaId;
332 : 0 : uint64_t currTimestamp = d_env.getResourceManager()->getResource(
333 : 0 : Resource::TheoryFullCheckStep);
334 : 0 : d_lemmaClauseTimestamp[normClauseNode] = currTimestamp;
335 : : }
336 : : }
337 [ + + ]: 4059167 : if (d_satPm)
338 : : {
339 : 8113044 : d_satPm->registerSatAssumptions({normClauseNode});
340 : : }
341 : : // if proof logging, make the call now
342 [ - + ]: 4059167 : if (d_plog != nullptr)
343 : : {
344 [ - - ]: 0 : if (!input)
345 : : {
346 [ - - ]: 0 : if (d_env.isTheoryProofProducing())
347 : : {
348 : : // if theory proof producing, we get the proof to log
349 : 0 : std::shared_ptr<ProofNode> pfn = d_proof.getProofFor(normClauseNode);
350 : 0 : d_plog->logTheoryLemmaProof(pfn);
351 : 0 : }
352 : : else
353 : : {
354 : : // otherwise we just notify the clause
355 : 0 : d_plog->logTheoryLemma(normClauseNode);
356 : : }
357 : : }
358 : : }
359 : 4059167 : return normClauseNode;
360 : 0 : }
361 : :
362 : 26934 : void PropPfManager::presolve()
363 : : {
364 : : // get the proof logger now
365 : 26934 : d_plog = d_env.getProofLogger();
366 [ + - ]: 53868 : Trace("pf-log-debug") << "PropPfManager::presolve, plog="
367 : 26934 : << (d_plog != nullptr) << std::endl;
368 : 26934 : }
369 : :
370 : 22179 : void PropPfManager::logPreprocessing()
371 : : {
372 [ - + ]: 22179 : if (d_plog != nullptr)
373 : : {
374 : : // TODO (wishues #157): in incremental mode, only get the new assertions
375 : 0 : std::vector<std::shared_ptr<ProofNode>> icp = getInputClausesProofs();
376 [ - - ]: 0 : for (const Node& a : d_assumptions)
377 : : {
378 : 0 : icp.emplace_back(d_proof.getProofFor(a));
379 : : }
380 [ - - ]: 0 : Trace("pf-log-debug") << "PropPfManager::presolve, we have "
381 : 0 : << d_inputClauses.size() << " inputs and "
382 : 0 : << d_assumptions.size() << " assumptions"
383 : 0 : << std::endl;
384 : 0 : d_plog->logCnfPreprocessInputProofs(icp);
385 : 0 : }
386 : 22179 : }
387 : :
388 : 21867 : void PropPfManager::postsolve(SatValue result)
389 : : {
390 [ - + ]: 21867 : if (d_plog != nullptr)
391 : : {
392 [ - - ]: 0 : if (result == SAT_VALUE_FALSE)
393 : : {
394 [ - - ]: 0 : if (d_env.isSatProofProducing())
395 : : {
396 : : // if SAT proof producing, log the proof
397 : 0 : std::shared_ptr<ProofNode> satPf = getProof(true);
398 : 0 : d_plog->logSatRefutationProof(satPf);
399 : 0 : }
400 : : else
401 : : {
402 : : // otherwise just mark the refutation
403 : 0 : d_plog->logSatRefutation();
404 : : }
405 : : }
406 : : }
407 : 21867 : }
408 : :
409 : 246162 : LazyCDProof* PropPfManager::getCnfProof() { return &d_proof; }
410 : :
411 : 0 : std::vector<Node> PropPfManager::getInputClauses()
412 : : {
413 : 0 : std::vector<Node> cls;
414 [ - - ]: 0 : for (const Node& c : d_inputClauses)
415 : : {
416 : 0 : cls.push_back(c);
417 : 0 : }
418 : 0 : return cls;
419 : 0 : }
420 : :
421 : 458 : std::vector<Node> PropPfManager::getLemmaClauses()
422 : : {
423 : 458 : std::vector<Node> cls;
424 [ + + ]: 689 : for (const Node& c : d_lemmaClauses)
425 : : {
426 : 231 : cls.push_back(c);
427 : 231 : }
428 : 458 : return cls;
429 : 0 : }
430 : :
431 : 3 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getInputClausesProofs()
432 : : {
433 : 3 : std::vector<std::shared_ptr<ProofNode>> pfs;
434 [ + + ]: 39 : for (const Node& a : d_inputClauses)
435 : : {
436 : 36 : pfs.push_back(d_proof.getProofFor(a));
437 : 36 : }
438 : 3 : return pfs;
439 : 0 : }
440 : :
441 : 3 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getLemmaClausesProofs()
442 : : {
443 : 3 : std::vector<std::shared_ptr<ProofNode>> pfs;
444 [ - + ]: 3 : for (const Node& a : d_lemmaClauses)
445 : : {
446 : 0 : pfs.push_back(d_proof.getProofFor(a));
447 : 0 : }
448 : 3 : return pfs;
449 : 0 : }
450 : :
451 : 158320 : void PropPfManager::notifyExplainedPropagation(TrustNode trn)
452 : : {
453 : 158320 : Node proven = trn.getProven();
454 : : // If we are not producing proofs in the theory engine there is no need to
455 : : // keep track in d_proof of the clausification. We still need however to let
456 : : // the SAT proof manager know that this clause is an assumption.
457 : 158320 : bool proofLogging = trn.getGenerator() != nullptr;
458 [ + - ]: 316640 : Trace("cnf")
459 : 0 : << "PropPfManager::notifyExplainedPropagation: proven explanation"
460 : 158320 : << proven << ", proofLogging=" << proofLogging << "\n";
461 [ + + ]: 158320 : if (proofLogging)
462 : : {
463 [ - + ][ - + ]: 110172 : Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
[ - - ]
464 [ + - ]: 220344 : Trace("cnf-steps") << proven << " by explainPropagation "
465 [ - + ][ - - ]: 110172 : << trn.identifyGenerator() << std::endl;
466 : 110172 : d_proof.addLazyStep(proven,
467 : : trn.getGenerator(),
468 : : TrustId::NONE,
469 : : true,
470 : : "PropPfManager::notifyExplainedPropagation");
471 : : }
472 : : // since the propagation is added directly to the SAT solver via theoryProxy,
473 : : // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
474 : 158320 : NodeManager* nm = nodeManager();
475 : 158320 : Node clauseImpliesElim;
476 [ + + ]: 158320 : if (proofLogging)
477 : : {
478 : 110172 : clauseImpliesElim = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
479 [ + - ]: 220344 : Trace("cnf") << "PropPfManager::notifyExplainedPropagation: adding "
480 : 110172 : << ProofRule::IMPLIES_ELIM << " rule to conclude "
481 : 110172 : << clauseImpliesElim << "\n";
482 : 220344 : d_proof.addStep(clauseImpliesElim, ProofRule::IMPLIES_ELIM, {proven}, {});
483 : : }
484 : 158320 : Node clauseExp;
485 : : // need to eliminate AND
486 [ + + ]: 158320 : if (proven[0].getKind() == Kind::AND)
487 : : {
488 : 451557 : std::vector<Node> disjunctsAndNeg{proven[0]};
489 : 150519 : std::vector<Node> disjunctsRes;
490 [ + + ]: 1679149 : for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i)
491 : : {
492 : 1528630 : disjunctsAndNeg.push_back(proven[0][i].notNode());
493 : 1528630 : disjunctsRes.push_back(proven[0][i].notNode());
494 : : }
495 : 150519 : disjunctsRes.push_back(proven[1]);
496 : 150519 : clauseExp = nm->mkNode(Kind::OR, disjunctsRes);
497 [ + + ]: 150519 : if (proofLogging)
498 : : {
499 : : // add proof steps to convert into clause
500 : 104983 : Node clauseAndNeg = nm->mkNode(Kind::OR, disjunctsAndNeg);
501 : 209966 : d_proof.addStep(clauseAndNeg, ProofRule::CNF_AND_NEG, {}, {proven[0]});
502 : 524915 : d_proof.addStep(clauseExp,
503 : : ProofRule::RESOLUTION,
504 : : {clauseAndNeg, clauseImpliesElim},
505 : 104983 : {nm->mkConst(true), proven[0]});
506 : 104983 : }
507 : 150519 : }
508 : : else
509 : : {
510 : 7801 : clauseExp = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
511 : : }
512 : 158320 : d_currPropagationProcessed = normalizeAndRegister(clauseExp, false);
513 : : // If we are not logging the clausification, we need to add the clause, as *it
514 : : // will be saved in the SAT solver* (i.e., as clauseExp), as closed step in
515 : : // the d_proof, so that there are no non-input assumptions.
516 [ + + ]: 158320 : if (!proofLogging)
517 : : {
518 : 48148 : d_proof.addTrustedStep(clauseExp, TrustId::THEORY_LEMMA, {}, {});
519 : : }
520 : 158320 : }
521 : :
522 : 83 : Node PropPfManager::getLastExplainedPropagation() const
523 : : {
524 : 83 : return d_currPropagationProcessed;
525 : : }
526 : :
527 : 83 : void PropPfManager::resetLastExplainedPropagation()
528 : : {
529 : 83 : d_currPropagationProcessed = Node::null();
530 : 83 : }
531 : :
532 : : } // namespace prop
533 : : } // namespace cvc5::internal
|
