diff options
Diffstat (limited to 'src/proof/resolution_bitvector_proof.h')
-rw-r--r-- | src/proof/resolution_bitvector_proof.h | 58 |
1 files changed, 19 insertions, 39 deletions
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index ccb288f6e..6c2ae589f 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -24,32 +24,16 @@ #include "context/context.h" #include "expr/expr.h" #include "proof/bitvector_proof.h" +#include "proof/sat_proof.h" #include "proof/theory_proof.h" #include "prop/bvminisat/core/Solver.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_types.h" +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" namespace CVC4 { -namespace theory { -namespace bv { -class TheoryBV; -template <class T> -class TBitblaster; -} // namespace bv -} // namespace theory - -// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream -// header cycle and remove this. -namespace prop { -class CnfStream; -} - -} /* namespace CVC4 */ - - -namespace CVC4 { - -template <class Solver> -class TSatProof; typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof; namespace proof { @@ -76,13 +60,7 @@ class ResolutionBitVectorProof : public BitVectorProof BVSatProof* getSatProof(); - /** - * Kind of a mess. - * In eager mode this must be invoked before printing a proof of the empty - * clause. In lazy mode the behavior is ??? - * TODO(aozdemir) clean this up. - */ - void finalizeConflicts(std::vector<Expr>& conflicts); + void finalizeConflicts(std::vector<Expr>& conflicts) override; void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); @@ -91,13 +69,14 @@ class ResolutionBitVectorProof : public BitVectorProof void markAssumptionConflict() { d_isAssumptionConflict = true; } bool isAssumptionConflict() const { return d_isAssumptionConflict; } - virtual void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) = 0; - - void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override; + void initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) override; protected: + void attachToSatSolver(prop::SatSolver& sat_solver) override; + context::Context d_fakeContext; // The CNF formula that results from bit-blasting will need a proof. @@ -106,13 +85,13 @@ class ResolutionBitVectorProof : public BitVectorProof bool d_isAssumptionConflict; - theory::TheoryId getTheoryId() override; }; -class LFSCBitVectorProof : public ResolutionBitVectorProof +class LfscResolutionBitVectorProof : public ResolutionBitVectorProof { public: - LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) : ResolutionBitVectorProof(bv, proofEngine) { } @@ -120,9 +99,10 @@ class LFSCBitVectorProof : public ResolutionBitVectorProof std::ostream& os, std::ostream& paren, const ProofLetMap& map) override; - void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) override; + void printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; void calculateAtomsInBitblastingProof() override; }; |