Add support for BV proofs with the simple bitblasting solver. (#5603)

1 files changed, 34 insertions, 176 deletions

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 153d85df5..98fce24be 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -16,7 +16,6 @@
 
 #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"
@@ -25,176 +24,6 @@ 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 {
@@ -237,9 +66,18 @@ void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
 
 }  // namespace
 
-BVSolverSimple::BVSolverSimple(TheoryState& s, TheoryInferenceManager& inferMgr)
-    : BVSolver(s, inferMgr), d_bitblaster(new BBSimple(s))
+BVSolverSimple::BVSolverSimple(TheoryState* s,
+                               TheoryInferenceManager& inferMgr,
+                               ProofNodeManager* pnm)
+    : BVSolver(*s, inferMgr),
+      d_bitblaster(new BBSimple(s)),
+      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+                : nullptr)
 {
+  if (pnm != nullptr)
+  {
+    d_bvProofChecker.registerTo(pnm->getChecker());
+  }
 }
 
 void BVSolverSimple::addBBLemma(TNode fact)
@@ -249,9 +87,19 @@ void BVSolverSimple::addBBLemma(TNode fact)
     d_bitblaster->bbAtom(fact);
   }
   NodeManager* nm = NodeManager::currentNM();
-  Node atom_bb = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+
+  Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
   Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
-  d_inferManager.lemma(lemma);
+
+  if (d_epg == nullptr)
+  {
+    d_inferManager.lemma(lemma);
+  }
+  else
+  {
+    TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
+    d_inferManager.trustedLemma(tlem);
+  }
 }
 
 bool BVSolverSimple::preNotifyFact(
@@ -272,7 +120,17 @@ bool BVSolverSimple::preNotifyFact(
 
     NodeManager* nm = NodeManager::currentNM();
     Node lemma = nm->mkNode(kind::EQUAL, fact, n);
-    d_inferManager.lemma(lemma);
+
+    if (d_epg == nullptr)
+    {
+      d_inferManager.lemma(lemma);
+    }
+    else
+    {
+      TrustNode tlem =
+          d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
+      d_inferManager.trustedLemma(tlem);
+    }
 
     std::unordered_set<Node, NodeHashFunction> bv_atoms;
     collectBVAtoms(n, bv_atoms);