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