1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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/sat_proof_manager.h" |
17 |
|
|
18 |
|
#include "expr/proof_node_algorithm.h" |
19 |
|
#include "options/proof_options.h" |
20 |
|
#include "prop/cnf_stream.h" |
21 |
|
#include "prop/minisat/minisat.h" |
22 |
|
#include "theory/theory_proof_step_buffer.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace prop { |
26 |
|
|
27 |
1197 |
SatProofManager::SatProofManager(Minisat::Solver* solver, |
28 |
|
CnfStream* cnfStream, |
29 |
|
context::UserContext* userContext, |
30 |
1197 |
ProofNodeManager* pnm) |
31 |
|
: d_solver(solver), |
32 |
|
d_cnfStream(cnfStream), |
33 |
|
d_pnm(pnm), |
34 |
|
d_resChains(pnm, true, userContext), |
35 |
|
d_resChainPg(userContext, pnm), |
36 |
|
d_assumptions(userContext), |
37 |
1197 |
d_conflictLit(undefSatVariable) |
38 |
|
{ |
39 |
1197 |
d_true = NodeManager::currentNM()->mkConst(true); |
40 |
1197 |
d_false = NodeManager::currentNM()->mkConst(false); |
41 |
1197 |
} |
42 |
|
|
43 |
|
void SatProofManager::printClause(const Minisat::Clause& clause) |
44 |
|
{ |
45 |
|
for (unsigned i = 0, size = clause.size(); i < size; ++i) |
46 |
|
{ |
47 |
|
SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); |
48 |
|
Trace("sat-proof") << satLit << " "; |
49 |
|
} |
50 |
|
} |
51 |
|
|
52 |
74254 |
Node SatProofManager::getClauseNode(SatLiteral satLit) |
53 |
|
{ |
54 |
74254 |
Assert(d_cnfStream->getNodeCache().find(satLit) |
55 |
|
!= d_cnfStream->getNodeCache().end()) |
56 |
|
<< "SatProofManager::getClauseNode: literal " << satLit |
57 |
|
<< " undefined.\n"; |
58 |
74254 |
return d_cnfStream->getNodeCache()[satLit]; |
59 |
|
} |
60 |
|
|
61 |
756305 |
Node SatProofManager::getClauseNode(const Minisat::Clause& clause) |
62 |
|
{ |
63 |
1512610 |
std::vector<Node> clauseNodes; |
64 |
5051947 |
for (unsigned i = 0, size = clause.size(); i < size; ++i) |
65 |
|
{ |
66 |
4295642 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); |
67 |
4295642 |
Assert(d_cnfStream->getNodeCache().find(satLit) |
68 |
|
!= d_cnfStream->getNodeCache().end()) |
69 |
|
<< "SatProofManager::getClauseNode: literal " << satLit |
70 |
|
<< " undefined\n"; |
71 |
4295642 |
clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]); |
72 |
|
} |
73 |
|
// order children by node id |
74 |
756305 |
std::sort(clauseNodes.begin(), clauseNodes.end()); |
75 |
1512610 |
return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes); |
76 |
|
} |
77 |
|
|
78 |
32874 |
void SatProofManager::startResChain(const Minisat::Clause& start) |
79 |
|
{ |
80 |
32874 |
if (Trace.isOn("sat-proof")) |
81 |
|
{ |
82 |
|
Trace("sat-proof") << "SatProofManager::startResChain: "; |
83 |
|
printClause(start); |
84 |
|
Trace("sat-proof") << "\n"; |
85 |
|
} |
86 |
32874 |
d_resLinks.emplace_back(getClauseNode(start), Node::null(), true); |
87 |
32874 |
} |
88 |
|
|
89 |
207562 |
void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant) |
90 |
|
{ |
91 |
207562 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); |
92 |
415124 |
Node litNode = d_cnfStream->getNodeCache()[satLit]; |
93 |
207562 |
bool negated = satLit.isNegated(); |
94 |
207562 |
Assert(!negated || litNode.getKind() == kind::NOT); |
95 |
207562 |
if (!redundant) |
96 |
|
{ |
97 |
291744 |
Trace("sat-proof") << "SatProofManager::addResolutionStep: {" |
98 |
291744 |
<< satLit.isNegated() << "} [" << satLit << "] " |
99 |
145872 |
<< ~satLit << "\n"; |
100 |
|
// if lit is negated then the chain resolution construction will use it as a |
101 |
|
// pivot occurring as is in the second clause and the node under the |
102 |
|
// negation in the first clause |
103 |
291744 |
d_resLinks.emplace_back(d_cnfStream->getNodeCache()[~satLit], |
104 |
291744 |
negated ? litNode[0] : litNode, |
105 |
437616 |
!satLit.isNegated()); |
106 |
|
} |
107 |
|
else |
108 |
|
{ |
109 |
123380 |
Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit " |
110 |
61690 |
<< satLit << " stored\n"; |
111 |
61690 |
d_redundantLits.push_back(satLit); |
112 |
|
} |
113 |
207562 |
} |
114 |
|
|
115 |
489352 |
void SatProofManager::addResolutionStep(const Minisat::Clause& clause, |
116 |
|
Minisat::Lit lit) |
117 |
|
{ |
118 |
489352 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); |
119 |
978704 |
Node litNode = d_cnfStream->getNodeCache()[satLit]; |
120 |
489352 |
bool negated = satLit.isNegated(); |
121 |
489352 |
Assert(!negated || litNode.getKind() == kind::NOT); |
122 |
978704 |
Node clauseNode = getClauseNode(clause); |
123 |
|
// if lit is negative then the chain resolution construction will use it as a |
124 |
|
// pivot occurring as is in the second clause and the node under the |
125 |
|
// negation in the first clause, which means that the third argument of the |
126 |
|
// tuple must be false |
127 |
489352 |
d_resLinks.emplace_back(clauseNode, negated ? litNode[0] : litNode, negated); |
128 |
489352 |
if (Trace.isOn("sat-proof")) |
129 |
|
{ |
130 |
|
Trace("sat-proof") << "SatProofManager::addResolutionStep: {" |
131 |
|
<< satLit.isNegated() << "} [" << ~satLit << "] "; |
132 |
|
printClause(clause); |
133 |
|
Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t" |
134 |
|
<< clauseNode << "\n"; |
135 |
|
} |
136 |
489352 |
} |
137 |
|
|
138 |
2288 |
void SatProofManager::endResChain(Minisat::Lit lit) |
139 |
|
{ |
140 |
2288 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); |
141 |
4576 |
Trace("sat-proof") << "SatProofManager::endResChain: chain_res for " |
142 |
2288 |
<< satLit; |
143 |
2288 |
endResChain(getClauseNode(satLit), {satLit}); |
144 |
2288 |
} |
145 |
|
|
146 |
30586 |
void SatProofManager::endResChain(const Minisat::Clause& clause) |
147 |
|
{ |
148 |
30586 |
if (Trace.isOn("sat-proof")) |
149 |
|
{ |
150 |
|
Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "; |
151 |
|
printClause(clause); |
152 |
|
} |
153 |
61172 |
std::set<SatLiteral> clauseLits; |
154 |
538284 |
for (unsigned i = 0, size = clause.size(); i < size; ++i) |
155 |
|
{ |
156 |
507698 |
clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i])); |
157 |
|
} |
158 |
30586 |
endResChain(getClauseNode(clause), clauseLits); |
159 |
30586 |
} |
160 |
|
|
161 |
32874 |
void SatProofManager::endResChain(Node conclusion, |
162 |
|
const std::set<SatLiteral>& conclusionLits) |
163 |
|
{ |
164 |
32874 |
Trace("sat-proof") << ", " << conclusion << "\n"; |
165 |
|
// first process redundant literals |
166 |
65605 |
std::set<SatLiteral> visited; |
167 |
32874 |
unsigned pos = d_resLinks.size(); |
168 |
94564 |
for (SatLiteral satLit : d_redundantLits) |
169 |
|
{ |
170 |
61690 |
processRedundantLit(satLit, conclusionLits, visited, pos); |
171 |
|
} |
172 |
32874 |
d_redundantLits.clear(); |
173 |
|
// build resolution chain |
174 |
|
// the conclusion is stored already in the arguments because of the |
175 |
|
// possibility of reordering |
176 |
65605 |
std::vector<Node> children, args{conclusion}; |
177 |
893165 |
for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i) |
178 |
|
{ |
179 |
1720582 |
Node clause, pivot; |
180 |
|
bool posFirst; |
181 |
860291 |
std::tie(clause, pivot, posFirst) = d_resLinks[i]; |
182 |
860291 |
children.push_back(clause); |
183 |
860291 |
Trace("sat-proof") << "SatProofManager::endResChain: "; |
184 |
860291 |
if (i > 0) |
185 |
|
{ |
186 |
1654834 |
Trace("sat-proof") << "{" << posFirst << "} [" |
187 |
827417 |
<< d_cnfStream->getTranslationCache()[pivot] << "] "; |
188 |
|
} |
189 |
|
// special case for clause (or l1 ... ln) being a single literal |
190 |
|
// corresponding itself to a clause, which is indicated by the pivot being |
191 |
|
// of the form (not (or l1 ... ln)) |
192 |
1720582 |
if (clause.getKind() == kind::OR |
193 |
2580873 |
&& !(pivot.getKind() == kind::NOT && pivot[0].getKind() == kind::OR |
194 |
860291 |
&& pivot[0] == clause)) |
195 |
|
{ |
196 |
4285384 |
for (unsigned j = 0, sizeJ = clause.getNumChildren(); j < sizeJ; ++j) |
197 |
|
{ |
198 |
3601175 |
Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause[j]]; |
199 |
3601175 |
if (j < sizeJ - 1) |
200 |
|
{ |
201 |
2916966 |
Trace("sat-proof") << ", "; |
202 |
|
} |
203 |
|
} |
204 |
|
} |
205 |
|
else |
206 |
|
{ |
207 |
352164 |
Assert(d_cnfStream->getTranslationCache().find(clause) |
208 |
|
!= d_cnfStream->getTranslationCache().end()) |
209 |
176082 |
<< "clause node " << clause |
210 |
176082 |
<< " treated as unit has no literal. Pivot is " << pivot << "\n"; |
211 |
176082 |
Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause]; |
212 |
|
} |
213 |
860291 |
Trace("sat-proof") << " : "; |
214 |
860291 |
if (i > 0) |
215 |
|
{ |
216 |
827417 |
args.push_back(posFirst ? d_true : d_false); |
217 |
827417 |
args.push_back(pivot); |
218 |
827417 |
Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] "; |
219 |
|
} |
220 |
860291 |
Trace("sat-proof") << clause << "\n"; |
221 |
|
} |
222 |
|
// clearing |
223 |
32874 |
d_resLinks.clear(); |
224 |
|
// whether no-op |
225 |
32874 |
if (children.size() == 1) |
226 |
|
{ |
227 |
4 |
Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion " |
228 |
2 |
<< conclusion << " is set-equal to premise " |
229 |
2 |
<< children[0] << "\n"; |
230 |
2 |
return; |
231 |
|
} |
232 |
|
// whether trivial cycle |
233 |
892738 |
for (const Node& child : children) |
234 |
|
{ |
235 |
860007 |
if (conclusion == child) |
236 |
|
{ |
237 |
282 |
Trace("sat-proof") |
238 |
141 |
<< "SatProofManager::endResChain: no-op. The conclusion " |
239 |
141 |
<< conclusion << " is equal to a premise\n"; |
240 |
141 |
return; |
241 |
|
} |
242 |
|
} |
243 |
32731 |
if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion)) |
244 |
|
{ |
245 |
|
Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of " |
246 |
|
<< conclusion << "\n"; |
247 |
|
} |
248 |
|
// since the conclusion can be both reordered and without duplicates and the |
249 |
|
// SAT solver does not record this information, we use a MACRO_RESOLUTION |
250 |
|
// step, which bypasses these. Note that we could generate a chain resolution |
251 |
|
// rule here by explicitly computing the detailed steps, but leave this for |
252 |
|
// post-processing. |
253 |
65462 |
ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); |
254 |
|
// note that we must tell the proof generator to overwrite if repeated |
255 |
32731 |
d_resChainPg.addStep(conclusion, ps, CDPOverwrite::ALWAYS); |
256 |
|
// the premises of this resolution may not have been justified yet, so we do |
257 |
|
// not pass assumptions to check closedness |
258 |
32731 |
d_resChains.addLazyStep(conclusion, &d_resChainPg); |
259 |
|
} |
260 |
|
|
261 |
281091 |
void SatProofManager::processRedundantLit( |
262 |
|
SatLiteral lit, |
263 |
|
const std::set<SatLiteral>& conclusionLits, |
264 |
|
std::set<SatLiteral>& visited, |
265 |
|
unsigned pos) |
266 |
|
{ |
267 |
562182 |
Trace("sat-proof") << push |
268 |
281091 |
<< "SatProofManager::processRedundantLit: Lit: " << lit |
269 |
281091 |
<< "\n"; |
270 |
281091 |
if (visited.count(lit)) |
271 |
|
{ |
272 |
88898 |
Trace("sat-proof") << "already visited\n" << pop; |
273 |
208622 |
return; |
274 |
|
} |
275 |
|
Minisat::Solver::TCRef reasonRef = |
276 |
192193 |
d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit))); |
277 |
192193 |
if (reasonRef == Minisat::Solver::TCRef_Undef) |
278 |
|
{ |
279 |
61652 |
Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos |
280 |
30826 |
<< "\n" |
281 |
30826 |
<< pop; |
282 |
30826 |
visited.insert(lit); |
283 |
61652 |
Node litNode = d_cnfStream->getNodeCache()[lit]; |
284 |
30826 |
bool negated = lit.isNegated(); |
285 |
30826 |
Assert(!negated || litNode.getKind() == kind::NOT); |
286 |
|
|
287 |
92478 |
d_resLinks.emplace(d_resLinks.begin() + pos, |
288 |
61652 |
d_cnfStream->getNodeCache()[~lit], |
289 |
61652 |
negated ? litNode[0] : litNode, |
290 |
154130 |
!negated); |
291 |
30826 |
return; |
292 |
|
} |
293 |
161367 |
Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size()) |
294 |
|
<< "reasonRef " << reasonRef << " and d_satSolver->ca.size() " |
295 |
|
<< d_solver->ca.size() << "\n"; |
296 |
161367 |
const Minisat::Clause& reason = d_solver->ca[reasonRef]; |
297 |
161367 |
if (Trace.isOn("sat-proof")) |
298 |
|
{ |
299 |
|
Trace("sat-proof") << "reason: "; |
300 |
|
printClause(reason); |
301 |
|
Trace("sat-proof") << "\n"; |
302 |
|
} |
303 |
|
// check if redundant literals in the reason. The first literal is the one we |
304 |
|
// will be eliminating, so we check the others |
305 |
481964 |
for (unsigned i = 1, size = reason.size(); i < size; ++i) |
306 |
|
{ |
307 |
320597 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]); |
308 |
|
// if literal does not occur in the conclusion we process it as well |
309 |
320597 |
if (!conclusionLits.count(satLit)) |
310 |
|
{ |
311 |
219401 |
processRedundantLit(satLit, conclusionLits, visited, pos); |
312 |
|
} |
313 |
|
} |
314 |
161367 |
Assert(!visited.count(lit)); |
315 |
161367 |
visited.insert(lit); |
316 |
322734 |
Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos |
317 |
161367 |
<< "\n" |
318 |
161367 |
<< pop; |
319 |
|
// add the step before steps for children. Note that the step is with the |
320 |
|
// reason, not only with ~lit, since the learned clause is built under the |
321 |
|
// assumption that the redundant literal is removed via the resolution with |
322 |
|
// the explanation of its negation |
323 |
322734 |
Node clauseNode = getClauseNode(reason); |
324 |
322734 |
Node litNode = d_cnfStream->getNodeCache()[lit]; |
325 |
161367 |
bool negated = lit.isNegated(); |
326 |
161367 |
Assert(!negated || litNode.getKind() == kind::NOT); |
327 |
484101 |
d_resLinks.emplace(d_resLinks.begin() + pos, |
328 |
|
clauseNode, |
329 |
322734 |
negated ? litNode[0] : litNode, |
330 |
645468 |
!negated); |
331 |
|
} |
332 |
|
|
333 |
23647 |
void SatProofManager::explainLit(SatLiteral lit, |
334 |
|
std::unordered_set<TNode>& premises) |
335 |
|
{ |
336 |
23647 |
Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit; |
337 |
34893 |
Node litNode = getClauseNode(lit); |
338 |
23647 |
Trace("sat-proof") << " [" << litNode << "]\n"; |
339 |
23647 |
if (d_resChainPg.hasProofFor(litNode)) |
340 |
|
{ |
341 |
13918 |
Trace("sat-proof") << "SatProofManager::explainLit: already justified " |
342 |
6959 |
<< lit << ", ABORT\n" |
343 |
6959 |
<< pop; |
344 |
6959 |
return; |
345 |
|
} |
346 |
|
Minisat::Solver::TCRef reasonRef = |
347 |
16688 |
d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit))); |
348 |
16688 |
if (reasonRef == Minisat::Solver::TCRef_Undef) |
349 |
|
{ |
350 |
5440 |
Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop; |
351 |
5440 |
return; |
352 |
|
} |
353 |
11248 |
Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size()) |
354 |
|
<< "reasonRef " << reasonRef << " and d_satSolver->ca.size() " |
355 |
|
<< d_solver->ca.size() << "\n"; |
356 |
11248 |
const Minisat::Clause& reason = d_solver->ca[reasonRef]; |
357 |
11248 |
unsigned size = reason.size(); |
358 |
11248 |
if (Trace.isOn("sat-proof")) |
359 |
|
{ |
360 |
|
Trace("sat-proof") << "SatProofManager::explainLit: with clause: "; |
361 |
|
printClause(reason); |
362 |
|
Trace("sat-proof") << "\n"; |
363 |
|
} |
364 |
|
#ifdef CVC5_ASSERTIONS |
365 |
|
// pedantically check that the negation of the literal to explain *does not* |
366 |
|
// occur in the reason, otherwise we will loop forever |
367 |
41311 |
for (unsigned i = 0; i < size; ++i) |
368 |
|
{ |
369 |
30063 |
AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit) |
370 |
|
<< "cyclic justification\n"; |
371 |
|
} |
372 |
|
#endif |
373 |
|
// add the reason clause first |
374 |
22494 |
std::vector<Node> children{getClauseNode(reason)}, args; |
375 |
|
// save in the premises |
376 |
11248 |
premises.insert(children.back()); |
377 |
|
// Since explainLit calls can reallocate memory in the |
378 |
|
// SAT solver, we directly get the literals we need to explain so we no |
379 |
|
// longer depend on the reference to reason |
380 |
22494 |
std::vector<Node> toExplain{children.back().begin(), children.back().end()}; |
381 |
11248 |
Trace("sat-proof") << push; |
382 |
41311 |
for (unsigned i = 0; i < size; ++i) |
383 |
|
{ |
384 |
|
#ifdef CVC5_ASSERTIONS |
385 |
|
// pedantically make sure that the reason stays the same |
386 |
30063 |
const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef]; |
387 |
30063 |
AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size())); |
388 |
30063 |
AlwaysAssert(children[0] == getClauseNode(reloadedReason)); |
389 |
|
#endif |
390 |
30063 |
SatLiteral currLit = d_cnfStream->getTranslationCache()[toExplain[i]]; |
391 |
|
// ignore the lit we are trying to explain... |
392 |
30063 |
if (currLit == lit) |
393 |
|
{ |
394 |
11248 |
continue; |
395 |
|
} |
396 |
37630 |
std::unordered_set<TNode> childPremises; |
397 |
18815 |
explainLit(~currLit, childPremises); |
398 |
|
// save to resolution chain premises / arguments |
399 |
18815 |
Assert(d_cnfStream->getNodeCache().find(currLit) |
400 |
|
!= d_cnfStream->getNodeCache().end()); |
401 |
18815 |
children.push_back(d_cnfStream->getNodeCache()[~currLit]); |
402 |
37630 |
Node currLitNode = d_cnfStream->getNodeCache()[currLit]; |
403 |
18815 |
bool negated = currLit.isNegated(); |
404 |
18815 |
Assert(!negated || currLitNode.getKind() == kind::NOT); |
405 |
|
// note this is the opposite of what is done in addResolutionStep. This is |
406 |
|
// because here the clause, which contains the literal being analyzed, is |
407 |
|
// the first clause rather than the second |
408 |
18815 |
args.push_back(!negated ? d_true : d_false); |
409 |
18815 |
args.push_back(negated ? currLitNode[0] : currLitNode); |
410 |
|
// add child premises and the child itself |
411 |
18815 |
premises.insert(childPremises.begin(), childPremises.end()); |
412 |
18815 |
premises.insert(d_cnfStream->getNodeCache()[~currLit]); |
413 |
|
} |
414 |
11248 |
if (Trace.isOn("sat-proof")) |
415 |
|
{ |
416 |
|
Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for " |
417 |
|
<< lit << ", " << litNode << " with clauses:\n"; |
418 |
|
for (unsigned i = 0, csize = children.size(); i < csize; ++i) |
419 |
|
{ |
420 |
|
Trace("sat-proof") << "SatProofManager::explainLit: " << children[i]; |
421 |
|
if (i > 0) |
422 |
|
{ |
423 |
|
Trace("sat-proof") << " [" << args[i - 1] << "]"; |
424 |
|
} |
425 |
|
Trace("sat-proof") << "\n"; |
426 |
|
} |
427 |
|
} |
428 |
|
// if justification of children contains the expected conclusion, avoid the |
429 |
|
// cyclic proof by aborting. |
430 |
11248 |
if (premises.count(litNode)) |
431 |
|
{ |
432 |
4 |
Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit |
433 |
2 |
<< " [" << litNode << "], ABORT\n" |
434 |
2 |
<< pop; |
435 |
2 |
return; |
436 |
|
} |
437 |
11246 |
Trace("sat-proof") << pop; |
438 |
|
// create step |
439 |
11246 |
args.insert(args.begin(), litNode); |
440 |
22492 |
ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); |
441 |
11246 |
d_resChainPg.addStep(litNode, ps); |
442 |
|
// the premises in the limit of the justification may correspond to other |
443 |
|
// links in the chain which have, themselves, literals yet to be justified. So |
444 |
|
// we are not ready yet to check closedness w.r.t. CNF transformation of the |
445 |
|
// preprocessed assertions |
446 |
11246 |
d_resChains.addLazyStep(litNode, &d_resChainPg); |
447 |
|
} |
448 |
|
|
449 |
1302 |
void SatProofManager::finalizeProof(Node inConflictNode, |
450 |
|
const std::vector<SatLiteral>& inConflict) |
451 |
|
{ |
452 |
2604 |
Trace("sat-proof") |
453 |
1302 |
<< "SatProofManager::finalizeProof: conflicting clause node: " |
454 |
1302 |
<< inConflictNode << "\n"; |
455 |
|
// nothing to do |
456 |
1302 |
if (inConflictNode == d_false) |
457 |
|
{ |
458 |
389 |
return; |
459 |
|
} |
460 |
913 |
if (Trace.isOn("sat-proof-debug2")) |
461 |
|
{ |
462 |
|
Trace("sat-proof-debug2") |
463 |
|
<< push << "SatProofManager::finalizeProof: saved proofs in chain:\n"; |
464 |
|
std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks(); |
465 |
|
std::unordered_set<Node> skip; |
466 |
|
for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links) |
467 |
|
{ |
468 |
|
if (skip.count(link.first)) |
469 |
|
{ |
470 |
|
continue; |
471 |
|
} |
472 |
|
auto it = d_cnfStream->getTranslationCache().find(link.first); |
473 |
|
if (it != d_cnfStream->getTranslationCache().end()) |
474 |
|
{ |
475 |
|
Trace("sat-proof-debug2") |
476 |
|
<< "SatProofManager::finalizeProof: " << it->second; |
477 |
|
} |
478 |
|
// a refl step added due to double elim negation, ignore |
479 |
|
else if (link.second->getRule() == PfRule::REFL) |
480 |
|
{ |
481 |
|
continue; |
482 |
|
} |
483 |
|
// a clause |
484 |
|
else |
485 |
|
{ |
486 |
|
Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:"; |
487 |
|
Assert(link.first.getKind() == kind::OR) << link.first; |
488 |
|
for (const Node& n : link.first) |
489 |
|
{ |
490 |
|
it = d_cnfStream->getTranslationCache().find(n); |
491 |
|
Assert(it != d_cnfStream->getTranslationCache().end()); |
492 |
|
Trace("sat-proof-debug2") << it->second << " "; |
493 |
|
} |
494 |
|
} |
495 |
|
Trace("sat-proof-debug2") << "\n"; |
496 |
|
Trace("sat-proof-debug2") |
497 |
|
<< "SatProofManager::finalizeProof: " << link.first << "\n"; |
498 |
|
// get resolution |
499 |
|
Node cur = link.first; |
500 |
|
std::shared_ptr<ProofNode> pfn = link.second; |
501 |
|
while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST) |
502 |
|
{ |
503 |
|
Assert(pfn->getChildren().size() == 1 |
504 |
|
&& pfn->getChildren()[0]->getRule() == PfRule::ASSUME) |
505 |
|
<< *link.second.get() << "\n" |
506 |
|
<< *pfn.get(); |
507 |
|
cur = pfn->getChildren()[0]->getResult(); |
508 |
|
// retrieve justification of assumption in the links |
509 |
|
Assert(links.find(cur) != links.end()); |
510 |
|
pfn = links[cur]; |
511 |
|
// ignore it in the rest of the outside loop |
512 |
|
skip.insert(cur); |
513 |
|
} |
514 |
|
std::vector<Node> fassumps; |
515 |
|
expr::getFreeAssumptions(pfn.get(), fassumps); |
516 |
|
Trace("sat-proof-debug2") << push; |
517 |
|
for (const Node& fa : fassumps) |
518 |
|
{ |
519 |
|
Trace("sat-proof-debug2") << "SatProofManager::finalizeProof: - "; |
520 |
|
it = d_cnfStream->getTranslationCache().find(fa); |
521 |
|
if (it != d_cnfStream->getTranslationCache().end()) |
522 |
|
{ |
523 |
|
Trace("sat-proof-debug2") << it->second << "\n"; |
524 |
|
continue; |
525 |
|
} |
526 |
|
// then it's a clause |
527 |
|
Assert(fa.getKind() == kind::OR); |
528 |
|
for (const Node& n : fa) |
529 |
|
{ |
530 |
|
it = d_cnfStream->getTranslationCache().find(n); |
531 |
|
Assert(it != d_cnfStream->getTranslationCache().end()); |
532 |
|
Trace("sat-proof-debug2") << it->second << " "; |
533 |
|
} |
534 |
|
Trace("sat-proof-debug2") << "\n"; |
535 |
|
} |
536 |
|
Trace("sat-proof-debug2") << pop; |
537 |
|
Trace("sat-proof-debug2") |
538 |
|
<< "SatProofManager::finalizeProof: " << *pfn.get() << "\n=======\n"; |
539 |
|
; |
540 |
|
} |
541 |
|
Trace("sat-proof-debug2") << pop; |
542 |
|
} |
543 |
|
// We will resolve away of the literals l_1...l_n in inConflict. At this point |
544 |
|
// each ~l_i must be either explainable, the result of a previously saved |
545 |
|
// resolution chain, or an input. In account of it possibly being the first, |
546 |
|
// we call explainLit on each ~l_i while accumulating the children and |
547 |
|
// arguments for the resolution step to conclude false. |
548 |
1826 |
std::vector<Node> children{inConflictNode}, args; |
549 |
1826 |
std::unordered_set<TNode> premises; |
550 |
4669 |
for (unsigned i = 0, size = inConflict.size(); i < size; ++i) |
551 |
|
{ |
552 |
3756 |
Assert(d_cnfStream->getNodeCache().find(inConflict[i]) |
553 |
|
!= d_cnfStream->getNodeCache().end()); |
554 |
7512 |
std::unordered_set<TNode> childPremises; |
555 |
3756 |
explainLit(~inConflict[i], childPremises); |
556 |
7512 |
Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]]; |
557 |
|
// save to resolution chain premises / arguments |
558 |
3756 |
children.push_back(negatedLitNode); |
559 |
7512 |
Node litNode = d_cnfStream->getNodeCache()[inConflict[i]]; |
560 |
3756 |
bool negated = inConflict[i].isNegated(); |
561 |
3756 |
Assert(!negated || litNode.getKind() == kind::NOT); |
562 |
|
// note this is the opposite of what is done in addResolutionStep. This is |
563 |
|
// because here the clause, which contains the literal being analyzed, is |
564 |
|
// the first clause rather than the second |
565 |
3756 |
args.push_back(!negated ? d_true : d_false); |
566 |
3756 |
args.push_back(negated ? litNode[0] : litNode); |
567 |
|
// add child premises and the child itself |
568 |
3756 |
premises.insert(childPremises.begin(), childPremises.end()); |
569 |
3756 |
premises.insert(negatedLitNode); |
570 |
3756 |
Trace("sat-proof") << "===========\n"; |
571 |
|
} |
572 |
913 |
if (Trace.isOn("sat-proof")) |
573 |
|
{ |
574 |
|
Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false " |
575 |
|
"with clauses:\n"; |
576 |
|
for (unsigned i = 0, size = children.size(); i < size; ++i) |
577 |
|
{ |
578 |
|
Trace("sat-proof") << "SatProofManager::finalizeProof: " << children[i]; |
579 |
|
if (i > 0) |
580 |
|
{ |
581 |
|
Trace("sat-proof") << " [" << args[i - 1] << "]"; |
582 |
|
} |
583 |
|
Trace("sat-proof") << "\n"; |
584 |
|
} |
585 |
|
} |
586 |
|
// create step |
587 |
913 |
args.insert(args.begin(), d_false); |
588 |
1826 |
ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); |
589 |
913 |
d_resChainPg.addStep(d_false, ps); |
590 |
|
// not yet ready to check closedness because maybe only now we will justify |
591 |
|
// literals used in resolutions |
592 |
913 |
d_resChains.addLazyStep(d_false, &d_resChainPg); |
593 |
|
// Fix point justification of literals in leaves of the proof of false |
594 |
|
bool expanded; |
595 |
1132 |
do |
596 |
|
{ |
597 |
1132 |
expanded = false; |
598 |
1132 |
Trace("sat-proof") << "expand assumptions to prove false\n"; |
599 |
2264 |
std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false); |
600 |
1132 |
Assert(pfn); |
601 |
1132 |
Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n"; |
602 |
2264 |
std::vector<Node> fassumps; |
603 |
1132 |
expr::getFreeAssumptions(pfn.get(), fassumps); |
604 |
1132 |
if (Trace.isOn("sat-proof")) |
605 |
|
{ |
606 |
|
for (const Node& fa : fassumps) |
607 |
|
{ |
608 |
|
Trace("sat-proof") << "- "; |
609 |
|
auto it = d_cnfStream->getTranslationCache().find(fa); |
610 |
|
if (it != d_cnfStream->getTranslationCache().end()) |
611 |
|
{ |
612 |
|
Trace("sat-proof") << it->second << "\n"; |
613 |
|
Trace("sat-proof") << "- " << fa << "\n"; |
614 |
|
continue; |
615 |
|
} |
616 |
|
// then it's a clause |
617 |
|
Assert(fa.getKind() == kind::OR); |
618 |
|
for (const Node& n : fa) |
619 |
|
{ |
620 |
|
it = d_cnfStream->getTranslationCache().find(n); |
621 |
|
Assert(it != d_cnfStream->getTranslationCache().end()); |
622 |
|
Trace("sat-proof") << it->second << " "; |
623 |
|
} |
624 |
|
Trace("sat-proof") << "\n"; |
625 |
|
Trace("sat-proof") << "- " << fa << "\n"; |
626 |
|
} |
627 |
|
} |
628 |
|
|
629 |
|
// for each assumption, see if it has a reason |
630 |
92483 |
for (const Node& fa : fassumps) |
631 |
|
{ |
632 |
|
// ignore already processed assumptions |
633 |
111965 |
if (premises.count(fa)) |
634 |
|
{ |
635 |
20614 |
Trace("sat-proof") << "already processed assumption " << fa << "\n"; |
636 |
110889 |
continue; |
637 |
|
} |
638 |
|
// ignore input assumptions. This is necessary to avoid rare collisions |
639 |
|
// between input clauses and literals that are equivalent at the node |
640 |
|
// level. In trying to justify the literal below if, it was previously |
641 |
|
// propagated (say, in a previous check-sat call that survived the |
642 |
|
// user-context changes) but no longer holds, then we may introduce a |
643 |
|
// bogus proof for it, rather than keeping it as an input. |
644 |
140395 |
if (d_assumptions.contains(fa)) |
645 |
|
{ |
646 |
69658 |
Trace("sat-proof") << "input assumption " << fa << "\n"; |
647 |
69658 |
continue; |
648 |
|
} |
649 |
|
// ignore non-literals |
650 |
1079 |
auto it = d_cnfStream->getTranslationCache().find(fa); |
651 |
1082 |
if (it == d_cnfStream->getTranslationCache().end()) |
652 |
|
{ |
653 |
3 |
Trace("sat-proof") << "no lit assumption " << fa << "\n"; |
654 |
3 |
premises.insert(fa); |
655 |
3 |
continue; |
656 |
|
} |
657 |
2152 |
Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa |
658 |
1076 |
<< "\n"; |
659 |
|
// mark another iteration for the loop, as some resolution link may be |
660 |
|
// connected because of the new justifications |
661 |
1076 |
expanded = true; |
662 |
2152 |
std::unordered_set<TNode> childPremises; |
663 |
1076 |
explainLit(it->second, childPremises); |
664 |
|
// add the premises used in the justification. We know they will have |
665 |
|
// been as expanded as possible |
666 |
1076 |
premises.insert(childPremises.begin(), childPremises.end()); |
667 |
|
// add free assumption itself |
668 |
1076 |
premises.insert(fa); |
669 |
|
} |
670 |
|
} while (expanded); |
671 |
|
// now we should be able to close it |
672 |
913 |
if (options::proofEagerChecking()) |
673 |
|
{ |
674 |
|
std::vector<Node> assumptionsVec; |
675 |
|
for (const Node& a : d_assumptions) |
676 |
|
{ |
677 |
|
assumptionsVec.push_back(a); |
678 |
|
} |
679 |
|
d_resChains.addLazyStep(d_false, &d_resChainPg, assumptionsVec); |
680 |
|
} |
681 |
|
} |
682 |
|
|
683 |
44 |
void SatProofManager::storeUnitConflict(Minisat::Lit inConflict) |
684 |
|
{ |
685 |
44 |
Assert(d_conflictLit == undefSatVariable); |
686 |
44 |
d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict); |
687 |
44 |
} |
688 |
|
|
689 |
44 |
void SatProofManager::finalizeProof() |
690 |
|
{ |
691 |
44 |
Assert(d_conflictLit != undefSatVariable); |
692 |
88 |
Trace("sat-proof") |
693 |
44 |
<< "SatProofManager::finalizeProof: conflicting (lazy) satLit: " |
694 |
44 |
<< d_conflictLit << "\n"; |
695 |
44 |
finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit}); |
696 |
44 |
} |
697 |
|
|
698 |
443 |
void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding) |
699 |
|
{ |
700 |
443 |
SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict); |
701 |
886 |
Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: " |
702 |
443 |
<< satLit << "\n"; |
703 |
886 |
Node clauseNode = getClauseNode(satLit); |
704 |
443 |
if (adding) |
705 |
|
{ |
706 |
443 |
registerSatAssumptions({clauseNode}); |
707 |
|
} |
708 |
443 |
finalizeProof(clauseNode, {satLit}); |
709 |
443 |
} |
710 |
|
|
711 |
815 |
void SatProofManager::finalizeProof(const Minisat::Clause& inConflict, |
712 |
|
bool adding) |
713 |
|
{ |
714 |
815 |
if (Trace.isOn("sat-proof")) |
715 |
|
{ |
716 |
|
Trace("sat-proof") |
717 |
|
<< "SatProofManager::finalizeProof: conflicting clause: "; |
718 |
|
printClause(inConflict); |
719 |
|
Trace("sat-proof") << "\n"; |
720 |
|
} |
721 |
1630 |
std::vector<SatLiteral> clause; |
722 |
4473 |
for (unsigned i = 0, size = inConflict.size(); i < size; ++i) |
723 |
|
{ |
724 |
3658 |
clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i])); |
725 |
|
} |
726 |
1630 |
Node clauseNode = getClauseNode(inConflict); |
727 |
815 |
if (adding) |
728 |
|
{ |
729 |
18 |
registerSatAssumptions({clauseNode}); |
730 |
|
} |
731 |
815 |
finalizeProof(clauseNode, clause); |
732 |
815 |
} |
733 |
|
|
734 |
2698 |
std::shared_ptr<ProofNode> SatProofManager::getProof() |
735 |
|
{ |
736 |
2698 |
std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false); |
737 |
2698 |
if (!pfn) |
738 |
|
{ |
739 |
810 |
pfn = d_pnm->mkAssume(d_false); |
740 |
|
} |
741 |
2698 |
return pfn; |
742 |
|
} |
743 |
|
|
744 |
23916 |
void SatProofManager::registerSatLitAssumption(Minisat::Lit lit) |
745 |
|
{ |
746 |
47832 |
Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - " |
747 |
47832 |
<< getClauseNode(MinisatSatSolver::toSatLiteral(lit)) |
748 |
23916 |
<< "\n"; |
749 |
23916 |
d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit))); |
750 |
23916 |
} |
751 |
|
|
752 |
407232 |
void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps) |
753 |
|
{ |
754 |
814464 |
for (const Node& a : assumps) |
755 |
|
{ |
756 |
814464 |
Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a |
757 |
407232 |
<< "\n"; |
758 |
407232 |
d_assumptions.insert(a); |
759 |
|
} |
760 |
407232 |
} |
761 |
|
|
762 |
|
} // namespace prop |
763 |
28191 |
} // namespace cvc5 |