diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
| commit | f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b (patch) | |
| tree | a2afaaa295c8964408dd7c53127df61527e00d90 /src/theory/bv | |
| parent | b8a010d260c90efa5433a71dd317a03f051c2592 (diff) | |
adding ::getBooleanVariables to the PropEngine
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bitblaster.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index eb5f3e155..2c45fb603 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -61,7 +61,7 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_statistics() { d_satSolver = prop::SatSolverFactory::createMinisat(c); - d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context()); MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); d_satSolver->setNotify(notify); |