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 Minisat.
11 : : */
12 : :
13 : : #include "prop/minisat/sat_proof_manager.h"
14 : :
15 : : #include "options/proof_options.h"
16 : : #include "proof/proof_node_algorithm.h"
17 : : #include "proof/theory_proof_step_buffer.h"
18 : : #include "prop/cnf_stream.h"
19 : : #include "prop/minisat/minisat.h"
20 : : #include "prop/prop_proof_manager.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace prop {
24 : :
25 : 20020 : SatProofManager::SatProofManager(Env& env,
26 : : Minisat::Solver* solver,
27 : : CnfStream* cnfStream,
28 : 20020 : PropPfManager* ppm)
29 : : : EnvObj(env),
30 : 20020 : d_solver(solver),
31 : 20020 : d_cnfStream(cnfStream),
32 : 20020 : d_ppm(ppm),
33 : 20020 : d_resChains(d_env, true, userContext()),
34 : : // enforce unique assumptions and no symmetry. This avoids creating
35 : : // duplicate assumption proof nodes for the premises of resolution steps,
36 : : // which when expanded in the lazy proof chain would duplicate their
37 : : // justifications (which can lead to performance impacts when proof
38 : : // post-processing). Symmetry we can disable because there is no equality
39 : : // reasoning performed here
40 : 20020 : d_resChainPg(d_env, userContext(), true, false),
41 : 20020 : d_assumptions(userContext()),
42 : 20020 : d_conflictLit(undefSatVariable),
43 : 20020 : d_optResLevels(userContext()),
44 : 20020 : d_optResManager(userContext(), &d_resChains, d_optResProofs),
45 : 80080 : d_optClausesManager(userContext(), ppm->getCnfProof(), d_optClausesPfs)
46 : : {
47 : 20020 : d_true = nodeManager()->mkConst(true);
48 : 20020 : d_false = nodeManager()->mkConst(false);
49 : 20020 : d_optResManager.trackNodeHashSet(&d_assumptions, &d_assumptionLevels);
50 : : // temporary, to allow this class to be notified when new clauses are added
51 : : // see https://github.com/cvc5/cvc5-wishues/issues/149
52 : 20020 : ppm->d_satPm = this;
53 : 20020 : }
54 : :
55 : 0 : void SatProofManager::printClause(const Minisat::Clause& clause)
56 : : {
57 [ - - ]: 0 : for (size_t i = 0, size = clause.size(); i < size; ++i)
58 : : {
59 : 0 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
60 [ - - ]: 0 : Trace("sat-proof") << satLit << " ";
61 : : }
62 : 0 : }
63 : :
64 : 6948272 : Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
65 : : {
66 : 6948272 : std::vector<Node> clauseNodes;
67 [ + + ]: 38924645 : for (size_t i = 0, size = clause.size(); i < size; ++i)
68 : : {
69 : 31976373 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
70 : 31976373 : clauseNodes.push_back(d_cnfStream->getNode(satLit));
71 : : }
72 : : // order children by node id
73 : 6948272 : std::sort(clauseNodes.begin(), clauseNodes.end());
74 : 13896544 : return nodeManager()->mkNode(Kind::OR, clauseNodes);
75 : 6948272 : }
76 : :
77 : 210178 : void SatProofManager::startResChain(const Minisat::Clause& start)
78 : : {
79 [ - + ]: 210178 : if (TraceIsOn("sat-proof"))
80 : : {
81 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::startResChain: ";
82 : 0 : printClause(start);
83 [ - - ]: 0 : Trace("sat-proof") << "\n";
84 : : }
85 : 210178 : d_resLinks.emplace_back(getClauseNode(start), Node::null(), true);
86 : 210178 : }
87 : :
88 : 1640607 : void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant)
89 : : {
90 : 1640607 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
91 : 1640607 : Node litNode = d_cnfStream->getNodeCache()[satLit];
92 : 1640607 : bool negated = satLit.isNegated();
93 [ + + ][ + - ]: 1640607 : Assert(!negated || litNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
94 [ + + ]: 1640607 : if (!redundant)
95 : : {
96 [ + - ]: 1460354 : Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
97 : 0 : << satLit.isNegated() << "} [" << satLit << "] "
98 : 730177 : << ~satLit << "\n";
99 : : // if lit is negated then the chain resolution construction will use it as a
100 : : // pivot occurring as is in the second clause and the node under the
101 : : // negation in the first clause
102 : 730177 : d_resLinks.emplace_back(d_cnfStream->getNodeCache()[~satLit],
103 : 1460354 : negated ? litNode[0] : litNode,
104 [ + + ]: 1460354 : !satLit.isNegated());
105 : : }
106 : : else
107 : : {
108 [ + - ]: 1820860 : Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit "
109 : 910430 : << satLit << " stored\n";
110 : 910430 : d_redundantLits.push_back(satLit);
111 : : }
112 : 1640607 : }
113 : :
114 : 4183309 : void SatProofManager::addResolutionStep(const Minisat::Clause& clause,
115 : : Minisat::Lit lit)
116 : : {
117 : 4183309 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
118 : 4183309 : Node litNode = d_cnfStream->getNodeCache()[satLit];
119 : 4183309 : bool negated = satLit.isNegated();
120 [ + + ][ + - ]: 4183309 : Assert(!negated || litNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
121 : 4183309 : Node clauseNode = getClauseNode(clause);
122 : : // if lit is negative then the chain resolution construction will use it as a
123 : : // pivot occurring as is in the second clause and the node under the
124 : : // negation in the first clause, which means that the third argument of the
125 : : // tuple must be false
126 [ + + ]: 4183309 : d_resLinks.emplace_back(clauseNode, negated ? litNode[0] : litNode, negated);
127 [ - + ]: 4183309 : if (TraceIsOn("sat-proof"))
128 : : {
129 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
130 : 0 : << satLit.isNegated() << "} [" << ~satLit << "] ";
131 : 0 : printClause(clause);
132 [ - - ]: 0 : Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t"
133 : 0 : << clauseNode << " - lvl " << clause.level() + 1 << "\n";
134 : : }
135 : 4183309 : }
136 : :
137 : 9910 : void SatProofManager::endResChain(Minisat::Lit lit)
138 : : {
139 : 9910 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
140 [ + - ]: 19820 : Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
141 : 9910 : << userContext()->getLevel() << "\n";
142 [ + - ]: 19820 : Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
143 : 9910 : << satLit;
144 : 9910 : endResChain(d_cnfStream->getNode(satLit), {satLit});
145 : 9910 : }
146 : :
147 : 200268 : void SatProofManager::endResChain(const Minisat::Clause& clause)
148 : : {
149 [ - + ]: 200268 : if (TraceIsOn("sat-proof"))
150 : : {
151 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
152 : 0 : << userContext()->getLevel() << "\n";
153 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::endResChain: chain_res for ";
154 : 0 : printClause(clause);
155 : : }
156 : 200268 : std::set<SatLiteral> clauseLits;
157 [ + + ]: 3723616 : for (unsigned i = 0, size = clause.size(); i < size; ++i)
158 : : {
159 : 3523348 : clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i]));
160 : : }
161 : 200268 : endResChain(getClauseNode(clause), clauseLits, clause.level() + 1);
162 : 200268 : }
163 : :
164 : 210178 : void SatProofManager::endResChain(Node conclusion,
165 : : const std::set<SatLiteral>& conclusionLits,
166 : : uint32_t clauseLevel)
167 : : {
168 [ + - ]: 210178 : Trace("sat-proof") << ", " << conclusion << "\n";
169 : 210178 : LazyCDProof* cnfProof = d_ppm->getCnfProof();
170 : 210178 : if (cnfProof->hasStep(conclusion) || cnfProof->hasGenerator(conclusion))
171 : : {
172 [ + - ]: 496 : Trace("sat-proof") << "SatProofManager::endResChain: cnf proof has "
173 : 248 : "step/gen for it; skip\n";
174 : : // clearing
175 : 248 : d_resLinks.clear();
176 : 248 : d_redundantLits.clear();
177 : 2648 : return;
178 : : }
179 [ + + ]: 209930 : if (d_resChains.hasGenerator(conclusion))
180 : : {
181 [ + - ]: 3712 : Trace("sat-proof")
182 : 0 : << "SatProofManager::endResChain: skip repeated proof of " << conclusion
183 : 1856 : << "\n";
184 : : // clearing
185 : 1856 : d_resLinks.clear();
186 : 1856 : d_redundantLits.clear();
187 : 1856 : return;
188 : : }
189 : : // first process redundant literals
190 : 208074 : std::set<SatLiteral> visited;
191 : 208074 : unsigned pos = d_resLinks.size();
192 [ + + ]: 1114610 : for (SatLiteral satLit : d_redundantLits)
193 : : {
194 : 906536 : processRedundantLit(satLit, conclusionLits, visited, pos);
195 : : }
196 : 208074 : d_redundantLits.clear();
197 : : // build resolution chain
198 : : // the conclusion is stored already in the arguments because of the
199 : : // possibility of reordering
200 : 624222 : std::vector<Node> children, args{conclusion};
201 : 208074 : std::vector<Node> pols;
202 : 208074 : std::vector<Node> lits;
203 [ + + ]: 7565608 : for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i)
204 : : {
205 : 7357534 : Node clause, pivot;
206 : : bool posFirst;
207 : 7357534 : std::tie(clause, pivot, posFirst) = d_resLinks[i];
208 : 7357534 : children.push_back(clause);
209 [ + - ]: 7357534 : Trace("sat-proof") << "SatProofManager::endResChain: ";
210 [ + + ]: 7357534 : if (i > 0)
211 : : {
212 [ + - ]: 14298920 : Trace("sat-proof") << "{" << posFirst << "} ["
213 : 7149460 : << d_cnfStream->getTranslationCache()[pivot] << "] ";
214 : : }
215 : : // special case for clause (or l1 ... ln) being a single literal
216 : : // corresponding itself to a clause, which is indicated by the pivot being
217 : : // of the form (not (or l1 ... ln))
218 : 22072602 : if (clause.getKind() == Kind::OR
219 [ + + ][ - + ]: 14715068 : && !(pivot.getKind() == Kind::NOT && pivot[0].getKind() == Kind::OR
[ - - ][ + + ]
[ - - ]
220 [ - - ][ - + ]: 7357534 : && pivot[0] == clause))
[ - + ][ - - ]
221 : : {
222 [ + + ]: 33755382 : for (unsigned j = 0, sizeJ = clause.getNumChildren(); j < sizeJ; ++j)
223 : : {
224 [ + - ][ - + ]: 27320382 : Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause[j]];
[ - - ]
225 [ + + ]: 27320382 : if (j < sizeJ - 1)
226 : : {
227 [ + - ]: 20885382 : Trace("sat-proof") << ", ";
228 : : }
229 : : }
230 : : }
231 : : else
232 : : {
233 [ - + ][ - - ]: 922534 : Assert(d_cnfStream->getTranslationCache().find(clause)
234 : : != d_cnfStream->getTranslationCache().end())
235 [ - + ][ - - ]: 922534 : << "clause node " << clause
236 [ - + ][ - + ]: 922534 : << " treated as unit has no literal. Pivot is " << pivot << "\n";
[ - - ]
237 [ + - ]: 922534 : Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause];
238 : : }
239 [ + - ]: 7357534 : Trace("sat-proof") << " : ";
240 [ + + ]: 7357534 : if (i > 0)
241 : : {
242 [ + + ]: 7149460 : pols.push_back(posFirst ? d_true : d_false);
243 : 7149460 : lits.push_back(pivot);
244 [ + - ]: 7149460 : Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] ";
245 : : }
246 [ + - ]: 7357534 : Trace("sat-proof") << clause << "\n";
247 : 7357534 : }
248 : 208074 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, pols));
249 : 208074 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, lits));
250 : : // clearing
251 : 208074 : d_resLinks.clear();
252 : : // whether no-op
253 [ - + ]: 208074 : if (children.size() == 1)
254 : : {
255 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion "
256 : 0 : << conclusion << " is set-equal to premise "
257 : 0 : << children[0] << "\n";
258 : 0 : return;
259 : : }
260 : : // whether trivial cycle
261 [ + + ]: 7563976 : for (const Node& child : children)
262 : : {
263 [ + + ]: 7356446 : if (conclusion == child)
264 : : {
265 [ + - ]: 1088 : Trace("sat-proof")
266 : 0 : << "SatProofManager::endResChain: no-op. The conclusion "
267 : 544 : << conclusion << " is equal to a premise\n";
268 : 544 : return;
269 : : }
270 : : }
271 : : // if this is a clause whose level is below the current user level, we save it
272 : : // to have its proof kept during backtracking
273 [ + + ]: 207530 : if (clauseLevel < userContext()->getLevel())
274 : : {
275 : 43 : d_optResLevels[conclusion] = clauseLevel;
276 [ + - ]: 86 : Trace("sat-proof") << "SatProofManager::endResChain: ..clause's lvl "
277 : 0 : << clauseLevel << " below curr user level "
278 : 43 : << userContext()->getLevel() << "\n";
279 : : }
280 : : // since the conclusion can be both reordered and without duplicates and the
281 : : // SAT solver does not record this information, we use a CHAIN_M_RESOLUTION
282 : : // step, which bypasses these. Note that we could generate a chain resolution
283 : : // rule here by explicitly computing the detailed steps, but leave this for
284 : : // post-processing.
285 : 207530 : ProofStep ps(ProofRule::CHAIN_M_RESOLUTION, children, args);
286 : : // note that we must tell the proof generator to overwrite if repeated
287 : 207530 : d_resChainPg.addStep(conclusion, ps);
288 : : // the premises of this resolution may not have been justified yet, so we do
289 : : // not pass assumptions to check closedness
290 : 207530 : d_resChains.addLazyStep(conclusion, &d_resChainPg);
291 [ + + ][ + + ]: 210250 : }
[ + + ][ + + ]
[ + + ]
292 : :
293 : 3299721 : void SatProofManager::processRedundantLit(
294 : : SatLiteral lit,
295 : : const std::set<SatLiteral>& conclusionLits,
296 : : std::set<SatLiteral>& visited,
297 : : unsigned pos)
298 : : {
299 [ + - ]: 6599442 : Trace("sat-proof") << push
300 : 0 : << "SatProofManager::processRedundantLit: Lit: " << lit
301 : 3299721 : << "\n";
302 [ + + ]: 3299721 : if (visited.count(lit))
303 : : {
304 [ + - ]: 1022949 : Trace("sat-proof") << "already visited\n" << pop;
305 : 1225634 : return;
306 : : }
307 : : Minisat::Solver::TCRef reasonRef =
308 : 2276772 : d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
309 [ + + ]: 2276772 : if (reasonRef == Minisat::Solver::TCRef_Undef)
310 : : {
311 [ + - ]: 405370 : Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos
312 : 0 : << "\n"
313 : 202685 : << pop;
314 : 202685 : visited.insert(lit);
315 : 202685 : Node litNode = d_cnfStream->getNodeCache()[lit];
316 : 202685 : bool negated = lit.isNegated();
317 [ + + ][ + - ]: 202685 : Assert(!negated || litNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
318 : :
319 : 202685 : d_resLinks.emplace(d_resLinks.begin() + pos,
320 : 202685 : d_cnfStream->getNodeCache()[~lit],
321 : 405370 : negated ? litNode[0] : litNode,
322 [ + + ]: 202685 : !negated);
323 : 202685 : return;
324 : 202685 : }
325 [ - + ][ - + ]: 2074087 : Assert(reasonRef < d_solver->ca.size())
[ - - ]
326 : 0 : << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
327 : 0 : << d_solver->ca.size() << "\n";
328 : 2074087 : const Minisat::Clause& reason = d_solver->ca[reasonRef];
329 [ - + ]: 2074087 : if (TraceIsOn("sat-proof"))
330 : : {
331 [ - - ]: 0 : Trace("sat-proof") << "reason: ";
332 : 0 : printClause(reason);
333 [ - - ]: 0 : Trace("sat-proof") << "\n";
334 : : }
335 : : // Since processRedundantLit calls can reallocate memory in the SAT solver due
336 : : // to explaining stuff, we directly get the literals and the clause node here
337 : 2074087 : std::vector<SatLiteral> toProcess;
338 [ + + ]: 5772656 : for (unsigned i = 1, size = reason.size(); i < size; ++i)
339 : : {
340 : 3698569 : toProcess.push_back(MinisatSatSolver::toSatLiteral(reason[i]));
341 : : }
342 : 2074087 : Node clauseNode = getClauseNode(reason);
343 : : // check if redundant literals in the reason. The first literal is the one we
344 : : // will be eliminating, so we check the others
345 [ + + ]: 5772656 : for (unsigned i = 0, size = toProcess.size(); i < size; ++i)
346 : : {
347 : 3698569 : SatLiteral satLit = toProcess[i];
348 : : // if literal does not occur in the conclusion we process it as well
349 [ + + ]: 3698569 : if (!conclusionLits.count(satLit))
350 : : {
351 : 2393185 : processRedundantLit(satLit, conclusionLits, visited, pos);
352 : : }
353 : : }
354 [ - + ][ - + ]: 2074087 : Assert(!visited.count(lit));
[ - - ]
355 : 2074087 : visited.insert(lit);
356 [ + - ]: 4148174 : Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos
357 : 0 : << "\n"
358 : 2074087 : << pop;
359 : : // add the step before steps for children. Note that the step is with the
360 : : // reason, not only with ~lit, since the learned clause is built under the
361 : : // assumption that the redundant literal is removed via the resolution with
362 : : // the explanation of its negation
363 : 2074087 : Node litNode = d_cnfStream->getNodeCache()[lit];
364 : 2074087 : bool negated = lit.isNegated();
365 [ + + ][ + - ]: 2074087 : Assert(!negated || litNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
366 : 2074087 : d_resLinks.emplace(d_resLinks.begin() + pos,
367 : : clauseNode,
368 : 4148174 : negated ? litNode[0] : litNode,
369 [ + + ]: 2074087 : !negated);
370 : 2074087 : }
371 : :
372 : 154965 : void SatProofManager::explainLit(SatLiteral lit,
373 : : std::unordered_set<TNode>& premises)
374 : : {
375 [ + - ]: 154965 : Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
376 : 154965 : Node litNode = d_cnfStream->getNode(lit);
377 [ + - ]: 154965 : Trace("sat-proof") << " [" << litNode << "]\n";
378 : : // We don't need to explain nodes who are inputs. Note that it's *necessary*
379 : : // to avoid attempting such explanations because they can introduce cycles at
380 : : // the node level. For example, if a literal l depends on an input clause C
381 : : // but a literal l', node-equivalent to C, depends on l, we may have a cycle
382 : : // when building the overall SAT proof.
383 [ + + ]: 154965 : if (d_assumptions.contains(litNode))
384 : : {
385 [ + - ]: 69428 : Trace("sat-proof")
386 : 0 : << "SatProofManager::explainLit: input assumption, ABORT\n"
387 : 34714 : << pop;
388 : 34714 : return;
389 : : }
390 : : // We don't need to explain nodes who already have proofs.
391 : : //
392 : : // Note that if we had two literals for (= a b) and (= b a) and we had already
393 : : // a proof for (= a b) this test would return true for (= b a), which could
394 : : // lead to open proof. However we should never have two literals like this in
395 : : // the SAT solver since they'd be rewritten to the same one
396 [ + + ]: 120251 : if (d_resChainPg.hasProofFor(litNode))
397 : : {
398 [ + - ]: 89940 : Trace("sat-proof") << "SatProofManager::explainLit: already justified "
399 : 0 : << lit << ", ABORT\n"
400 : 44970 : << pop;
401 : 44970 : return;
402 : : }
403 : : Minisat::Solver::TCRef reasonRef =
404 : 75281 : d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
405 [ + + ]: 75281 : if (reasonRef == Minisat::Solver::TCRef_Undef)
406 : : {
407 [ + - ]: 79 : Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop;
408 : 79 : return;
409 : : }
410 [ - + ][ - + ]: 75202 : Assert(reasonRef < d_solver->ca.size())
[ - - ]
411 : 0 : << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
412 : 0 : << d_solver->ca.size() << "\n";
413 : 75202 : const Minisat::Clause& reason = d_solver->ca[reasonRef];
414 : 75202 : unsigned size = reason.size();
415 [ - + ]: 75202 : if (TraceIsOn("sat-proof"))
416 : : {
417 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::explainLit: with clause: ";
418 : 0 : printClause(reason);
419 [ - - ]: 0 : Trace("sat-proof") << "\n";
420 : : }
421 : : #ifdef CVC5_ASSERTIONS
422 : : // pedantically check that the negation of the literal to explain *does not*
423 : : // occur in the reason, otherwise we will loop forever
424 [ + + ]: 275048 : for (unsigned i = 0; i < size; ++i)
425 : : {
426 [ - + ][ - + ]: 199846 : AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit)
[ - - ]
427 : 0 : << "cyclic justification\n";
428 : : }
429 : : #endif
430 : : // add the reason clause first
431 : 300808 : std::vector<Node> children{getClauseNode(reason)}, args;
432 : : // save in the premises
433 : 75202 : premises.insert(children.back());
434 : : // Since explainLit calls can reallocate memory in the
435 : : // SAT solver, we directly get the literals we need to explain so we no
436 : : // longer depend on the reference to reason
437 : 75202 : std::vector<Node> toExplain{children.back().begin(), children.back().end()};
438 [ + - ]: 75202 : Trace("sat-proof") << push;
439 : 75202 : std::vector<Node> pols;
440 : 75202 : std::vector<Node> lits;
441 [ + + ]: 275048 : for (unsigned i = 0; i < size; ++i)
442 : : {
443 : : #ifdef CVC5_ASSERTIONS
444 : : // pedantically make sure that the reason stays the same
445 : 199846 : const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef];
446 [ - + ][ - + ]: 199846 : AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
[ - - ]
447 [ - + ][ - + ]: 199846 : AlwaysAssert(children[0] == getClauseNode(reloadedReason));
[ - - ]
448 : : #endif
449 : 199846 : SatLiteral currLit = d_cnfStream->getTranslationCache()[toExplain[i]];
450 : : // ignore the lit we are trying to explain...
451 [ + + ]: 199846 : if (currLit == lit)
452 : : {
453 : 75202 : continue;
454 : : }
455 : 124644 : std::unordered_set<TNode> childPremises;
456 : 124644 : explainLit(~currLit, childPremises);
457 : : // save to resolution chain premises / arguments
458 [ - + ][ - + ]: 124644 : Assert(d_cnfStream->getNodeCache().find(currLit)
[ - - ]
459 : : != d_cnfStream->getNodeCache().end());
460 : 124644 : children.push_back(d_cnfStream->getNodeCache()[~currLit]);
461 : 124644 : Node currLitNode = d_cnfStream->getNodeCache()[currLit];
462 : 124644 : bool negated = currLit.isNegated();
463 [ + + ][ + - ]: 124644 : Assert(!negated || currLitNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
464 : : // note this is the opposite of what is done in addResolutionStep. This is
465 : : // because here the clause, which contains the literal being analyzed, is
466 : : // the first clause rather than the second
467 [ + + ]: 124644 : pols.push_back(!negated ? d_true : d_false);
468 [ + + ]: 124644 : lits.push_back(negated ? currLitNode[0] : currLitNode);
469 : : // add child premises and the child itself
470 : 124644 : premises.insert(childPremises.begin(), childPremises.end());
471 : 124644 : premises.insert(d_cnfStream->getNodeCache()[~currLit]);
472 : 124644 : }
473 [ - + ]: 75202 : if (TraceIsOn("sat-proof"))
474 : : {
475 [ - - ]: 0 : Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for "
476 : 0 : << lit << ", " << litNode << " with clauses:\n";
477 [ - - ]: 0 : for (unsigned i = 0, csize = children.size(); i < csize; ++i)
478 : : {
479 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::explainLit: " << children[i];
480 [ - - ]: 0 : if (i > 0)
481 : : {
482 [ - - ]: 0 : Trace("sat-proof") << " [" << lits[i] << ", " << pols[i] << "]";
483 : : }
484 [ - - ]: 0 : Trace("sat-proof") << "\n";
485 : : }
486 : : }
487 : : // if justification of children contains the expected conclusion, avoid the
488 : : // cyclic proof by aborting.
489 [ - + ]: 75202 : if (premises.count(litNode))
490 : : {
491 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit
492 : 0 : << " [" << litNode << "], ABORT\n"
493 : 0 : << pop;
494 : 0 : return;
495 : : }
496 [ + - ]: 75202 : Trace("sat-proof") << pop;
497 : : // create step
498 : 75202 : args.push_back(litNode);
499 : 75202 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, pols));
500 : 75202 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, lits));
501 : 75202 : ProofStep ps(ProofRule::CHAIN_M_RESOLUTION, children, args);
502 : 75202 : d_resChainPg.addStep(litNode, ps);
503 : : // the premises in the limit of the justification may correspond to other
504 : : // links in the chain which have, themselves, literals yet to be justified. So
505 : : // we are not ready yet to check closedness w.r.t. CNF transformation of the
506 : : // preprocessed assertions
507 : 75202 : d_resChains.addLazyStep(litNode, &d_resChainPg);
508 [ + - ][ + - ]: 154965 : }
[ + - ][ + - ]
[ + - ][ + + ]
509 : :
510 : 9532 : void SatProofManager::finalizeProof(Node inConflictNode,
511 : : const std::vector<SatLiteral>& inConflict)
512 : : {
513 [ + - ]: 19064 : Trace("sat-proof")
514 : 0 : << "SatProofManager::finalizeProof: conflicting clause node: "
515 : 9532 : << inConflictNode << "\n";
516 : : // nothing to do
517 [ + + ]: 9532 : if (inConflictNode == d_false)
518 : : {
519 : 3571 : return;
520 : : }
521 [ - + ]: 5961 : if (TraceIsOn("sat-proof-debug2"))
522 : : {
523 [ - - ]: 0 : Trace("sat-proof-debug2")
524 : 0 : << push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
525 : 0 : std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
526 : 0 : std::unordered_set<Node> skip;
527 [ - - ]: 0 : for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
528 : : {
529 [ - - ]: 0 : if (skip.count(link.first))
530 : : {
531 : 0 : continue;
532 : : }
533 : 0 : auto it = d_cnfStream->getTranslationCache().find(link.first);
534 [ - - ]: 0 : if (it != d_cnfStream->getTranslationCache().end())
535 : : {
536 [ - - ]: 0 : Trace("sat-proof-debug2")
537 : 0 : << "SatProofManager::finalizeProof: " << it->second;
538 : : }
539 : : // a refl step added due to double elim negation, ignore
540 [ - - ]: 0 : else if (link.second->getRule() == ProofRule::REFL)
541 : : {
542 : 0 : continue;
543 : : }
544 : : // a clause
545 : : else
546 : : {
547 [ - - ]: 0 : Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:";
548 : 0 : Assert(link.first.getKind() == Kind::OR) << link.first;
549 [ - - ]: 0 : for (const Node& n : link.first)
550 : : {
551 : 0 : it = d_cnfStream->getTranslationCache().find(n);
552 : 0 : Assert(it != d_cnfStream->getTranslationCache().end());
553 [ - - ]: 0 : Trace("sat-proof-debug2") << it->second << " ";
554 : 0 : }
555 : : }
556 [ - - ]: 0 : Trace("sat-proof-debug2") << "\n";
557 [ - - ]: 0 : Trace("sat-proof-debug2")
558 : 0 : << "SatProofManager::finalizeProof: " << link.first << "\n";
559 : : // get resolution
560 : 0 : Node cur = link.first;
561 : 0 : std::shared_ptr<ProofNode> pfn = link.second;
562 [ - - ]: 0 : while (pfn->getRule() != ProofRule::CHAIN_M_RESOLUTION)
563 : : {
564 : 0 : Assert(pfn->getChildren().size() == 1
565 : : && pfn->getChildren()[0]->getRule() == ProofRule::ASSUME)
566 : 0 : << *link.second.get() << "\n"
567 : 0 : << *pfn.get();
568 : 0 : cur = pfn->getChildren()[0]->getResult();
569 : : // retrieve justification of assumption in the links
570 : 0 : Assert(links.find(cur) != links.end());
571 : 0 : pfn = links[cur];
572 : : // ignore it in the rest of the outside loop
573 : 0 : skip.insert(cur);
574 : : }
575 : 0 : std::vector<Node> fassumps;
576 : 0 : expr::getFreeAssumptions(pfn.get(), fassumps);
577 [ - - ]: 0 : Trace("sat-proof-debug2") << push;
578 [ - - ]: 0 : for (const Node& fa : fassumps)
579 : : {
580 [ - - ]: 0 : Trace("sat-proof-debug2") << "SatProofManager::finalizeProof: - ";
581 : 0 : it = d_cnfStream->getTranslationCache().find(fa);
582 [ - - ]: 0 : if (it != d_cnfStream->getTranslationCache().end())
583 : : {
584 [ - - ]: 0 : Trace("sat-proof-debug2") << it->second << "\n";
585 : 0 : continue;
586 : : }
587 : : // then it's a clause
588 : 0 : Assert(fa.getKind() == Kind::OR);
589 [ - - ]: 0 : for (const Node& n : fa)
590 : : {
591 : 0 : it = d_cnfStream->getTranslationCache().find(n);
592 : 0 : Assert(it != d_cnfStream->getTranslationCache().end());
593 [ - - ]: 0 : Trace("sat-proof-debug2") << it->second << " ";
594 : 0 : }
595 [ - - ]: 0 : Trace("sat-proof-debug2") << "\n";
596 : : }
597 [ - - ]: 0 : Trace("sat-proof-debug2") << pop;
598 [ - - ]: 0 : Trace("sat-proof-debug2")
599 : 0 : << "SatProofManager::finalizeProof: " << *pfn.get() << "\n=======\n";
600 : : ;
601 : 0 : }
602 [ - - ]: 0 : Trace("sat-proof-debug2") << pop;
603 : 0 : }
604 : : // We will resolve away of the literals l_1...l_n in inConflict. At this point
605 : : // each ~l_i must be either explainable, the result of a previously saved
606 : : // resolution chain, or an input. In account of it possibly being the first,
607 : : // we call explainLit on each ~l_i while accumulating the children and
608 : : // arguments for the resolution step to conclude false.
609 : 23844 : std::vector<Node> children{inConflictNode}, args;
610 : 5961 : std::unordered_set<TNode> premises;
611 : 5961 : std::vector<Node> pols;
612 : 5961 : std::vector<Node> lits;
613 [ + + ]: 27861 : for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
614 : : {
615 [ - + ][ - + ]: 21900 : Assert(d_cnfStream->getNodeCache().find(inConflict[i])
[ - - ]
616 : : != d_cnfStream->getNodeCache().end());
617 : 21900 : std::unordered_set<TNode> childPremises;
618 : 21900 : explainLit(~inConflict[i], childPremises);
619 : 21900 : Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
620 : : // save to resolution chain premises / arguments
621 : 21900 : children.push_back(negatedLitNode);
622 : 21900 : Node litNode = d_cnfStream->getNodeCache()[inConflict[i]];
623 : 21900 : bool negated = inConflict[i].isNegated();
624 [ + + ][ + - ]: 21900 : Assert(!negated || litNode.getKind() == Kind::NOT);
[ - + ][ - + ]
[ - - ]
625 : : // note this is the opposite of what is done in addResolutionStep. This is
626 : : // because here the clause, which contains the literal being analyzed, is
627 : : // the first clause rather than the second
628 [ + + ]: 21900 : pols.push_back(!negated ? d_true : d_false);
629 [ + + ]: 21900 : lits.push_back(negated ? litNode[0] : litNode);
630 : : // add child premises and the child itself
631 : 21900 : premises.insert(childPremises.begin(), childPremises.end());
632 : 21900 : premises.insert(negatedLitNode);
633 [ + - ]: 21900 : Trace("sat-proof") << "===========\n";
634 : 21900 : }
635 [ - + ]: 5961 : if (TraceIsOn("sat-proof"))
636 : : {
637 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false "
638 : 0 : "with clauses:\n";
639 [ - - ]: 0 : for (unsigned i = 0, size = children.size(); i < size; ++i)
640 : : {
641 [ - - ]: 0 : Trace("sat-proof") << "SatProofManager::finalizeProof: " << children[i];
642 [ - - ]: 0 : if (i > 0)
643 : : {
644 [ - - ]: 0 : Trace("sat-proof") << " [" << args[i - 1] << "]";
645 : : }
646 [ - - ]: 0 : Trace("sat-proof") << "\n";
647 : : }
648 : : }
649 : : // create step
650 : 5961 : args.push_back(d_false);
651 : 5961 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, pols));
652 : 5961 : args.push_back(nodeManager()->mkNode(Kind::SEXPR, lits));
653 : 5961 : ProofStep ps(ProofRule::CHAIN_M_RESOLUTION, children, args);
654 : 5961 : d_resChainPg.addStep(d_false, ps);
655 : : // not yet ready to check closedness because maybe only now we will justify
656 : : // literals used in resolutions
657 : 5961 : d_resChains.addLazyStep(d_false, &d_resChainPg);
658 : : // Fix point justification of literals in leaves of the proof of false
659 : : bool expanded;
660 [ + + ]: 7174 : do
661 : : {
662 : 7174 : expanded = false;
663 [ + - ]: 7174 : Trace("sat-proof") << "expand assumptions to prove false\n";
664 : 7174 : std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
665 [ - + ][ - + ]: 7174 : Assert(pfn);
[ - - ]
666 [ - + ]: 7174 : if (TraceIsOn("sat-proof-debug"))
667 : : {
668 : 0 : std::stringstream ss;
669 : 0 : pfn->printDebug(ss, true);
670 : 0 : Trace("sat-proof-debug") << "sat proof of false: " << ss.str() << "\n";
671 : 0 : }
672 : 7174 : std::vector<Node> fassumps;
673 : 7174 : expr::getFreeAssumptions(pfn.get(), fassumps);
674 [ - + ]: 7174 : if (TraceIsOn("sat-proof"))
675 : : {
676 [ - - ]: 0 : for (const Node& fa : fassumps)
677 : : {
678 : 0 : auto it = d_cnfStream->getTranslationCache().find(fa);
679 [ - - ]: 0 : if (it != d_cnfStream->getTranslationCache().end())
680 : : {
681 [ - - ]: 0 : Trace("sat-proof") << "- " << it->second << "\n";
682 [ - - ]: 0 : Trace("sat-proof") << " - " << fa << "\n";
683 : 0 : continue;
684 : : }
685 : : // then it's a clause
686 : 0 : std::stringstream ss;
687 : 0 : Assert(fa.getKind() == Kind::OR);
688 [ - - ]: 0 : for (const Node& n : fa)
689 : : {
690 : 0 : it = d_cnfStream->getTranslationCache().find(n);
691 : 0 : Assert(it != d_cnfStream->getTranslationCache().end());
692 : 0 : ss << it->second << " ";
693 : 0 : }
694 : 0 : Trace("sat-proof") << "- " << ss.str() << "\n";
695 [ - - ]: 0 : Trace("sat-proof") << " - " << fa << "\n";
696 : 0 : }
697 : : }
698 : :
699 : : // for each assumption, see if it has a reason
700 [ + + ]: 650343 : for (const Node& fa : fassumps)
701 : : {
702 : : // ignore already processed assumptions
703 [ + + ]: 643169 : if (premises.count(fa))
704 : : {
705 [ + - ]: 140121 : Trace("sat-proof") << "already processed assumption " << fa << "\n";
706 : 634748 : continue;
707 : : }
708 : : // ignore input assumptions. This is necessary to avoid rare collisions
709 : : // between input clauses and literals that are equivalent at the node
710 : : // level. In trying to justify the literal below, if it was previously
711 : : // propagated (say, in a previous check-sat call that survived the
712 : : // user-context changes) but no longer holds, then we may introduce a
713 : : // bogus proof for it, rather than keeping it as an input.
714 [ + + ]: 503048 : if (d_assumptions.contains(fa))
715 : : {
716 [ + - ]: 494627 : Trace("sat-proof") << "input assumption " << fa << "\n";
717 : 494627 : continue;
718 : : }
719 : : // ignore non-literals
720 : 8421 : auto it = d_cnfStream->getTranslationCache().find(fa);
721 [ - + ]: 8421 : if (it == d_cnfStream->getTranslationCache().end())
722 : : {
723 [ - - ]: 0 : Trace("sat-proof") << "no lit assumption " << fa << "\n";
724 : 0 : premises.insert(fa);
725 : 0 : continue;
726 : : }
727 [ + - ]: 16842 : Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa
728 : 8421 : << "\n";
729 : : // mark another iteration for the loop, as some resolution link may be
730 : : // connected because of the new justifications
731 : 8421 : expanded = true;
732 : 8421 : std::unordered_set<TNode> childPremises;
733 : 8421 : explainLit(it->second, childPremises);
734 : : // add the premises used in the justification. We know they will have
735 : : // been as expanded as possible
736 : 8421 : premises.insert(childPremises.begin(), childPremises.end());
737 : : // add free assumption itself
738 : 8421 : premises.insert(fa);
739 : 8421 : }
740 : 7174 : } while (expanded);
741 : 5961 : }
742 : :
743 : 387 : void SatProofManager::storeUnitConflict(Minisat::Lit inConflict)
744 : : {
745 [ - + ][ - + ]: 387 : Assert(d_conflictLit == undefSatLiteral);
[ - - ]
746 : 387 : d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict);
747 : 387 : }
748 : :
749 : 387 : void SatProofManager::finalizeProof()
750 : : {
751 [ - + ][ - + ]: 387 : Assert(d_conflictLit != undefSatLiteral);
[ - - ]
752 [ + - ]: 774 : Trace("sat-proof")
753 : 0 : << "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
754 : 387 : << d_conflictLit << "\n";
755 : 387 : finalizeProof(d_cnfStream->getNode(d_conflictLit), {d_conflictLit});
756 : : // reset since if in incremental mode this may be used again
757 : 387 : d_conflictLit = undefSatLiteral;
758 : 387 : }
759 : :
760 : 3763 : void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
761 : : {
762 : 3763 : SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
763 [ + - ]: 7526 : Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
764 : 3763 : << satLit << "\n";
765 : 3763 : Node clauseNode = d_cnfStream->getNode(satLit);
766 [ + - ]: 3763 : if (adding)
767 : : {
768 : 7526 : registerSatAssumptions({clauseNode});
769 : : }
770 : 3763 : finalizeProof(clauseNode, {satLit});
771 : 3763 : }
772 : :
773 : 5382 : void SatProofManager::finalizeProof(const Minisat::Clause& inConflict,
774 : : bool adding)
775 : : {
776 [ - + ]: 5382 : if (TraceIsOn("sat-proof"))
777 : : {
778 [ - - ]: 0 : Trace("sat-proof")
779 : 0 : << "SatProofManager::finalizeProof: conflicting clause: ";
780 : 0 : printClause(inConflict);
781 [ - - ]: 0 : Trace("sat-proof") << "\n";
782 : : }
783 : 5382 : std::vector<SatLiteral> clause;
784 [ + + ]: 26703 : for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
785 : : {
786 : 21321 : clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i]));
787 : : }
788 : 5382 : Node clauseNode = getClauseNode(inConflict);
789 [ + + ]: 5382 : if (adding)
790 : : {
791 : 230 : registerSatAssumptions({clauseNode});
792 : : }
793 : 5382 : finalizeProof(clauseNode, clause);
794 : 5382 : }
795 : :
796 : 9417 : std::shared_ptr<ProofNode> SatProofManager::getProof()
797 : : {
798 : 9417 : std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
799 [ + + ]: 9417 : if (!pfn)
800 : : {
801 : 3072 : pfn = d_env.getProofNodeManager()->mkAssume(d_false);
802 : : }
803 : 9417 : return pfn;
804 : 0 : }
805 : :
806 : 75112 : void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
807 : : {
808 [ + - ]: 150224 : Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
809 [ - + ][ - - ]: 75112 : << d_cnfStream->getNode(
810 : 75112 : MinisatSatSolver::toSatLiteral(lit))
811 : 75112 : << "\n";
812 : 75112 : d_assumptions.insert(
813 : 150224 : d_cnfStream->getNode(MinisatSatSolver::toSatLiteral(lit)));
814 : 75112 : }
815 : :
816 : 3860785 : void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
817 : : {
818 [ + + ]: 7721570 : for (const Node& a : assumps)
819 : : {
820 [ + - ]: 7721570 : Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a
821 : 3860785 : << "\n";
822 : 3860785 : d_assumptions.insert(a);
823 : : }
824 : 3860785 : }
825 : :
826 : 100 : void SatProofManager::notifyAssumptionInsertedAtLevel(int level,
827 : : Node assumption)
828 : : {
829 [ - + ][ - + ]: 100 : Assert(d_assumptions.contains(assumption));
[ - - ]
830 : 100 : d_assumptionLevels[level].push_back(assumption);
831 : 100 : }
832 : :
833 : 961 : void SatProofManager::notifyPop()
834 : : {
835 : 961 : for (context::CDHashMap<Node, int>::const_iterator it =
836 : 961 : d_optResLevels.begin();
837 [ + + ]: 1019 : it != d_optResLevels.end();
838 : 58 : ++it)
839 : : {
840 : : // Save into map the proof of the resolution chain. We copy to prevent the
841 : : // proof node saved to be restored of suffering unintended updates. This is
842 : : // *necessary*.
843 : : std::shared_ptr<ProofNode> clauseResPf =
844 : 116 : d_resChains.getProofFor(it->first)->clone();
845 [ + - ][ + - ]: 58 : Assert(clauseResPf && clauseResPf->getRule() != ProofRule::ASSUME);
[ - + ][ - + ]
[ - - ]
846 : 58 : d_optResProofs[it->second].push_back(clauseResPf);
847 : 58 : }
848 : 961 : }
849 : :
850 : 83 : void SatProofManager::notifyCurrPropagationInsertedAtLevel(uint32_t explLevel)
851 : : {
852 [ - + ][ - + ]: 83 : Assert(explLevel < (userContext()->getLevel() - 1));
[ - - ]
853 : 83 : Node currProp = d_ppm->getLastExplainedPropagation();
854 [ - + ][ - + ]: 83 : Assert(!currProp.isNull());
[ - - ]
855 : 83 : LazyCDProof* pf = d_ppm->getCnfProof();
856 [ + - ]: 166 : Trace("cnf") << "Need to save curr propagation " << currProp
857 : 0 : << "'s proof in level " << explLevel + 1
858 : 0 : << " despite being currently in level "
859 : 83 : << userContext()->getLevel() << "\n";
860 : : // Save into map the proof of the processed propagation. Note that
861 : : // propagations must be explained eagerly, since their justification depends
862 : : // on the theory engine and may be different if we only get its proof when the
863 : : // SAT solver pops the user context. Not doing this may lead to open proofs.
864 : : //
865 : : // It's also necessary to copy the proof node, so we prevent unintended
866 : : // updates to the saved proof. Not doing this may also lead to open proofs.
867 : : std::shared_ptr<ProofNode> currPropagationProcPf =
868 : 166 : pf->getProofFor(currProp)->clone();
869 [ - + ][ - + ]: 83 : Assert(currPropagationProcPf->getRule() != ProofRule::ASSUME);
[ - - ]
870 [ + - ]: 166 : Trace("cnf-debug") << "\t..saved pf {" << currPropagationProcPf << "} "
871 : 83 : << *currPropagationProcPf.get() << "\n";
872 : 83 : d_optClausesPfs[explLevel + 1].push_back(currPropagationProcPf);
873 : : // Notify this proof manager that the propagation (which is a SAT assumption)
874 : : // had its level optimized
875 : 83 : notifyAssumptionInsertedAtLevel(explLevel, currProp);
876 : : // Reset
877 : 83 : d_ppm->resetLastExplainedPropagation();
878 : 83 : }
879 : :
880 : 17 : void SatProofManager::notifyClauseInsertedAtLevel(const SatClause& clause,
881 : : uint32_t clLevel)
882 : : {
883 [ + - ]: 34 : Trace("cnf") << "Need to save clause " << clause << " in level "
884 : 0 : << clLevel + 1 << " despite being currently in level "
885 : 17 : << userContext()->getLevel() << "\n";
886 : 17 : LazyCDProof* pf = d_ppm->getCnfProof();
887 : 17 : Node clauseNode = getClauseNode(clause);
888 [ + - ]: 17 : Trace("cnf") << "Node equivalent: " << clauseNode << "\n";
889 [ - + ][ - + ]: 17 : Assert(clLevel < (userContext()->getLevel() - 1));
[ - - ]
890 : : // As above, also justify eagerly.
891 : 34 : std::shared_ptr<ProofNode> clauseCnfPf = pf->getProofFor(clauseNode)->clone();
892 [ - + ][ - + ]: 17 : Assert(clauseCnfPf->getRule() != ProofRule::ASSUME);
[ - - ]
893 : 17 : d_optClausesPfs[clLevel + 1].push_back(clauseCnfPf);
894 : : // Notify SAT proof manager that the propagation (which is a SAT assumption)
895 : : // had its level optimized
896 : 17 : notifyAssumptionInsertedAtLevel(clLevel, clauseNode);
897 : 17 : }
898 : :
899 : 17 : Node SatProofManager::getClauseNode(const SatClause& clause)
900 : : {
901 : 17 : std::vector<Node> clauseNodes;
902 [ + + ]: 111 : for (size_t i = 0, size = clause.size(); i < size; ++i)
903 : : {
904 : 94 : SatLiteral satLit = clause[i];
905 : 94 : clauseNodes.push_back(d_cnfStream->getNode(satLit));
906 : : }
907 : : // order children by node id
908 : 17 : std::sort(clauseNodes.begin(), clauseNodes.end());
909 : 34 : return nodeManager()->mkNode(Kind::OR, clauseNodes);
910 : 17 : }
911 : :
912 : : } // namespace prop
913 : : } // namespace cvc5::internal
|
