diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-14 10:53:31 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-14 10:53:31 -0800 |
commit | 23374b9d7fe9363165c99fbbddfd7591302a3431 (patch) | |
tree | b86973ea904e9d6628b4c8a6da0a4619f8b45d51 /src/proof/resolution_bitvector_proof.cpp | |
parent | 300560dda47178cae18f5f4ad2edb381eabddb30 (diff) |
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
Diffstat (limited to 'src/proof/resolution_bitvector_proof.cpp')
-rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 69 |
1 files changed, 36 insertions, 33 deletions
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index 667d630f8..1db673949 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -26,6 +26,7 @@ #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" +#include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_rewrite_rules.h" @@ -54,32 +55,22 @@ void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true)); } -theory::TheoryId ResolutionBitVectorProof::getTheoryId() +void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) { - return theory::THEORY_BV; + Assert(d_resolutionProof != NULL); + Assert(d_cnfProof == nullptr); + d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); + + d_cnfProof->registerTrueUnitClause(d_resolutionProof->getTrueUnit()); + d_cnfProof->registerFalseUnitClause(d_resolutionProof->getFalseUnit()); } -void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf) +void ResolutionBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver) { - Assert(d_resolutionProof != NULL); - BitVectorProof::initCnfProof(cnfStream, cnf); - - // true and false have to be setup in a special way - Node true_node = NodeManager::currentNM()->mkConst<bool>(true); - Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode(); - - d_cnfProof->pushCurrentAssertion(true_node); - d_cnfProof->pushCurrentDefinition(true_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); - - d_cnfProof->pushCurrentAssertion(false_node); - d_cnfProof->pushCurrentDefinition(false_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); + sat_solver.setResolutionProofLog(this); } BVSatProof* ResolutionBitVectorProof::getSatProof() @@ -258,13 +249,15 @@ void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) } } -void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) +void LfscResolutionBitVectorProof::printTheoryLemmaProof( + std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) { - Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" - << std::endl; + Debug("pf::bv") + << "(pf::bv) LfscResolutionBitVectorProof::printTheoryLemmaProof called" + << std::endl; Expr conflict = utils::mkSortedExpr(kind::OR, lemma); Debug("pf::bv") << "\tconflict = " << conflict << std::endl; @@ -467,7 +460,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, } } -void LFSCBitVectorProof::calculateAtomsInBitblastingProof() +void LfscResolutionBitVectorProof::calculateAtomsInBitblastingProof() { // Collect the input clauses used IdToSatClause used_lemmas; @@ -477,9 +470,9 @@ void LFSCBitVectorProof::calculateAtomsInBitblastingProof() Assert(used_lemmas.empty()); } -void LFSCBitVectorProof::printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) +void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) { // print mapping between theory atoms and internal SAT variables os << std::endl << ";; BB atom mapping\n" << std::endl; @@ -517,6 +510,16 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren); } -} /* namespace proof */ +void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os, + std::ostream& paren) +{ + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER, + "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"); + proof::LFSCProofPrinter::printResolutionEmptyClause( + d_resolutionProof.get(), os, paren); +} + +} // namespace proof } /* namespace CVC4 */ |