Add simple BV solver (#5065)

This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.

9 files changed, 446 insertions, 5 deletions

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 36444afbe..6e251fc2d 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -68,7 +68,7 @@ class BVSolver
    */
   virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
 
-  virtual bool needsCheckLastEffort() = 0;
+  virtual bool needsCheckLastEffort() { return false; }
 
   virtual void propagate(Theory::Effort e){};
 
@@ -103,7 +103,12 @@ class BVSolver
 
   /** Called by abstraction preprocessing pass. */
   virtual bool applyAbstraction(const std::vector<Node>& assertions,
-                                std::vector<Node>& new_assertions) = 0;
+                                std::vector<Node>& new_assertions)
+  {
+    new_assertions.insert(
+        new_assertions.end(), assertions.begin(), assertions.end());
+    return false;
+  };
 
  protected:
   TheoryState& d_state;
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
new file mode 100644
index 000000000..e03feedfc
--- /dev/null
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -0,0 +1,296 @@
+/*********************                                                        */
+/*! \file bv_solver_simple.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 Simple bit-blast solver
+ **
+ ** Simple bit-blast solver that sends bitblast lemmas directly to MiniSat.
+ **/
+
+#include "theory/bv/bv_solver_simple.h"
+
+#include "theory/bv/bitblast/lazy_bitblaster.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 {
+
+/**
+ * Implementation of a simple Node-based bit-blaster.
+ *
+ * Implements the bare minimum to bit-blast bit-vector atoms/terms.
+ */
+class BBSimple : public TBitblaster<Node>
+{
+  using Bits = std::vector<Node>;
+
+ public:
+  BBSimple(TheoryState& state);
+  ~BBSimple() = default;
+
+  /** Bit-blast term 'node' and return bit-blasted 'bits'. */
+  void bbTerm(TNode node, Bits& bits) override;
+  /** Bit-blast atom 'node'. */
+  void bbAtom(TNode node) override;
+  /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */
+  Node getBBAtom(TNode atom) const override;
+  /** Store Boolean node representing the bit-blasted atom. */
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  /** Store bits of bit-blasted term. */
+  void storeBBTerm(TNode node, const Bits& bits) override;
+  /** Check if atom was already bit-blasted. */
+  bool hasBBAtom(TNode atom) const override;
+  /** Get bit-blasted node stored for atom. */
+  Node getStoredBBAtom(TNode node);
+  /** Create 'bits' for variable 'var'. */
+  void makeVariable(TNode var, Bits& bits) override;
+
+  /** Collect model values for all relevant terms given in 'relevantTerms'. */
+  bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
+
+  prop::SatSolver* getSatSolver() override { Unreachable(); }
+
+ private:
+  /** Query SAT solver for assignment of node 'a'. */
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+  /** Caches variables for which we already created bits. */
+  TNodeSet d_variables;
+  /** Stores bit-blasted atoms. */
+  std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms;
+  /** Theory state. */
+  TheoryState& d_state;
+};
+
+BBSimple::BBSimple(TheoryState& s) : TBitblaster<Node>(), d_state(s) {}
+
+void BBSimple::bbAtom(TNode node)
+{
+  node = node.getKind() == kind::NOT ? node[0] : node;
+
+  if (hasBBAtom(node))
+  {
+    return;
+  }
+
+  Node normalized = Rewriter::rewrite(node);
+  Node atom_bb =
+      normalized.getKind() != kind::CONST_BOOLEAN
+              && normalized.getKind() != kind::BITVECTOR_BITOF
+          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
+          : normalized;
+
+  storeBBAtom(node, atom_bb);
+}
+
+void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
+{
+  d_bbAtoms.emplace(atom, atom_bb);
+}
+
+void BBSimple::storeBBTerm(TNode node, const Bits& bits)
+{
+  d_termCache.emplace(node, bits);
+}
+
+bool BBSimple::hasBBAtom(TNode atom) const
+{
+  return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+void BBSimple::makeVariable(TNode var, Bits& bits)
+{
+  Assert(bits.size() == 0);
+  for (unsigned i = 0; i < utils::getSize(var); ++i)
+  {
+    bits.push_back(utils::mkBitOf(var, i));
+  }
+  d_variables.insert(var);
+}
+
+Node BBSimple::getBBAtom(TNode node) const { return node; }
+
+void BBSimple::bbTerm(TNode node, Bits& bits)
+{
+  Assert(node.getType().isBitVector());
+  if (hasBBTerm(node))
+  {
+    getBBTerm(node, bits);
+    return;
+  }
+  d_termBBStrategies[node.getKind()](node, bits, this);
+  Assert(bits.size() == utils::getSize(node));
+  storeBBTerm(node, bits);
+}
+
+Node BBSimple::getStoredBBAtom(TNode node)
+{
+  bool negated = false;
+  if (node.getKind() == kind::NOT)
+  {
+    node = node[0];
+    negated = true;
+  }
+
+  Assert(hasBBAtom(node));
+  Node atom_bb = d_bbAtoms.at(node);
+  return negated ? atom_bb.negate() : atom_bb;
+}
+
+Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
+{
+  if (!hasBBTerm(a))
+  {
+    return utils::mkConst(utils::getSize(a), 0u);
+  }
+
+  bool assignment;
+  Bits bits;
+  getBBTerm(a, bits);
+  Integer value(0);
+  Integer one(1), zero(0);
+  for (int i = bits.size() - 1; i >= 0; --i)
+  {
+    Integer bit;
+    if (d_state.hasSatValue(bits[i], assignment))
+    {
+      bit = assignment ? one : zero;
+    }
+    else
+    {
+      bit = zero;
+    }
+    value = value * 2 + bit;
+  }
+  return utils::mkConst(bits.size(), value);
+}
+
+bool BBSimple::collectModelValues(TheoryModel* m,
+                                  const std::set<Node>& relevantTerms)
+{
+  for (const auto& var : relevantTerms)
+  {
+    if (d_variables.find(var) == d_variables.end()) continue;
+
+    Node const_value = getModelFromSatSolver(var, true);
+    Assert(const_value.isNull() || const_value.isConst());
+    if (!const_value.isNull())
+    {
+      if (!m->assertEquality(var, const_value, true))
+      {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+/* -------------------------------------------------------------------------- */
+
+namespace {
+
+bool isBVAtom(TNode n)
+{
+  return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
+         || n.getKind() == kind::BITVECTOR_ULT
+         || n.getKind() == kind::BITVECTOR_ULE
+         || n.getKind() == kind::BITVECTOR_SLT
+         || n.getKind() == kind::BITVECTOR_SLE;
+}
+
+/* Traverse Boolean nodes and collect BV atoms. */
+void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
+{
+  std::vector<TNode> visit;
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+
+  visit.push_back(n);
+
+  do
+  {
+    TNode cur = visit.back();
+    visit.pop_back();
+
+    if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
+      continue;
+
+    visited.insert(cur);
+    if (isBVAtom(cur))
+    {
+      atoms.insert(cur);
+      continue;
+    }
+
+    visit.insert(visit.end(), cur.begin(), cur.end());
+  } while (!visit.empty());
+}
+
+}  // namespace
+
+BVSolverSimple::BVSolverSimple(TheoryState& s, TheoryInferenceManager& inferMgr)
+    : BVSolver(s, inferMgr), d_bitblaster(new BBSimple(s))
+{
+}
+
+void BVSolverSimple::addBBLemma(TNode fact)
+{
+  if (!d_bitblaster->hasBBAtom(fact))
+  {
+    d_bitblaster->bbAtom(fact);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node atom_bb = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+  Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
+  d_inferManager.lemma(lemma);
+}
+
+bool BVSolverSimple::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  if (fact.getKind() == kind::NOT)
+  {
+    fact = fact[0];
+  }
+
+  if (isBVAtom(fact))
+  {
+    addBBLemma(fact);
+  }
+  else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
+  {
+    TNode n = fact[0];
+
+    NodeManager* nm = NodeManager::currentNM();
+    Node lemma = nm->mkNode(kind::EQUAL, fact, n);
+    d_inferManager.lemma(lemma);
+
+    std::unordered_set<Node, NodeHashFunction> bv_atoms;
+    collectBVAtoms(n, bv_atoms);
+    for (const Node& nn : bv_atoms)
+    {
+      addBBLemma(nn);
+    }
+  }
+
+  return true;
+}
+
+bool BVSolverSimple::collectModelValues(TheoryModel* m,
+                                        const std::set<Node>& termSet)
+{
+  return d_bitblaster->collectModelValues(m, termSet);
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
new file mode 100644
index 000000000..b7d86cf67
--- /dev/null
+++ b/src/theory/bv/bv_solver_simple.h
@@ -0,0 +1,80 @@
+/*********************                                                        */
+/*! \file bv_solver_simple.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 Simple bit-blast solver
+ **
+ ** Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+
+#include <unordered_map>
+
+#include "theory/bv/bv_solver.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+class BBSimple;
+
+/**
+ * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
+ * internal MiniSat. It is also ablo to handle atoms of kind
+ * BITVECTOR_EAGER_ATOM.
+ *
+ * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
+ */
+class BVSolverSimple : public BVSolver
+{
+ public:
+  BVSolverSimple(TheoryState& state, TheoryInferenceManager& inferMgr);
+  ~BVSolverSimple() = default;
+
+  void preRegisterTerm(TNode n) override {}
+
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+
+  std::string identify() const override { return "BVSolverSimple"; };
+
+  Theory::PPAssertStatus ppAssert(TNode in,
+                                  SubstitutionMap& outSubstitutions) override
+  {
+    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
+  }
+
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
+
+ private:
+  /**
+   * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
+   * inference manager.
+   */
+  void addBBLemma(TNode fact);
+
+  /** Bit-blaster used to bit-blast atoms/terms. */
+  std::unique_ptr<BBSimple> d_bitblaster;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 3e462d5cc..857d4d6fb 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 "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
@@ -38,7 +39,16 @@ TheoryBV::TheoryBV(context::Context* c,
       d_state(c, u, valuation),
       d_inferMgr(*this, d_state, pnm)
 {
-  d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
+  switch (options::bvSolver())
+  {
+    case options::BVSolver::LAZY:
+      d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
+      break;
+
+    default:
+      AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
+      d_internal.reset(new BVSolverSimple(d_state, d_inferMgr));
+  }
   d_theoryState = &d_state;
   d_inferManager = &d_inferMgr;
 }
@@ -159,6 +169,19 @@ void TheoryBV::preRegisterTerm(TNode node)
 
 bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
 
+void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
+
+bool TheoryBV::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
+}
+
+void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+  d_internal->notifyFact(atom, pol, fact, isInternal);
+}
+
 bool TheoryBV::needsCheckLastEffort()
 {
   return d_internal->needsCheckLastEffort();
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index a93fd438b..a01c74382 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -65,6 +65,16 @@ class TheoryBV : public Theory
 
   bool preCheck(Effort e) override;
 
+  void postCheck(Effort e) override;
+
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+
   bool needsCheckLastEffort() override;
 
   void propagate(Effort e) override;
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index bfea2f1e6..8f97bf3a6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -203,6 +203,7 @@ enum RewriteRuleId
   ConcatToMult,
   IsPowerOfTwo,
   MultSltMult,
+  BitOfConst,
 };
 
 inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
@@ -367,6 +368,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
   case MultSltMult: out << "MultSltMult"; return out;
   case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out;
+  case BitOfConst: out << "BitOfConst"; return out;
   default:
     Unreachable();
   }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d0c68c9e7..dd0d47078 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -28,6 +28,23 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/* -------------------------------------------------------------------------- */
+
+/**
+ * BitOfConst
+ */
+template <>
+inline bool RewriteRule<BitOfConst>::applies(TNode node)
+{
+  return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst();
+}
+
+template <>
+inline Node RewriteRule<BitOfConst>::apply(TNode node)
+{
+  size_t pos = node.getOperator().getConst<BitVectorBitOf>().d_bitIndex;
+  return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse();
+}
 
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 6cea74a95..4f84facca 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -53,6 +53,12 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return res; 
 }
 
+RewriteResponse TheoryBVRewriter::RewriteBitOf(TNode node, bool prerewrite)
+{
+  Node resultNode = LinearRewriteStrategy<RewriteRule<BitOfConst>>::apply(node);
+  return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
 RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
   // reduce common subexpressions on both sides
   Node resultNode = LinearRewriteStrategy
@@ -683,6 +689,7 @@ void TheoryBVRewriter::initializeRewrites() {
   }
 
   d_rewriteTable [ kind::EQUAL ] = RewriteEqual;
+  d_rewriteTable[kind::BITVECTOR_BITOF] = RewriteBitOf;
   d_rewriteTable [ kind::BITVECTOR_ULT ] = RewriteUlt;
   d_rewriteTable [ kind::BITVECTOR_SLT ] = RewriteSlt;
   d_rewriteTable [ kind::BITVECTOR_ULE ] = RewriteUle;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index dee0f81d6..7e2110b14 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -50,8 +50,9 @@ class TheoryBVRewriter : public TheoryRewriter
 
  private:
   static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
-  static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); 
-  
+  static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
+
+  static RewriteResponse RewriteBitOf(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false);