diff options
Diffstat (limited to 'src/theory/bv/bitblast/lazy_bitblaster.h')
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 1195d3590..9af74d8db 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -77,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(proof::ResolutionBitVectorProof* bvp); + void setProofLog(proof::BitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -126,15 +126,11 @@ 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::BVSatSolverNotify> d_satSolverNotify; - std::unique_ptr<prop::CnfStream> d_cnfStream; AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms @@ -155,6 +151,7 @@ class TLazyBitblaster : public TBitblaster<Node> void addAtom(TNode atom); bool hasValue(TNode a); Node getModelFromSatSolver(TNode a, bool fullModel) override; + prop::SatSolver* getSatSolver() override { return d_satSolver.get(); } class Statistics { |