Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Andrew Reynolds, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of the proof manager for the PropPfManager.
14 : : */
15 : :
16 : : #include "prop/prop_proof_manager.h"
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "options/base_options.h"
20 : : #include "options/main_options.h"
21 : : #include "printer/printer.h"
22 : : #include "proof/proof_ensure_closed.h"
23 : : #include "proof/proof_node_algorithm.h"
24 : : #include "proof/theory_proof_step_buffer.h"
25 : : #include "prop/cnf_stream.h"
26 : : #include "prop/minisat/sat_proof_manager.h"
27 : : #include "prop/prop_proof_manager.h"
28 : : #include "prop/sat_solver.h"
29 : : #include "prop/sat_solver_factory.h"
30 : : #include "smt/env.h"
31 : : #include "smt/logic_exception.h"
32 : : #include "util/resource_manager.h"
33 : : #include "util/string.h"
34 : :
35 : : namespace cvc5::internal {
36 : : namespace prop {
37 : :
38 : 10845 : PropPfManager::PropPfManager(Env& env,
39 : : CDCLTSatSolver* satSolver,
40 : : CnfStream& cnf,
41 : 10845 : const context::CDList<Node>& assumptions)
42 : : : EnvObj(env),
43 : 21690 : d_propProofs(userContext()),
44 : : // Since the ProofCnfStream performs no equality reasoning, there is no
45 : : // need to automatically add symmetry steps. Note that it is *safer* to
46 : : // forbid this, since adding symmetry steps when proof nodes are being
47 : : // updated may inadvertently generate cyclic proofs.
48 : : //
49 : : // This can happen for example if the proof cnf stream has a generator for
50 : : // (= a b), whose proof depends on symmetry applied to (= b a). It does
51 : : // not have a generator for (= b a). However if asked for a proof of the
52 : : // fact (= b a) (after having expanded the proof of (= a b)), since it has
53 : : // no generator for (= b a), a proof (= b a) can be generated via symmetry
54 : : // on the proof of (= a b). As a result, the assumption (= b a) would be
55 : : // assigned a proof with assumption (= b a). This breaks the invariant of
56 : : // the proof node manager of no cyclic proofs if the ASSUMPTION proof node
57 : : // of both the assumption (= b a) we are asking the proof for and the
58 : : // assumption (= b a) in the proof of (= a b) are the same.
59 : : d_proof(
60 : 10845 : env, nullptr, userContext(), "ProofCnfStream::LazyCDProof", false),
61 : 10845 : d_pfpp(new ProofPostprocess(env, &d_proof)),
62 : : d_pfCnfStream(env, cnf, this),
63 : : d_satSolver(satSolver),
64 : 21690 : d_assertions(userContext()),
65 : : d_cnfStream(cnf),
66 : : d_assumptions(assumptions),
67 : 21690 : d_inputClauses(userContext()),
68 : 21690 : d_lemmaClauses(userContext()),
69 : : d_trackLemmaClauseIds(false),
70 : 21690 : d_lemmaClauseIds(userContext()),
71 : 21690 : d_lemmaClauseTimestamp(userContext()),
72 : : d_currLemmaId(theory::InferenceId::NONE),
73 : : d_satPm(nullptr),
74 : 21690 : d_uclIds(statisticsRegistry().registerHistogram<theory::InferenceId>(
75 : 10845 : "ppm::unsatCoreLemmaIds")),
76 : 10845 : d_uclSize(statisticsRegistry().registerInt("ppm::unsatCoreLemmaSize")),
77 : 43380 : d_numUcl(statisticsRegistry().registerInt("ppm::unsatCoreLemmaCalls"))
78 : : {
79 : : // Add trivial assumption. This is so that we can check that the prop engine's
80 : : // proof is closed, as the SAT solver's refutation proof may use True as an
81 : : // assumption even when True is not given as an assumption. An example is when
82 : : // a propagated literal has an empty explanation (i.e., it is a valid
83 : : // literal), which leads to adding True as its explanation, since for creating
84 : : // a learned clause we need at least two literals.
85 : 10845 : d_assertions.push_back(nodeManager()->mkConst(true));
86 : 10845 : d_trackLemmaClauseIds = isOutputOn(OutputTag::UNSAT_CORE_LEMMAS);
87 : 10845 : }
88 : :
89 : 146909 : void PropPfManager::ensureLiteral(TNode n) { d_pfCnfStream.ensureLiteral(n); }
90 : :
91 : 583830 : void PropPfManager::convertAndAssert(theory::InferenceId id,
92 : : TNode node,
93 : : bool negated,
94 : : bool removable,
95 : : bool input,
96 : : ProofGenerator* pg)
97 : : {
98 : 583830 : d_currLemmaId = id;
99 : 583830 : d_pfCnfStream.convertAndAssert(node, negated, removable, input, pg);
100 : 583830 : d_currLemmaId = theory::InferenceId::NONE;
101 : : // if input, register the assertion in the proof manager
102 [ + + ]: 583830 : if (input)
103 : : {
104 : 219228 : d_assertions.push_back(node);
105 : : }
106 : 583830 : }
107 : :
108 : 0 : void PropPfManager::registerAssertion(Node assertion)
109 : : {
110 : 0 : d_assertions.push_back(assertion);
111 : 0 : }
112 : :
113 : 14 : void PropPfManager::checkProof(const context::CDList<Node>& assertions)
114 : : {
115 [ + - ]: 28 : Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
116 : 14 : "proof of false is closed\n";
117 : 28 : std::shared_ptr<ProofNode> conflictProof = getProof(false);
118 [ - + ][ - + ]: 14 : Assert(conflictProof);
[ - - ]
119 : : // connect it with CNF proof
120 : 14 : d_pfpp->process(conflictProof);
121 : : // add given assertions d_assertions
122 [ + + ]: 38 : for (const Node& assertion : assertions)
123 : : {
124 : 24 : d_assertions.push_back(assertion);
125 : : }
126 : 28 : std::vector<Node> avec{d_assertions.begin(), d_assertions.end()};
127 : 14 : pfnEnsureClosedWrt(options(),
128 : : conflictProof.get(),
129 : : avec,
130 : : "sat-proof",
131 : : "PropPfManager::checkProof");
132 : 14 : }
133 : :
134 : 400 : std::vector<Node> PropPfManager::getUnsatCoreLemmas()
135 : : {
136 : 400 : std::vector<Node> usedLemmas;
137 : 800 : std::vector<Node> allLemmas = getLemmaClauses();
138 : : // compute the unsat core clauses, as below
139 : 800 : std::vector<Node> ucc = getUnsatCoreClauses();
140 [ + - ]: 800 : Trace("prop-pf") << "Compute unsat core lemmas from " << ucc.size()
141 : 400 : << " clauses (of " << allLemmas.size() << " lemmas)"
142 : 400 : << std::endl;
143 [ + - ]: 400 : Trace("prop-pf") << "lemmas: " << allLemmas << std::endl;
144 [ + - ]: 400 : Trace("prop-pf") << "uc: " << ucc << std::endl;
145 : : // filter to only those corresponding to lemmas
146 [ + + ]: 603 : for (const Node& lemma : allLemmas)
147 : : {
148 [ + - ]: 203 : if (std::find(ucc.begin(), ucc.end(), lemma) != ucc.end())
149 : : {
150 : 203 : usedLemmas.push_back(lemma);
151 : : }
152 : : }
153 [ - + ]: 400 : if (d_trackLemmaClauseIds)
154 : : {
155 : 0 : ++d_numUcl;
156 : : uint64_t timestamp;
157 [ - - ]: 0 : for (const Node& lemma : usedLemmas)
158 : : {
159 : 0 : d_uclIds << getInferenceIdFor(lemma, timestamp);
160 : 0 : ++d_uclSize;
161 : : }
162 : : }
163 : 800 : return usedLemmas;
164 : : }
165 : :
166 : 0 : theory::InferenceId PropPfManager::getInferenceIdFor(const Node& lem,
167 : : uint64_t& timestamp) const
168 : : {
169 : : context::CDHashMap<Node, theory::InferenceId>::const_iterator it =
170 : 0 : d_lemmaClauseIds.find(lem);
171 [ - - ]: 0 : if (it != d_lemmaClauseIds.end())
172 : : {
173 : : context::CDHashMap<Node, uint64_t>::const_iterator itt =
174 : 0 : d_lemmaClauseTimestamp.find(lem);
175 [ - - ]: 0 : if (itt != d_lemmaClauseTimestamp.end())
176 : : {
177 : 0 : timestamp = itt->second;
178 : : }
179 : 0 : return it->second;
180 : : }
181 : 0 : return theory::InferenceId::NONE;
182 : : }
183 : 400 : std::vector<Node> PropPfManager::getUnsatCoreClauses()
184 : : {
185 : 400 : std::vector<Node> uc;
186 : : // if it has a proof
187 : 800 : std::shared_ptr<ProofNode> satPf = d_satSolver->getProof();
188 : : // Note that we currently assume that the proof is the standard way of
189 : : // communicating the unsat core of theory lemmas. If no proofs are
190 : : // available, then a trust step (e.g. SAT_REFUTATION) with free assumptions
191 : : // F1 ... Fn can be used to indicate that F1 ... Fn is the unsat core
192 [ - + ]: 400 : if (satPf == nullptr)
193 : : {
194 : 0 : std::stringstream ss;
195 : : ss << "ERROR: cannot get unsat core clauses when SAT solver is not proof "
196 : 0 : "producing.";
197 : 0 : throw LogicException(ss.str());
198 : : }
199 : : // then, get the proof *without* connecting the CNF
200 : 400 : expr::getFreeAssumptions(satPf.get(), uc);
201 : 800 : return uc;
202 : : }
203 : :
204 : 8 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getProofLeaves(
205 : : modes::ProofComponent pc)
206 : : {
207 [ + - ]: 16 : Trace("sat-proof") << "PropPfManager::getProofLeaves: Getting " << pc
208 : 8 : << " component proofs\n";
209 : 16 : std::vector<Node> fassumps;
210 [ + + ][ - + ]: 8 : Assert(pc == modes::ProofComponent::THEORY_LEMMAS
[ - + ][ - - ]
211 : : || pc == modes::ProofComponent::PREPROCESS);
212 : : std::vector<std::shared_ptr<ProofNode>> pfs =
213 : 8 : pc == modes::ProofComponent::THEORY_LEMMAS ? getLemmaClausesProofs()
214 [ + + ]: 16 : : getInputClausesProofs();
215 : 16 : std::shared_ptr<ProofNode> satPf = getProof(false);
216 : 16 : std::vector<Node> satLeaves;
217 : 8 : expr::getFreeAssumptions(satPf.get(), satLeaves);
218 : 8 : std::vector<std::shared_ptr<ProofNode>> usedPfs;
219 [ + + ]: 44 : for (const std::shared_ptr<ProofNode>& pf : pfs)
220 : : {
221 : 72 : Node proven = pf->getResult();
222 [ + + ]: 36 : if (std::find(satLeaves.begin(), satLeaves.end(), proven) != satLeaves.end())
223 : : {
224 : 16 : usedPfs.push_back(pf);
225 : : }
226 : : }
227 : 16 : return usedPfs;
228 : : }
229 : :
230 : 10047 : std::shared_ptr<ProofNode> PropPfManager::getProof(bool connectCnf)
231 : : {
232 : 10047 : auto it = d_propProofs.find(connectCnf);
233 [ + + ]: 10047 : if (it != d_propProofs.end())
234 : : {
235 : 645 : return it->second;
236 : : }
237 : : // retrieve the SAT solver's refutation proof
238 [ + - ]: 9402 : Trace("sat-proof") << "PropPfManager::getProof: Getting proof of false\n";
239 : :
240 : : // get the proof based on the proof mode
241 : 9402 : options::PropProofMode pmode = options().proof.propProofMode;
242 : 9402 : std::shared_ptr<ProofNode> conflictProof;
243 : : // take proof from SAT solver as is
244 : 9402 : conflictProof = d_satSolver->getProof();
245 : :
246 [ - + ][ - + ]: 9402 : Assert(conflictProof);
[ - - ]
247 [ - + ]: 9402 : 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 : : }
262 [ + + ]: 9402 : if (!connectCnf)
263 : : {
264 : 395 : d_propProofs[connectCnf] = conflictProof;
265 : 395 : 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 [ + - ]: 9007 : if (pmode == options::PropProofMode::PROOF)
271 : : {
272 : 9007 : conflictProof = conflictProof->clone();
273 : : }
274 : : // connect it with CNF proof
275 : 9007 : d_pfpp->process(conflictProof);
276 [ - + ]: 9007 : 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 : : }
294 : 9007 : d_propProofs[connectCnf] = conflictProof;
295 : 9007 : return conflictProof;
296 : : }
297 : :
298 : 3195930 : Node PropPfManager::normalizeAndRegister(TNode clauseNode,
299 : : bool input,
300 : : bool doNormalize)
301 : : {
302 : 3195930 : Node normClauseNode = clauseNode;
303 [ + + ]: 3195930 : if (doNormalize)
304 : : {
305 : 6044980 : TheoryProofStepBuffer psb;
306 : 3022490 : normClauseNode = psb.factorReorderElimDoubleNeg(clauseNode);
307 : 3022490 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
308 [ + + ]: 15087600 : for (const std::pair<Node, ProofStep>& step : steps)
309 : : {
310 : 12065100 : d_proof.addStep(step.first, step.second);
311 : : }
312 : : }
313 : 3195930 : 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 [ + - ]: 6391860 : Trace("cnf-input") << "New clause: " << normClauseNode << " " << input
321 : 3195930 : << std::endl;
322 [ + + ]: 3195930 : if (input)
323 : : {
324 : 519321 : d_inputClauses.insert(normClauseNode);
325 : : }
326 : : else
327 : : {
328 : 2676610 : d_lemmaClauses.insert(normClauseNode);
329 [ - + ]: 2676610 : 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 [ + - ]: 3195930 : if (d_satPm)
338 : : {
339 : 6391860 : d_satPm->registerSatAssumptions({normClauseNode});
340 : : }
341 : 3195930 : return normClauseNode;
342 : : }
343 : :
344 : 272628 : LazyCDProof* PropPfManager::getCnfProof() { return &d_proof; }
345 : :
346 : 0 : std::vector<Node> PropPfManager::getInputClauses()
347 : : {
348 : 0 : std::vector<Node> cls;
349 [ - - ]: 0 : for (const Node& c : d_inputClauses)
350 : : {
351 : 0 : cls.push_back(c);
352 : : }
353 : 0 : return cls;
354 : : }
355 : :
356 : 400 : std::vector<Node> PropPfManager::getLemmaClauses()
357 : : {
358 : 400 : std::vector<Node> cls;
359 [ + + ]: 603 : for (const Node& c : d_lemmaClauses)
360 : : {
361 : 203 : cls.push_back(c);
362 : : }
363 : 400 : return cls;
364 : : }
365 : :
366 : 4 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getInputClausesProofs()
367 : : {
368 : 4 : std::vector<std::shared_ptr<ProofNode>> pfs;
369 [ + + ]: 40 : for (const Node& a : d_inputClauses)
370 : : {
371 : 36 : pfs.push_back(d_proof.getProofFor(a));
372 : : }
373 : 4 : return pfs;
374 : : }
375 : :
376 : 4 : std::vector<std::shared_ptr<ProofNode>> PropPfManager::getLemmaClausesProofs()
377 : : {
378 : 4 : std::vector<std::shared_ptr<ProofNode>> pfs;
379 [ - + ]: 4 : for (const Node& a : d_lemmaClauses)
380 : : {
381 : 0 : pfs.push_back(d_proof.getProofFor(a));
382 : : }
383 : 4 : return pfs;
384 : : }
385 : :
386 : 79837 : void PropPfManager::notifyExplainedPropagation(TrustNode trn)
387 : : {
388 : 159674 : Node proven = trn.getProven();
389 : : // If we are not producing proofs in the theory engine there is no need to
390 : : // keep track in d_proof of the clausification. We still need however to let
391 : : // the SAT proof manager know that this clause is an assumption.
392 : 79837 : bool proofLogging = trn.getGenerator() != nullptr;
393 [ + - ]: 159674 : Trace("cnf")
394 : 0 : << "PropPfManager::notifyExplainedPropagation: proven explanation"
395 : 79837 : << proven << ", proofLogging=" << proofLogging << "\n";
396 [ + + ]: 79837 : if (proofLogging)
397 : : {
398 [ - + ][ - + ]: 79834 : Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
[ - - ]
399 [ + - ]: 159668 : Trace("cnf-steps") << proven << " by explainPropagation "
400 [ - + ][ - - ]: 79834 : << trn.identifyGenerator() << std::endl;
401 : 79834 : d_proof.addLazyStep(proven,
402 : : trn.getGenerator(),
403 : : TrustId::NONE,
404 : : true,
405 : : "PropPfManager::notifyExplainedPropagation");
406 : : }
407 : : // since the propagation is added directly to the SAT solver via theoryProxy,
408 : : // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
409 : 79837 : NodeManager* nm = nodeManager();
410 : 159674 : Node clauseImpliesElim;
411 [ + + ]: 79837 : if (proofLogging)
412 : : {
413 : 79834 : clauseImpliesElim = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
414 [ + - ]: 159668 : Trace("cnf") << "PropPfManager::notifyExplainedPropagation: adding "
415 : 79834 : << ProofRule::IMPLIES_ELIM << " rule to conclude "
416 : 79834 : << clauseImpliesElim << "\n";
417 : 159668 : d_proof.addStep(clauseImpliesElim, ProofRule::IMPLIES_ELIM, {proven}, {});
418 : : }
419 : 159674 : Node clauseExp;
420 : : // need to eliminate AND
421 [ + + ]: 79837 : if (proven[0].getKind() == Kind::AND)
422 : : {
423 : 300676 : std::vector<Node> disjunctsAndNeg{proven[0]};
424 : 150338 : std::vector<Node> disjunctsRes;
425 [ + + ]: 660429 : for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i)
426 : : {
427 : 585260 : disjunctsAndNeg.push_back(proven[0][i].notNode());
428 : 585260 : disjunctsRes.push_back(proven[0][i].notNode());
429 : : }
430 : 75169 : disjunctsRes.push_back(proven[1]);
431 : 75169 : clauseExp = nm->mkNode(Kind::OR, disjunctsRes);
432 [ + + ]: 75169 : if (proofLogging)
433 : : {
434 : : // add proof steps to convert into clause
435 : 75166 : Node clauseAndNeg = nm->mkNode(Kind::OR, disjunctsAndNeg);
436 : 150332 : d_proof.addStep(clauseAndNeg, ProofRule::CNF_AND_NEG, {}, {proven[0]});
437 : 375830 : d_proof.addStep(clauseExp,
438 : : ProofRule::RESOLUTION,
439 : : {clauseAndNeg, clauseImpliesElim},
440 : 450996 : {nm->mkConst(true), proven[0]});
441 : : }
442 : : }
443 : : else
444 : : {
445 : 4668 : clauseExp = nm->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
446 : : }
447 : 79837 : d_currPropagationProcessed = normalizeAndRegister(clauseExp, false);
448 : : // If we are not logging the clausification, we need to add the clause, as *it
449 : : // will be saved in the SAT solver* (i.e., as clauseExp), as closed step in
450 : : // the d_proof, so that there are no non-input assumptions.
451 [ + + ]: 79837 : if (!proofLogging)
452 : : {
453 : 3 : d_proof.addTrustedStep(clauseExp, TrustId::THEORY_LEMMA, {}, {});
454 : : }
455 : 79837 : }
456 : :
457 : 153 : Node PropPfManager::getLastExplainedPropagation() const
458 : : {
459 : 153 : return d_currPropagationProcessed;
460 : : }
461 : :
462 : 153 : void PropPfManager::resetLastExplainedPropagation()
463 : : {
464 : 153 : d_currPropagationProcessed = Node::null();
465 : 153 : }
466 : :
467 : : } // namespace prop
468 : : } // namespace cvc5::internal
|
