diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-03 11:56:47 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-03 11:56:47 -0800 |
commit | aa0a875dfd40bd9dfa810238327db51498b74677 (patch) | |
tree | 5606b1214ef8388b86e964213ed3b9c67254317f /src/theory/bv/bitblast/lazy_bitblaster.h | |
parent | 2a19474cdb6761fd4c9aeb0165e661c531ba3e38 (diff) |
Bit vector proof superclass (#2599)
* Split BitvectorProof into a sub/superclass
The superclass contains general printing knowledge.
The subclass contains CNF or Resolution-specific knowledge.
* Renames & code moves
* Nits cleaned in prep for PR
* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof
Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.
* Unique pointers, comments, and code movement.
Adjusted the distribution of code between BVP and RBVP.
Notably, put the CNF proof in BVP because it isn't
resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
BVP's pointer to a CNF proof
RBVP's pointer to a resolution proof
BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`
* clang-format
* Undo manual copyright modification
* s/superclass/base class/
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public
* Andres's Comments
Mostly cleaning up (or trying to clean up) includes.
* Cleaned up one header cycle
However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.
* Added single _s to header gaurds
* Fix Class name in debug output
Credits to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original ordering
Diffstat (limited to 'src/theory/bv/bitblast/lazy_bitblaster.h')
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 5e16b743a..1195d3590 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -19,13 +19,14 @@ #ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H #define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H +#include "proof/resolution_bitvector_proof.h" #include "theory/bv/bitblast/bitblaster.h" #include "context/cdhashmap.h" #include "context/cdlist.h" #include "prop/cnf_stream.h" #include "prop/registrar.h" -#include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" #include "theory/bv/abstraction.h" namespace CVC4 { @@ -76,7 +77,7 @@ class TLazyBitblaster : public TBitblaster<Node> * constants to equivalence classes that don't already have them */ bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setProofLog(proof::ResolutionBitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -106,7 +107,7 @@ class TLazyBitblaster : public TBitblaster<Node> prop::SatLiteralHashFunction> ExplanationMap; /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify + class MinisatNotify : public prop::BVSatSolverNotify { prop::CnfStream* d_cnf; TheoryBV* d_bv; @@ -125,13 +126,14 @@ class TLazyBitblaster : public TBitblaster<Node> }; TheoryBV* d_bv; + proof::ResolutionBitVectorProof* d_bvp; context::Context* d_ctx; std::unique_ptr<prop::NullRegistrar> d_nullRegistrar; std::unique_ptr<context::Context> d_nullContext; // sat solver used for bitblasting and associated CnfStream std::unique_ptr<prop::BVSatSolverInterface> d_satSolver; - std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify; + std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify; std::unique_ptr<prop::CnfStream> d_cnfStream; AssertionList* |