Add support for incremental eager bit-blasting. (#1838)

Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.

13 files changed, 136 insertions, 74 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b48647116..a72eb2c30 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1088,12 +1088,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
     return theory::bv::SAT_SOLVER_MINISAT;
   } else if(optarg == "cryptominisat") {
     
-    if (options::incrementalSolving() &&
-        options::incrementalSolving.wasSetByUser()) {
-      throw OptionException(std::string("CryptoMinSat does not support incremental mode. \n\
-                                         Try --bv-sat-solver=minisat"));
-    }
-
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
         options::bitblastMode.wasSetByUser()) {
       throw OptionException(
@@ -1103,12 +1097,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
     if (!options::bitvectorToBool.wasSetByUser()) {
       options::bitvectorToBool.set(true);
     }
-
-    // if (!options::bvAbstraction.wasSetByUser() &&
-    //     !options::skolemizeArguments.wasSetByUser()) {
-    //   options::bvAbstraction.set(true);
-    //   options::skolemizeArguments.set(true); 
-    // }
     return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
   }
   else if (optarg == "cadical")
@@ -1118,7 +1106,8 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
     {
       throw OptionException(
           std::string("CaDiCaL does not support incremental mode. \n\
-                                         Try --bv-sat-solver=minisat"));
+                         Try --bv-sat-solver=cryptominisat or "
+                      "--bv-sat-solver=minisat"));
     }
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
@@ -1126,7 +1115,7 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
     {
       throw OptionException(
           std::string("CaDiCaL does not support lazy bit-blasting. \n\
-                                         Try --bv-sat-solver=minisat"));
+                         Try --bv-sat-solver=minisat"));
     }
     if (!options::bitvectorToBool.wasSetByUser())
     {
@@ -1180,12 +1169,6 @@ theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
     }
     return theory::bv::BITBLAST_MODE_LAZY;
   } else if(optarg == "eager") {
-
-    if (options::incrementalSolving() &&
-        options::incrementalSolving.wasSetByUser()) {
-      throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
-                                         Try --bitblast=lazy"));
-    }
     if (!options::bitvectorToBool.wasSetByUser()) {
       options::bitvectorToBool.set(true);
     }
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 4f239343e..df5a20791 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -164,6 +164,18 @@ SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
   return solve();
 }
 
+SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  std::vector<CMSat::Lit> assumpts;
+  for (const SatLiteral& lit : assumptions)
+  {
+    assumpts.push_back(toInternalLit(lit));
+  }
+  ++d_statistics.d_statCallsToSolve;
+  return toSatLiteralValue(d_solver->solve(&assumpts));
+}
+
 SatValue CryptoMinisatSolver::value(SatLiteral l){
   const std::vector<CMSat::lbool> model = d_solver->get_model();
   CMSatVar var = l.getSatVariable();
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index c265b2f35..c5345cb86 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -64,6 +64,8 @@ public:
   
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+
   bool ok() const override;
   SatValue value(SatLiteral l) override;
   SatValue modelValue(SatLiteral l) override;
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 055efa413..add73eebe 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -76,6 +76,12 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
+  /** Check satisfiability under assumptions */
+  virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
+  {
+    Unimplemented("Solving under assumptions not implemented");
+  };
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5296a3bca..de4537807 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1318,18 +1318,6 @@ void SmtEngine::setDefaults() {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
   {
-    if (options::incrementalSolving())
-    {
-      if (options::incrementalSolving.wasSetByUser())
-      {
-        throw OptionException(std::string(
-            "Eager bit-blasting does not currently support incremental mode. "
-            "Try --bitblast=lazy"));
-      }
-      Notice() << "SmtEngine: turning off incremental to support eager "
-               << "bit-blasting" << endl;
-      setOption("incremental", SExpr("false"));
-    }
     if (options::produceModels()
         && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
             || d_logic.isTheoryEnabled(THEORY_UF)))
@@ -4160,7 +4148,8 @@ void SmtEnginePrivate::processAssertions() {
                          "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
 
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+      && !options::incrementalSolving())
   {
     d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions);
   }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 7b12c3465..01437cb64 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -30,8 +30,9 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
+EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     : TBitblaster<Node>(),
+      d_context(c),
       d_nullContext(new context::Context()),
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
@@ -75,9 +76,18 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
 
 EagerBitblaster::~EagerBitblaster() {}
 
-void EagerBitblaster::bbFormula(TNode node) {
-  d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID,
-                                TNode::null());
+void EagerBitblaster::bbFormula(TNode node)
+{
+  /* For incremental eager solving we assume formulas at context levels > 1. */
+  if (options::incrementalSolving() && d_context->getLevel() > 1)
+  {
+    d_cnfStream->ensureLiteral(node);
+  }
+  else
+  {
+    d_cnfStream->convertAndAssert(
+        node, false, false, RULE_INVALID, TNode::null());
+  }
 }
 
 /**
@@ -185,6 +195,17 @@ bool EagerBitblaster::solve() {
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
+bool EagerBitblaster::solve(const std::vector<Node>& assumptions)
+{
+  std::vector<prop::SatLiteral> assumpts;
+  for (const Node& assumption : assumptions)
+  {
+    Assert(d_cnfStream->hasLiteral(assumption));
+    assumpts.push_back(d_cnfStream->getLiteral(assumption));
+  }
+  return prop::SAT_VALUE_TRUE == d_satSolver->solve(assumpts);
+}
+
 /**
  * Returns the value a is currently assigned to in the SAT solver
  * or null if the value is completely unassigned.
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index fbf1a4ddb..3e6190d76 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -36,7 +36,7 @@ class TheoryBV;
 class EagerBitblaster : public TBitblaster<Node>
 {
  public:
-  EagerBitblaster(TheoryBV* theory_bv);
+  EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
   ~EagerBitblaster();
 
   void addAtom(TNode atom);
@@ -51,10 +51,12 @@ class EagerBitblaster : public TBitblaster<Node>
 
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
+  bool solve(const std::vector<Node>& assumptions);
   bool collectModelInfo(TheoryModel* m, bool fullModel);
   void setProofLog(BitVectorProof* bvp);
 
  private:
+  context::Context* d_context;
   std::unique_ptr<context::Context> d_nullContext;
 
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
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();
 }
 
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 2754bdd3b..6a89a0f7c 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -2,7 +2,7 @@
 /*! \file bv_eager_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Andrew Reynolds
+ **   Liana Hadarean, Tim King, Mathias Preiner
  ** 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.
@@ -16,7 +16,8 @@
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#define __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 
 #include <unordered_set>
 #include <vector>
@@ -37,7 +38,7 @@ class AigBitblaster;
  */
 class EagerBitblastSolver {
  public:
-  EagerBitblastSolver(theory::bv::TheoryBV* bv);
+  EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -51,11 +52,13 @@ class EagerBitblastSolver {
   void setProofLog(BitVectorProof* bvp);
 
  private:
-  typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet;
-  AssertionSet d_assertionSet;
+  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
+  context::CDHashSet<Node, NodeHashFunction> d_assumptionSet;
+  context::Context* d_context;
+
   /** Bitblasters */
-  EagerBitblaster* d_bitblaster;
-  AigBitblaster* d_aigBitblaster;
+  std::unique_ptr<EagerBitblaster> d_bitblaster;
+  std::unique_ptr<AigBitblaster> d_aigBitblaster;
   bool d_useAig;
 
   TheoryBV* d_bv;
@@ -65,3 +68,5 @@ class EagerBitblastSolver {
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
+
+#endif  // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7dc6d3710..c4d419d83 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -74,7 +74,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver = new EagerBitblastSolver(this);
+    d_eagerSolver = new EagerBitblastSolver(c, this);
     return;
   }
 
@@ -243,18 +243,20 @@ void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == BITBLAST_MODE_EAGER)
+  {
     // the aig bit-blaster option is set heuristically
-    // if bv abstraction is not used
-    if (!d_eagerSolver->isInitialized()) {
+    // if bv abstraction is used
+    if (!d_eagerSolver->isInitialized())
+    {
       d_eagerSolver->initialize();
     }
 
-    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
+    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
+    {
       Node formula = node[0];
       d_eagerSolver->assertFormula(formula);
     }
-    // nothing to do for the other terms
     return;
   }
 
@@ -342,6 +344,7 @@ void TheoryBV::check(Effort e)
       TNode fact = get().assertion;
       Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
       assertions.push_back(fact);
+      d_eagerSolver->assertFormula(fact[0]);
     }
     Assert (d_eagerSolver->hasAssertions(assertions));
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c43e083f3..c15e3d045 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -239,6 +239,7 @@ REG0_TESTS = \
 	regress0/bv/core/slice-18.smt \
 	regress0/bv/core/slice-19.smt \
 	regress0/bv/core/slice-20.smt \
+	regress0/bv/eager-inc-cryptominisat.smt2 \
 	regress0/bv/divtest_2_5.smt2 \
 	regress0/bv/divtest_2_6.smt2 \
 	regress0/bv/fuzz01.smt \
diff --git a/test/regress/regress0/bv/eager-inc-cryptominisat.smt2 b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2
new file mode 100644
index 000000000..1c96ca25d
--- /dev/null
+++ b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2
@@ -0,0 +1,27 @@
+; REQUIRES: cryptominisat
+; COMMAND-LINE: --incremental --bv-sat-solver=cryptominisat --bitblast=eager
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+
+(assert (bvult a (bvadd b c)))
+(check-sat)
+; EXPECT: sat
+
+(push 1)
+(assert (bvult c b))
+(check-sat)
+; EXPECT: sat
+
+
+(push 1)
+(assert (bvugt c b))
+(check-sat)
+; EXPECT: unsat
+(pop 2)
+
+(check-sat)
+; EXPECT: sat
+(exit)
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index f95785f53..c830e7813 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -67,8 +67,11 @@ public:
  
   void testBitblasterCore() {
     d_smt->setOption("bitblast", SExpr("eager"));
-    EagerBitblaster* bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(
-        d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]));
+    d_smt->setOption("incremental", SExpr("false"));
+    EagerBitblaster* bb = new EagerBitblaster(
+        dynamic_cast<TheoryBV*>(
+            d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
+        d_smt->d_context);
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
     Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);