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.

5 files changed, 78 insertions, 39 deletions

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));