From d05aee802bf93d23193739e8280d2ad5ce7e7469 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 25 Sep 2020 12:24:06 -0300 Subject: Cleaning and documenting cnf stream (#5134) Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream. --- src/theory/bv/bitblast/lazy_bitblaster.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'src/theory/bv/bitblast/lazy_bitblaster.cpp') diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index c6590db81..95d78c69b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -80,13 +80,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - nullptr, - rm, - false, - "LazyBitblaster")); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + nullptr, + rm, + false, + "LazyBitblaster")); d_satSolverNotify.reset( d_emptyNotify @@ -575,11 +575,11 @@ void TLazyBitblaster::clearSolver() { d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - nullptr, - rm)); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + nullptr, + rm)); d_satSolverNotify.reset( d_emptyNotify ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() -- cgit v1.2.3