1 /********************* */
2 /*! \file resolution_bitvector_proof.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Paul Meng
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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.\endverbatim
12 ** [[ Add lengthier description here ]]
14 ** \todo document this file
18 #include "proof/resolution_bitvector_proof.h"
19 #include "options/bv_options.h"
20 #include "options/proof_options.h"
21 #include "proof/array_proof.h"
22 #include "proof/bitvector_proof.h"
23 #include "proof/clause_id.h"
24 #include "proof/lfsc_proof_printer.h"
25 #include "proof/proof_output_channel.h"
26 #include "proof/proof_utils.h"
27 #include "proof/sat_proof_implementation.h"
28 #include "prop/bvminisat/bvminisat.h"
29 #include "theory/bv/bitblast/bitblaster.h"
30 #include "theory/bv/theory_bv.h"
31 #include "theory/bv/theory_bv_rewrite_rules.h"
36 using namespace CVC4::theory
;
37 using namespace CVC4::theory::bv
;
43 ResolutionBitVectorProof::ResolutionBitVectorProof(
44 theory::bv::TheoryBV
* bv
, TheoryProofEngine
* proofEngine
)
45 : BitVectorProof(bv
, proofEngine
),
47 d_isAssumptionConflict(false)
51 void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver
* solver
)
53 Assert(d_resolutionProof
== NULL
);
54 d_resolutionProof
.reset(new BVSatProof(solver
, &d_fakeContext
, "bb", true));
57 theory::TheoryId
ResolutionBitVectorProof::getTheoryId()
59 return theory::THEORY_BV
;
62 void ResolutionBitVectorProof::initCnfProof(prop::CnfStream
* cnfStream
,
63 context::Context
* cnf
)
65 Assert(d_resolutionProof
!= NULL
);
66 BitVectorProof::initCnfProof(cnfStream
, cnf
);
68 // true and false have to be setup in a special way
69 Node true_node
= NodeManager::currentNM()->mkConst
<bool>(true);
70 Node false_node
= NodeManager::currentNM()->mkConst
<bool>(false).notNode();
72 d_cnfProof
->pushCurrentAssertion(true_node
);
73 d_cnfProof
->pushCurrentDefinition(true_node
);
74 d_cnfProof
->registerConvertedClause(d_resolutionProof
->getTrueUnit());
75 d_cnfProof
->popCurrentAssertion();
76 d_cnfProof
->popCurrentDefinition();
78 d_cnfProof
->pushCurrentAssertion(false_node
);
79 d_cnfProof
->pushCurrentDefinition(false_node
);
80 d_cnfProof
->registerConvertedClause(d_resolutionProof
->getFalseUnit());
81 d_cnfProof
->popCurrentAssertion();
82 d_cnfProof
->popCurrentDefinition();
85 BVSatProof
* ResolutionBitVectorProof::getSatProof()
87 Assert(d_resolutionProof
!= NULL
);
88 return d_resolutionProof
.get();
91 void ResolutionBitVectorProof::startBVConflict(
92 CVC4::BVMinisat::Solver::TCRef cr
)
94 d_resolutionProof
->startResChain(cr
);
97 void ResolutionBitVectorProof::startBVConflict(
98 CVC4::BVMinisat::Solver::TLit lit
)
100 d_resolutionProof
->startResChain(lit
);
103 void ResolutionBitVectorProof::endBVConflict(
104 const CVC4::BVMinisat::Solver::TLitVec
& confl
)
106 Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict called"
109 std::vector
<Expr
> expr_confl
;
110 for (int i
= 0; i
< confl
.size(); ++i
)
112 prop::SatLiteral lit
= prop::BVMinisatSatSolver::toSatLiteral(confl
[i
]);
113 Expr atom
= d_cnfProof
->getAtom(lit
.getSatVariable()).toExpr();
114 Expr expr_lit
= lit
.isNegated() ? atom
.notExpr() : atom
;
115 expr_confl
.push_back(expr_lit
);
118 Expr conflict
= utils::mkSortedExpr(kind::OR
, expr_confl
);
119 Debug("pf::bv") << "Make conflict for " << conflict
<< std::endl
;
121 if (d_bbConflictMap
.find(conflict
) != d_bbConflictMap
.end())
123 Debug("pf::bv") << "Abort...already conflict for " << conflict
<< std::endl
;
124 // This can only happen when we have eager explanations in the bv solver
125 // if we don't get to propagate p before ~p is already asserted
126 d_resolutionProof
->cancelResChain();
130 // we don't need to check for uniqueness in the sat solver then
131 ClauseId clause_id
= d_resolutionProof
->registerAssumptionConflict(confl
);
132 d_bbConflictMap
[conflict
] = clause_id
;
133 d_resolutionProof
->endResChain(clause_id
);
134 Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict id" << clause_id
135 << " => " << conflict
<< "\n";
136 d_isAssumptionConflict
= false;
139 void ResolutionBitVectorProof::finalizeConflicts(std::vector
<Expr
>& conflicts
)
141 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
143 Debug("pf::bv") << "Construct full proof." << std::endl
;
144 d_resolutionProof
->constructProof();
148 for (unsigned i
= 0; i
< conflicts
.size(); ++i
)
150 Expr confl
= conflicts
[i
];
151 Debug("pf::bv") << "Finalize conflict #" << i
<< ": " << confl
<< std::endl
;
153 // Special case: if the conflict has a (true) or a (not false) in it, it is
155 bool ignoreConflict
= false;
156 if ((confl
.isConst() && confl
.getConst
<bool>())
157 || (confl
.getKind() == kind::NOT
&& confl
[0].isConst()
158 && !confl
[0].getConst
<bool>()))
160 ignoreConflict
= true;
162 else if (confl
.getKind() == kind::OR
)
164 for (unsigned k
= 0; k
< confl
.getNumChildren(); ++k
)
166 if ((confl
[k
].isConst() && confl
[k
].getConst
<bool>())
167 || (confl
[k
].getKind() == kind::NOT
&& confl
[k
][0].isConst()
168 && !confl
[k
][0].getConst
<bool>()))
170 ignoreConflict
= true;
176 Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)"
181 if (d_bbConflictMap
.find(confl
) != d_bbConflictMap
.end())
183 ClauseId id
= d_bbConflictMap
[confl
];
184 d_resolutionProof
->collectClauses(id
);
188 // There is no exact match for our conflict, but maybe it is a subset of
190 ExprToClauseId::const_iterator it
;
191 bool matchFound
= false;
192 for (it
= d_bbConflictMap
.begin(); it
!= d_bbConflictMap
.end(); ++it
)
194 Expr possibleMatch
= it
->first
;
195 if (possibleMatch
.getKind() != kind::OR
)
197 // This is a single-node conflict. If this node is in the conflict
198 // we're trying to prove, we have a match.
199 for (unsigned k
= 0; k
< confl
.getNumChildren(); ++k
)
201 if (confl
[k
] == possibleMatch
)
204 d_resolutionProof
->collectClauses(it
->second
);
211 if (possibleMatch
.getNumChildren() > confl
.getNumChildren()) continue;
214 bool matching
= true;
215 for (unsigned j
= 0; j
< possibleMatch
.getNumChildren(); ++j
)
217 // j is the index in possibleMatch
218 // k is the index in confl
219 while (k
< confl
.getNumChildren() && confl
[k
] != possibleMatch
[j
])
223 if (k
== confl
.getNumChildren())
225 // We couldn't find a match for possibleMatch[j], so not a match
234 << "Collecting info from a sub-conflict" << std::endl
;
235 d_resolutionProof
->collectClauses(it
->second
);
244 Debug("pf::bv") << "Do not collect clauses for " << confl
<< std::endl
245 << "Dumping existing conflicts:" << std::endl
;
248 for (it
= d_bbConflictMap
.begin(); it
!= d_bbConflictMap
.end(); ++it
)
251 Debug("pf::bv") << "\tConflict #" << i
<< ": " << it
->first
261 void LFSCBitVectorProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
264 const ProofLetMap
& map
)
266 Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called"
268 Expr conflict
= utils::mkSortedExpr(kind::OR
, lemma
);
269 Debug("pf::bv") << "\tconflict = " << conflict
<< std::endl
;
271 if (d_bbConflictMap
.find(conflict
) != d_bbConflictMap
.end())
273 std::ostringstream lemma_paren
;
274 for (unsigned i
= 0; i
< lemma
.size(); ++i
)
278 if (lit
.getKind() == kind::NOT
)
280 os
<< "(intro_assump_t _ _ _ ";
284 os
<< "(intro_assump_f _ _ _ ";
287 // print corresponding literal in main sat solver
288 ProofManager
* pm
= ProofManager::currentPM();
289 CnfProof
* cnf
= pm
->getCnfProof();
290 prop::SatLiteral main_lit
= cnf
->getLiteral(lit
);
291 os
<< pm
->getLitName(main_lit
);
293 // print corresponding literal in bv sat solver
294 prop::SatVariable bb_var
= d_cnfProof
->getLiteral(lit
).getSatVariable();
295 os
<< pm
->getAtomName(bb_var
, "bb");
296 os
<< "(\\ unit" << bb_var
<< "\n";
299 Expr lem
= utils::mkOr(lemma
);
300 Assert(d_bbConflictMap
.find(lem
) != d_bbConflictMap
.end());
301 ClauseId lemma_id
= d_bbConflictMap
[lem
];
302 proof::LFSCProofPrinter::printAssumptionsResolution(
303 d_resolutionProof
.get(), lemma_id
, os
, lemma_paren
);
304 os
<< lemma_paren
.str();
308 Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching "
314 ExprToClauseId::const_iterator it
;
316 for (it
= d_bbConflictMap
.begin(); it
!= d_bbConflictMap
.end(); ++it
)
318 // Our conflict is sorted, and the records are also sorted.
320 Expr possibleMatch
= it
->first
;
322 if (possibleMatch
.getKind() != kind::OR
)
324 // This is a single-node conflict. If this node is in the conflict we're
325 // trying to prove, we have a match.
328 for (unsigned k
= 0; k
< conflict
.getNumChildren(); ++k
)
330 if (conflict
[k
] == possibleMatch
)
339 if (possibleMatch
.getNumChildren() > conflict
.getNumChildren())
345 for (unsigned j
= 0; j
< possibleMatch
.getNumChildren(); ++j
)
347 // j is the index in possibleMatch
348 // k is the index in conflict
349 while (k
< conflict
.getNumChildren()
350 && conflict
[k
] != possibleMatch
[j
])
354 if (k
== conflict
.getNumChildren())
356 // We couldn't find a match for possibleMatch[j], so not a match
365 Debug("pf::bv") << "Found a match with conflict #" << i
<< ": "
367 << possibleMatch
<< std::endl
;
368 // The rest is just a copy of the usual handling, if a precise match is
369 // found. We only use the literals that appear in the matching conflict,
370 // though, and not in the original lemma - as these may not have even
372 std::ostringstream lemma_paren
;
374 if (possibleMatch
.getKind() == kind::OR
)
376 for (unsigned i
= 0; i
< possibleMatch
.getNumChildren(); ++i
)
378 Expr lit
= possibleMatch
[i
];
380 if (lit
.getKind() == kind::NOT
)
382 os
<< "(intro_assump_t _ _ _ ";
386 os
<< "(intro_assump_f _ _ _ ";
389 // print corresponding literal in main sat solver
390 ProofManager
* pm
= ProofManager::currentPM();
391 CnfProof
* cnf
= pm
->getCnfProof();
392 prop::SatLiteral main_lit
= cnf
->getLiteral(lit
);
393 os
<< pm
->getLitName(main_lit
);
395 // print corresponding literal in bv sat solver
396 prop::SatVariable bb_var
=
397 d_cnfProof
->getLiteral(lit
).getSatVariable();
398 os
<< pm
->getAtomName(bb_var
, "bb");
399 os
<< "(\\ unit" << bb_var
<< "\n";
405 // The conflict only consists of one node, either positive or
407 Expr lit
= possibleMatch
;
408 if (lit
.getKind() == kind::NOT
)
410 os
<< "(intro_assump_t _ _ _ ";
414 os
<< "(intro_assump_f _ _ _ ";
417 // print corresponding literal in main sat solver
418 ProofManager
* pm
= ProofManager::currentPM();
419 CnfProof
* cnf
= pm
->getCnfProof();
420 prop::SatLiteral main_lit
= cnf
->getLiteral(lit
);
421 os
<< pm
->getLitName(main_lit
);
423 // print corresponding literal in bv sat solver
424 prop::SatVariable bb_var
=
425 d_cnfProof
->getLiteral(lit
).getSatVariable();
426 os
<< pm
->getAtomName(bb_var
, "bb");
427 os
<< "(\\ unit" << bb_var
<< "\n";
431 ClauseId lemma_id
= it
->second
;
432 proof::LFSCProofPrinter::printAssumptionsResolution(
433 d_resolutionProof
.get(), lemma_id
, os
, lemma_paren
);
434 os
<< lemma_paren
.str();
440 // We failed to find a matching sub conflict. The last hope is that the
441 // conflict has a FALSE assertion in it; this can happen in some corner
442 // cases, where the FALSE is the result of a rewrite.
444 for (unsigned i
= 0; i
< lemma
.size(); ++i
)
446 if (lemma
[i
].getKind() == kind::NOT
&& lemma
[i
][0] == utils::mkFalse())
448 Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl
;
449 os
<< "(clausify_false ";
450 os
<< ProofManager::getLitName(lemma
[i
]);
456 Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
457 << "Dumping existing conflicts:" << std::endl
;
460 for (it
= d_bbConflictMap
.begin(); it
!= d_bbConflictMap
.end(); ++it
)
463 Debug("pf::bv") << "\tConflict #" << i
<< ": " << it
->first
<< std::endl
;
470 void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
472 // Collect the input clauses used
473 IdToSatClause used_lemmas
;
474 IdToSatClause used_inputs
;
475 d_resolutionProof
->collectClausesUsed(used_inputs
, used_lemmas
);
476 d_cnfProof
->collectAtomsForClauses(used_inputs
, d_atomsInBitblastingProof
);
477 Assert(used_lemmas
.empty());
480 void LFSCBitVectorProof::printResolutionProof(std::ostream
& os
,
484 // print mapping between theory atoms and internal SAT variables
485 os
<< std::endl
<< ";; BB atom mapping\n" << std::endl
;
487 std::set
<Node
>::iterator atomIt
;
488 Debug("pf::bv") << std::endl
489 << "BV Dumping atoms from inputs: " << std::endl
491 for (atomIt
= d_atomsInBitblastingProof
.begin();
492 atomIt
!= d_atomsInBitblastingProof
.end();
495 Debug("pf::bv") << "\tAtom: " << *atomIt
<< std::endl
;
497 Debug("pf::bv") << std::endl
;
499 // first print bit-blasting
500 printBitblasting(os
, paren
);
502 // print CNF conversion proof for bit-blasted facts
503 IdToSatClause used_lemmas
;
504 IdToSatClause used_inputs
;
505 d_resolutionProof
->collectClausesUsed(used_inputs
, used_lemmas
);
507 d_cnfProof
->printAtomMapping(d_atomsInBitblastingProof
, os
, paren
, letMap
);
508 os
<< std::endl
<< ";; Bit-blasting definitional clauses \n" << std::endl
;
509 for (IdToSatClause::iterator it
= used_inputs
.begin();
510 it
!= used_inputs
.end();
513 d_cnfProof
->printCnfProofForClause(it
->first
, it
->second
, os
, paren
);
516 os
<< std::endl
<< " ;; Bit-blasting learned clauses \n" << std::endl
;
517 proof::LFSCProofPrinter::printResolutions(d_resolutionProof
.get(), os
, paren
);
520 } /* namespace proof */
522 } /* namespace CVC4 */