Add BV solver bitblast. (#5851)

This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.

7 files changed, 338 insertions, 17 deletions

diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index a4e1757e2..8bab969c5 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -611,11 +611,11 @@ void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
   Node a_size = utils::mkConst(size, size);
-  Node b_ult_a_size_node = Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
-  // ensure that the inequality is bit-blasted
-  bb->bbAtom(b_ult_a_size_node);
-  T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+  std::vector<T> a_size_bits;
+  DefaultConstBB(a_size, a_size_bits, bb);
+  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
+
   std::vector<T> prev_res;
   res = a;
   // we only need to look at the bits bellow log2_a_size
@@ -669,11 +669,11 @@ void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
   Node a_size = utils::mkConst(size, size);
-  Node b_ult_a_size_node = Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
-  // ensure that the inequality is bit-blasted
-  bb->bbAtom(b_ult_a_size_node);
-  T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+  std::vector<T> a_size_bits;
+  DefaultConstBB(a_size, a_size_bits, bb);
+  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
+
   res = a;
   std::vector<T> prev_res;
 
@@ -727,11 +727,10 @@ void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
   unsigned size = utils::getSize(node);
   unsigned log2_size = std::ceil(log2((double)size));
   Node a_size = utils::mkConst(size, size);
-  Node b_ult_a_size_node = Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
-  // ensure that the inequality is bit-blasted
-  bb->bbAtom(b_ult_a_size_node);
-  T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+  std::vector<T> a_size_bits;
+  DefaultConstBB(a_size, a_size_bits, bb);
+  T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
 
   res = a;
   T sign_bit = a.back();
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 36e115e5e..8eb209b53 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -51,9 +51,13 @@ void BBSimple::storeBBTerm(TNode node, const Bits& bits)
   d_termCache.emplace(node, bits);
 }
 
-bool BBSimple::hasBBAtom(TNode atom) const
+bool BBSimple::hasBBAtom(TNode lit) const
 {
-  return d_bbAtoms.find(atom) != d_bbAtoms.end();
+  if (lit.getKind() == kind::NOT)
+  {
+    lit = lit[0];
+  }
+  return d_bbAtoms.find(lit) != d_bbAtoms.end();
 }
 
 void BBSimple::makeVariable(TNode var, Bits& bits)
@@ -143,6 +147,11 @@ bool BBSimple::collectModelValues(TheoryModel* m,
   return true;
 }
 
+bool BBSimple::isVariable(TNode node)
+{
+  return d_variables.find(node) != d_variables.end();
+}
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 8a625b5e1..72a2fb0d8 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -58,6 +58,9 @@ class BBSimple : public TBitblaster<Node>
 
   prop::SatSolver* getSatSolver() override { Unreachable(); }
 
