diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-25 12:24:06 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-25 12:24:06 -0300 |
commit | d05aee802bf93d23193739e8280d2ad5ce7e7469 (patch) | |
tree | 49156d00634f9e9db4279eb6bc2adcdee9ec1bfe /src/theory/bv | |
parent | 96da64b450fc6dd6f5cf701587db38adbe8ba177 (diff) |
Cleaning and documenting cnf stream (#5134)
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 14 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 24 |
2 files changed, 19 insertions, 19 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index c48e20224..046ad4b1b 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -69,13 +69,13 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) } d_satSolver.reset(solver); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_bitblastingRegistrar.get(), - d_nullContext.get(), - nullptr, - rm, - false, - "EagerBitblaster")); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + nullptr, + rm, + false, + "EagerBitblaster")); } EagerBitblaster::~EagerBitblaster() {} 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() |