1 files changed, 29 insertions, 21 deletions

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 27dccfde0..7dd3fd3e7 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_eager_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Mathias Preiner
+ **   Liana Hadarean, Mathias Preiner, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -27,24 +27,20 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv)
-    : d_assertionSet(),
-      d_bitblaster(nullptr),
-      d_aigBitblaster(nullptr),
+EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv)
+    : d_assertionSet(c),
+      d_assumptionSet(c),
+      d_context(c),
+      d_bitblaster(),
+      d_aigBitblaster(),
       d_useAig(options::bitvectorAig()),
       d_bv(bv),
-      d_bvp(nullptr) {}
-
-EagerBitblastSolver::~EagerBitblastSolver() {
-  if (d_useAig) {
-    Assert(d_bitblaster == nullptr);
-    delete d_aigBitblaster;
-  } else {
-    Assert(d_aigBitblaster == nullptr);
-    delete d_bitblaster;
-  }
+      d_bvp(nullptr)
+{
 }
 
+EagerBitblastSolver::~EagerBitblastSolver() {}
+
 void EagerBitblastSolver::turnOffAig() {
   Assert(d_aigBitblaster == nullptr && d_bitblaster == nullptr);
   d_useAig = false;
@@ -54,15 +50,15 @@ void EagerBitblastSolver::initialize() {
   Assert(!isInitialized());
   if (d_useAig) {
 #ifdef CVC4_USE_ABC
-    d_aigBitblaster = new AigBitblaster();
+    d_aigBitblaster.reset(new AigBitblaster());
 #else
     Unreachable();
 #endif
   } else {
-    d_bitblaster = new EagerBitblaster(d_bv);
+    d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
     THEORY_PROOF(if (d_bvp) {
       d_bitblaster->setProofLog(d_bvp);
-      d_bvp->setBitblaster(d_bitblaster);
+      d_bvp->setBitblaster(d_bitblaster.get());
     });
   }
 }
@@ -79,6 +75,10 @@ void EagerBitblastSolver::assertFormula(TNode formula) {
   Assert(isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula
                            << "\n";
+  if (options::incrementalSolving() && d_context->getLevel() > 1)
+  {
+    d_assumptionSet.insert(formula);
+  }
   d_assertionSet.insert(formula);
   // ensures all atoms are bit-blasted and converted to AIG
   if (d_useAig) {
@@ -87,7 +87,9 @@ void EagerBitblastSolver::assertFormula(TNode formula) {
 #else
     Unreachable();
 #endif
-  } else {
+  }
+  else
+  {
     d_bitblaster->bbFormula(formula);
   }
 }
@@ -100,8 +102,8 @@ bool EagerBitblastSolver::checkSat() {
 
   if (d_useAig) {
 #ifdef CVC4_USE_ABC
-    const std::vector<TNode> assertions = {d_assertionSet.begin(),
-                                           d_assertionSet.end()};
+    const std::vector<Node> assertions = {d_assertionSet.key_begin(),
+                                          d_assertionSet.key_end()};
     Assert(!assertions.empty());
 
     Node query = utils::mkAnd(assertions);
@@ -111,6 +113,12 @@ bool EagerBitblastSolver::checkSat() {
 #endif
   }
 
+  if (options::incrementalSolving())
+  {
+    const std::vector<Node> assumptions = {d_assumptionSet.key_begin(),
+                                           d_assumptionSet.key_end()};
+    return d_bitblaster->solve(assumptions);
+  }
   return d_bitblaster->solve();
 }