+  /** Checks whether node is a variable introduced via `makeVariable`.*/
+  bool isVariable(TNode node);
+
  private:
   /** Query SAT solver for assignment of node 'a'. */
   Node getModelFromSatSolver(TNode a, bool fullModel) override;
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
new file mode 100644
index 000000000..68192e1d4
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file bv_solver_bitblast.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bit-blasting solver
+ **
+ ** Bit-blasting solver that supports multiple SAT backends.
+ **/
+
+#include "theory/bv/bv_solver_bitblast.h"
+
+#include "options/bv_options.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+BVSolverBitblast::BVSolverBitblast(TheoryState* s,
+                                   TheoryInferenceManager& inferMgr,
+                                   ProofNodeManager* pnm)
+    : BVSolver(*s, inferMgr),
+      d_bitblaster(new BBSimple(s)),
+      d_nullRegistrar(new prop::NullRegistrar()),
+      d_nullContext(new context::Context()),
+      d_facts(s->getSatContext()),
+      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+                : nullptr)
+{
+  if (pnm != nullptr)
+  {
+    d_bvProofChecker.registerTo(pnm->getChecker());
+  }
+
+  switch (options::bvSatSolver())
+  {
+    case options::SatSolverMode::CRYPTOMINISAT:
+      d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
+          smtStatisticsRegistry(), "BVSolverBitblast"));
+      break;
+    default:
+      d_satSolver.reset(prop::SatSolverFactory::createCadical(
+          smtStatisticsRegistry(), "BVSolverBitblast"));
+  }
+  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+                                        d_nullRegistrar.get(),
+                                        d_nullContext.get(),
+                                        nullptr,
+                                        smt::currentResourceManager()));
+}
+
+void BVSolverBitblast::postCheck(Theory::Effort level)
+{
+  if (level != Theory::Effort::EFFORT_FULL)
+  {
+    return;
+  }
+
+  std::vector<prop::SatLiteral> assumptions;
+  std::unordered_map<prop::SatLiteral, TNode, prop::SatLiteralHashFunction>
+      node_map;
+  for (const TNode fact : d_facts)
+  {
+    /* Bitblast fact */
+    d_bitblaster->bbAtom(fact);
+    Node bb_fact = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+    d_cnfStream->ensureLiteral(bb_fact);
+
+    prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
+    assumptions.push_back(lit);
+    node_map.emplace(lit, fact);
+  }
+
+  prop::SatValue val = d_satSolver->solve(assumptions);
+
+  if (val == prop::SatValue::SAT_VALUE_FALSE)
+  {
+    std::vector<prop::SatLiteral> unsat_assumptions;
+    d_satSolver->getUnsatAssumptions(unsat_assumptions);
+    Assert(unsat_assumptions.size() > 0);
+
+    std::vector<Node> conflict;
+    for (const prop::SatLiteral& lit : unsat_assumptions)
+    {
+      conflict.push_back(node_map[lit]);
+    }
+
+    NodeManager* nm = NodeManager::currentNM();
+    d_inferManager.conflict(nm->mkAnd(conflict));
+  }
+}
+
+bool BVSolverBitblast::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  d_facts.push_back(fact);
+  return false;  // Return false to enable equality engine reasoning in Theory.
+}
+
+bool BVSolverBitblast::collectModelValues(TheoryModel* m,
+                                          const std::set<Node>& termSet)
+{
+  for (const auto& term : termSet)
+  {
+    if (!d_bitblaster->isVariable(term))
+    {
+      continue;
+    }
+
+    Node value = getValueFromSatSolver(term);
+    Assert(value.isConst());
+    if (!m->assertEquality(term, value, true))
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+Node BVSolverBitblast::getValueFromSatSolver(TNode node)
+{
+  /* If node was not bit-blasted return zero-initialized bit-vector. */
+  if (!d_bitblaster->hasBBTerm(node))
+  {
+    return utils::mkConst(utils::getSize(node), 0u);
+  }
+
+  std::vector<Node> bits;
+  d_bitblaster->getBBTerm(node, bits);
+  Integer value(0), one(1), zero(0), bit;
+  for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
+  {
+    if (d_cnfStream->hasLiteral(bits[j]))
+    {
+      prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
+      prop::SatValue val = d_satSolver->modelValue(lit);
+      bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
+    }
+    else
+    {
+      bit = zero;
+    }
+    value = value * 2 + bit;
+  }
+  return utils::mkConst(bits.size(), value);
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
new file mode 100644
index 000000000..df0f2e085
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file bv_solver_bitblast.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bit-blasting solver
+ **
+ ** Bit-blasting solver that supports multiple SAT back ends.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+#define CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+
+#include <unordered_map>
+
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bv_solver.h"
+#include "theory/bv/proof_checker.h"
+#include "theory/eager_proof_generator.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+/**
+ * Bit-blasting solver with support for different SAT back ends.
+ */
+class BVSolverBitblast : public BVSolver
+{
+ public:
+  BVSolverBitblast(TheoryState* state,
+                   TheoryInferenceManager& inferMgr,
+                   ProofNodeManager* pnm);
+  ~BVSolverBitblast() = default;
+
+  bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
+
+  void preRegisterTerm(TNode n) override {}
+
+  void postCheck(Theory::Effort level) override;
+
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+
+  std::string identify() const override { return "BVSolverBitblast"; };
+
+  Theory::PPAssertStatus ppAssert(
+      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
+  {
+    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
+  }
+
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
+
+ private:
+  /** Get value of `node` from SAT solver. */
+  Node getValueFromSatSolver(TNode node);
+
+  /** Bit-blaster used to bit-blast atoms/terms. */
+  std::unique_ptr<BBSimple> d_bitblaster;
+
+  /** Used for initializing CnfStream> */
+  std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+  std::unique_ptr<context::Context> d_nullContext;
+
+  /** SAT solver back end (configured via options::bvSatSolver. */
+  std::unique_ptr<prop::SatSolver> d_satSolver;
+  /** CNF stream. */
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+  /** Facts sent to this solver. */
+  context::CDList<Node> d_facts;
+
+  /** Proof generator that manages proofs for lemmas generated by this class. */
+  std::unique_ptr<EagerProofGenerator> d_epg;
+
+  BVProofRuleChecker d_bvProofChecker;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 227df458a..b27bd04e1 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,6 +17,7 @@
 
 #include "options/bv_options.h"
 #include "options/smt_options.h"
+#include "theory/bv/bv_solver_bitblast.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -42,6 +43,10 @@ TheoryBV::TheoryBV(context::Context* c,
 {
   switch (options::bvSolver())
   {
+    case options::BVSolver::BITBLAST:
+      d_internal.reset(new BVSolverBitblast(&d_state, d_inferMgr, pnm));
+      break;
+
     case options::BVSolver::LAZY:
       d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
       break;
@@ -70,6 +75,44 @@ void TheoryBV::finishInit()
   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
   d_internal->finishInit();
+
+  eq::EqualityEngine* ee = getEqualityEngine();
+  if (ee)
+  {
+    // The kinds we are treating as function application in congruence
+    ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
+    //    ee->addFunctionKind(kind::BITVECTOR_AND);
+    //    ee->addFunctionKind(kind::BITVECTOR_OR);
+    //    ee->addFunctionKind(kind::BITVECTOR_XOR);
+    //    ee->addFunctionKind(kind::BITVECTOR_NOT);
+    //    ee->addFunctionKind(kind::BITVECTOR_NAND);
+    //    ee->addFunctionKind(kind::BITVECTOR_NOR);
+    //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
+    //    ee->addFunctionKind(kind::BITVECTOR_COMP);
+    ee->addFunctionKind(kind::BITVECTOR_MULT, true);
+    ee->addFunctionKind(kind::BITVECTOR_PLUS, true);
+    ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+    //    ee->addFunctionKind(kind::BITVECTOR_SUB);
+    //    ee->addFunctionKind(kind::BITVECTOR_NEG);
+    //    ee->addFunctionKind(kind::BITVECTOR_UDIV);
+    //    ee->addFunctionKind(kind::BITVECTOR_UREM);
+    //    ee->addFunctionKind(kind::BITVECTOR_SDIV);
+    //    ee->addFunctionKind(kind::BITVECTOR_SREM);
+    //    ee->addFunctionKind(kind::BITVECTOR_SMOD);
+    //    ee->addFunctionKind(kind::BITVECTOR_SHL);
+    //    ee->addFunctionKind(kind::BITVECTOR_LSHR);
+    //    ee->addFunctionKind(kind::BITVECTOR_ASHR);
+    //    ee->addFunctionKind(kind::BITVECTOR_ULT);
+    //    ee->addFunctionKind(kind::BITVECTOR_ULE);
+    //    ee->addFunctionKind(kind::BITVECTOR_UGT);
+    //    ee->addFunctionKind(kind::BITVECTOR_UGE);
+    //    ee->addFunctionKind(kind::BITVECTOR_SLT);
+    //    ee->addFunctionKind(kind::BITVECTOR_SLE);
+    //    ee->addFunctionKind(kind::BITVECTOR_SGT);
+    //    ee->addFunctionKind(kind::BITVECTOR_SGE);
+    ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
+    ee->addFunctionKind(kind::INT_TO_BITVECTOR);
+  }
 }
 
 Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
@@ -199,6 +242,11 @@ TrustNode TheoryBV::ppRewrite(TNode t)
 
 void TheoryBV::presolve() { d_internal->presolve(); }
 
+EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+{
+  return d_internal->getEqualityStatus(a, b);
+}
+
 TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 
 void TheoryBV::notifySharedTerm(TNode t)
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 093a35a1b..306b1ff93 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -96,6 +96,8 @@ class TheoryBV : public Theory
 
   void presolve() override;
 
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+
   /** Called by abstraction preprocessing pass. */
   bool applyAbstraction(const std::vector<Node>& assertions,
                         std::vector<Node>& new_assertions);