Add initial bit-blaster for proof logging. (#6053)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2b04bb40d91cbddf53a0522e9b88fa2294f9747d..c438d9a4f4560886743be71cfa52674b9b93fe77 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -516,6 +516,8 @@ libcvc4_add_sources(
   theory/bv/bitblast/eager_bitblaster.h
   theory/bv/bitblast/lazy_bitblaster.cpp
   theory/bv/bitblast/lazy_bitblaster.h
+  theory/bv/bitblast/proof_bitblaster.cpp
+  theory/bv/bitblast/proof_bitblaster.h
   theory/bv/bitblast/simple_bitblaster.cpp
   theory/bv/bitblast/simple_bitblaster.h
   theory/bv/bv_eager_solver.cpp

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
new file mode 100644 (file)
index 0000000..257107f
--- /dev/null
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -0,0 +1,87 @@
+/*********************                                                        */
+/*! \file proof_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 A bit-blaster wrapper around BBSimple for proof logging.
+ **/
+#include "theory/bv/bitblast/proof_bitblaster.h"
+
+#include <unordered_set>
+
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {}
+
+void BBProof::bbAtom(TNode node)
+{
+  std::vector<TNode> visit;
+  visit.push_back(node);
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  while (!visit.empty())
+  {
+    TNode n = visit.back();
+    if (hasBBAtom(n) || hasBBTerm(n))
+    {
+      visit.pop_back();
+      continue;
+    }
+
+    if (visited.find(n) == visited.end())
+    {
+      visited.insert(n);
+      if (!Theory::isLeafOf(n, theory::THEORY_BV))
+      {
+        visit.insert(visit.end(), n.begin(), n.end());
+      }
+    }
+    else
+    {
+      if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
+      {
+        // unused for now, will be needed for proof logging
+        Bits bits;
+        d_bb->makeVariable(n, bits);
+      }
+      else if (n.getType().isBitVector())
+      {
+        Bits bits;
+        d_bb->bbTerm(n, bits);
+      }
+      else
+      {
+        d_bb->bbAtom(n);
+      }
+      visit.pop_back();
+    }
+  }
+}
+
+bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
+
+bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
+
+Node BBProof::getStoredBBAtom(TNode node)
+{
+  return d_bb->getStoredBBAtom(node);
+}
+
+bool BBProof::collectModelValues(TheoryModel* m,
+                                 const std::set<Node>& relevantTerms)
+{
+  return d_bb->collectModelValues(m, relevantTerms);
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4

diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
new file mode 100644 (file)
index 0000000..af9ca25
--- /dev/null
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/*! \file proof_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 A bit-blaster wrapper around BBSimple for proof logging.
+ **/
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+
+#include "theory/bv/bitblast/simple_bitblaster.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BBProof
+{
+  using Bits = std::vector<Node>;
+
+ public:
+  BBProof(TheoryState* state);
+  ~BBProof() = default;
+
+  /** Bit-blast atom 'node'. */
+  void bbAtom(TNode node);
+  /** Check if atom was already bit-blasted. */
+  bool hasBBAtom(TNode atom) const;
+  /** Check if term was already bit-blasted. */
+  bool hasBBTerm(TNode node) const;
+  /** Get bit-blasted node stored for atom. */
+  Node getStoredBBAtom(TNode node);
+  /** Collect model values for all relevant terms given in 'relevantTerms'. */
+  bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
+
+ private:
+  std::unique_ptr<BBSimple> d_bb;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif

diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 72a2fb0d8d4525314d8122682cd746125544fd50..8c8a5fe09ed04b5335fc809dc0c51d75414a3cb6 100644 (file)
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -17,7 +17,7 @@
 #ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
 #define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
 
-#include "theory/bv/bitblast/lazy_bitblaster.h"
+#include "theory/bv/bitblast/bitblaster.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 58be5d826c036240642910c521a3fa62dee02f1c..1c698d686feaec88c70941e9d19548f7fb3a1bf6 100644 (file)
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -70,7 +70,7 @@ BVSolverSimple::BVSolverSimple(TheoryState* s,
                                TheoryInferenceManager& inferMgr,
                                ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
-      d_bitblaster(new BBSimple(s)),
+      d_bitblaster(new BBProof(s)),
       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
                 : nullptr)
 {

diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 17066e536735c3c551bc654f15a8786627600335..efd53436b5f6ec9cee034d2d456f585dc5ee84c9 100644 (file)
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -21,7 +21,7 @@
 
 #include <unordered_map>
 
-#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
 #include "theory/eager_proof_generator.h"
@@ -73,7 +73,7 @@ class BVSolverSimple : public BVSolver
   void addBBLemma(TNode fact);
 
   /** Bit-blaster used to bit-blast atoms/terms. */
-  std::unique_ptr<BBSimple> d_bitblaster;
+  std::unique_ptr<BBProof> d_bitblaster;
 
   /** Proof generator that manages proofs for lemmas generated by this class. */
   std::unique_ptr<EagerProofGenerator> d_epg;