diff options
Diffstat (limited to 'src/theory/bv/bitblast/lazy_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index a50916413..529f0373b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -19,17 +19,16 @@ #include "theory/bv/bitblast/lazy_bitblaster.h" #include "options/bv_options.h" +#include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" -#include "proof/bitvector_proof.h" -#include "proof/proof_manager.h" -#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -65,6 +64,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bool emptyNotify) : TBitblaster<Node>(), d_bv(bv), + d_bvp(nullptr), d_ctx(c), d_nullRegistrar(new prop::NullRegistrar()), d_nullContext(new context::Context()), @@ -90,8 +90,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); @@ -566,7 +566,8 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ +void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bvp = bvp; d_satSolver->setProofLog( bvp ); bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); @@ -590,8 +591,8 @@ void TLazyBitblaster::clearSolver() { d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), d_bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); } |