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.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b486471162dc83f5348c0116414f86b822627e2a..a72eb2c30a69650d9c2eb8768c4a3a6c34f9f075 100644 (file)
--- 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 4f239343e089d33334f049889542c370c461e168..df5a20791ac1e27cd7ef3b58c473c1c32a2e9c81 100644 (file)
--- 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 c265b2f353c08c8918fa59e8dcbfd65ef773ea6d..c5345cb8661f723d83ec9dac59c5d51edf594543 100644 (file)
--- 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 055efa4131a10247a4bd721ad46e770d6be8df4d..add73eebe903b625a2d91223fab7d5e989ea739d 100644 (file)
--- 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 5296a3bca0a088de7bd14f6092f43cbe2313bef8..de4537807c0d6cbf8ccbca0f6fd657710bfb6858 100644 (file)
--- 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 7b12c3465afcadcfa8869bb71e69edfbf9db472d..01437cb64ab0e584176ec329ea614bf7847ada8d 100644 (file)
--- 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 fbf1a4ddb435d02097c555ea18f33aeb1c9e234b..3e6190d7612c247133a40405c3437625d11f0f54 100644 (file)
--- 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 27dccfde03f410769d8e9c2e50cdc33e58b2317e..7dd3fd3e79928723ea6c08116beb2bc91d12fbba 100644 (file)
--- 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 2754bdd3b9cf2e5902c40c6320a010fa260a7e75..6a89a0f7cc661c315323e52ef5b1314aede323be 100644 (file)
--- 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 7dc6d37101cee734561eae996c52c9fe8de785c2..c4d419d835cda47bf910567d82dfd4df0458a00f 100644 (file)
--- 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 c43e083f38884d3769cf007e026493a4bcf5bc4b..c15e3d045df7398f3c80bc0626967d32ee65bba2 100644 (file)
--- 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 (file)
index 0000000..1c96ca2
--- /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 f95785f53497fa03d7190c886c665fb5ef1c06d0..c830e7813526c2193d998333b1c5003f96162695 100644 (file)
--- 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);