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/bitblast/lazy_bitblaster.cpp | |
| 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/bitblast/lazy_bitblaster.cpp')
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
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() |