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.

1 files changed, 12 insertions, 7 deletions

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