ClausalBitvectorProof (#2786)

* [DRAT] ClausalBitvectorProof

Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)

It fits into the `BitvectorProof` class hierarchy like this:

```
              BitvectorProof
              /            \
             /              \
ClausalBitvectorProof  ResolutionBitvectorProof
```

This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
   * CnfStream
   * SatSolver (specifically the BvSatSolver)
   * CnfProof
   * TheoryProof
   * TheoryBV
   * Both bitblasters

And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.

This means that references to and interactions with (R)BVP were
pervasive.

Nevertheless, an SMT developer must persist.

The change summary:
  * Create a subclass of BVP, called ClausalBitvectorProof, which has
    most methods stubbed out.
  * Make a some modifications to BVP and ResolutionBitvectorProof as the
    natural division of labor between the different classes becomes
    clear.
  * Go through all the components in the first list and try to figure
    out which kind of BVP they should **actually** be interacting with,
    and how. Make tweaks accordingly.
  * Add a hook from CryptoMinisat which pipes the produced DRAT proof
    into the new ClausalBitvectorProof.
  * Add a debug statement to ClausalBitvectorProof which parses and
    prints that DRAT proof, for testing purposes.

Test:
  * `make check` to verify that we didn't break any old stuff, including
    lazy BB, and eager BB when using bvminisat.
  * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
  -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
     1. It crashed with "Unimplemented"
     2. Right before that it prints out the (textual) DRAT proof.

* Remove 2 unneeded methods

* Missed a rename

* Typos

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Address Andres comments

* Reorder members of TBitblaster

12 files changed, 57 insertions, 40 deletions

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 73b4d19c7..b1fc084ed 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -24,6 +24,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "proof/bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
@@ -31,6 +32,7 @@
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -59,6 +61,10 @@ class TBitblaster
   // caches and mappings
   TermDefMap d_termCache;
   ModelCache d_modelCache;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<context::Context> d_nullContext;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+  proof::BitVectorProof* d_bvp;
 
   void initAtomBBStrategies();
   void initTermBBStrategies();
@@ -69,6 +75,8 @@ class TBitblaster
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
   AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
   virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+  virtual prop::SatSolver* getSatSolver() = 0;
+
 
  public:
   TBitblaster();
@@ -83,6 +91,8 @@ class TBitblaster
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
   virtual void storeBBTerm(TNode term, const Bits& bits);
+  void setProofLog(proof::BitVectorProof* bvp);
+
   /**
    * Return a constant representing the value of a in the  model.
    * If fullModel is true set unconstrained bits to 0. If not return
@@ -171,7 +181,12 @@ void TBitblaster<T>::initTermBBStrategies()
 }
 
 template <class T>
-TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache()
+TBitblaster<T>::TBitblaster()
+    : d_termCache(),
+      d_modelCache(),
+      d_nullContext(new context::Context()),
+      d_cnfStream(),
+      d_bvp(nullptr)
 {
   initAtomBBStrategies();
   initTermBBStrategies();
@@ -202,6 +217,20 @@ void TBitblaster<T>::invalidateModelCache()
 }
 
 template <class T>
+void TBitblaster<T>::setProofLog(proof::BitVectorProof* bvp)
+{
+  if (THEORY_PROOF_ON())
+  {
+    d_bvp = bvp;
+    prop::SatSolver* satSolver = getSatSolver();
+    bvp->attachToSatSolver(*satSolver);
+    prop::SatVariable t = satSolver->trueVar();
+    prop::SatVariable f = satSolver->falseVar();
+    bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f);
+  }
+}
+
+template <class T>
 Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 {
   if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 019918c2f..1e557bb64 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -32,11 +32,8 @@ namespace 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)),
-      d_cnfStream(),
-      d_bvp(nullptr),
       d_bv(theory_bv),
       d_bbAtoms(),
       d_variables(),
@@ -268,13 +265,6 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void EagerBitblaster::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
-{
-  THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp);
-               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());)
-}
-
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 3299ffc54..1c183b509 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -55,19 +55,13 @@ class EagerBitblaster : public TBitblaster<Node>
   bool solve();
   bool solve(const std::vector<Node>& assumptions);
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
 
  private:
   context::Context* d_context;
-  std::unique_ptr<context::Context> d_nullContext;
 
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
-  std::unique_ptr<prop::CnfStream> d_cnfStream;
-
-  BitVectorProof* d_bvp;
 
   TheoryBV* d_bv;
   TNodeSet d_bbAtoms;
@@ -77,6 +71,7 @@ class EagerBitblaster : public TBitblaster<Node>
   std::unique_ptr<MinisatEmptyNotify> d_notify;
 
   Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
   bool isSharedTerm(TNode node);
 };
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 529f0373b..2a47c2315 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -64,10 +64,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
                                  bool emptyNotify)
     : TBitblaster<Node>(),
       d_bv(bv),
-      d_bvp(nullptr),
       d_ctx(c),
       d_nullRegistrar(new prop::NullRegistrar()),
-      d_nullContext(new context::Context()),
       d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
       d_explanations(new (true) ExplanationMap(c)),
       d_variables(),
@@ -566,11 +564,12 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp)
 {
-  d_bvp = bvp;
-  d_satSolver->setProofLog( bvp );
-  bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+  THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver);
+               prop::SatVariable t = d_satSolver->trueVar();
+               prop::SatVariable f = d_satSolver->falseVar();
+               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f));
 }
 
 void TLazyBitblaster::clearSolver() {
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 1195d3590..9af74d8db 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -77,7 +77,7 @@ class TLazyBitblaster : public TBitblaster<Node>
    * constants to equivalence classes that don't already have them
    */
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
@@ -126,15 +126,11 @@ class TLazyBitblaster : public TBitblaster<Node>
   };
 
   TheoryBV* d_bv;
-  proof::ResolutionBitVectorProof* d_bvp;
   context::Context* d_ctx;
 
   std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
-  std::unique_ptr<context::Context> d_nullContext;
-  // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
   std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
-  std::unique_ptr<prop::CnfStream> d_cnfStream;
 
   AssertionList*
       d_assertedAtoms;            /**< context dependent list storing the atoms
@@ -155,6 +151,7 @@ class TLazyBitblaster : public TBitblaster<Node>
   void addAtom(TNode atom);
   bool hasValue(TNode a);
   Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
 
   class Statistics
   {
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 119195c4a..336529dfd 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -56,7 +56,7 @@ void EagerBitblastSolver::initialize() {
   } else {
     d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
     THEORY_PROOF(if (d_bvp) {
-      d_bitblaster->setResolutionProofLog(d_bvp);
+      d_bitblaster->setProofLog(d_bvp);
       d_bvp->setBitblaster(d_bitblaster.get());
     });
   }
@@ -127,8 +127,7 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
   return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
-void EagerBitblastSolver::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
+void EagerBitblastSolver::setProofLog(proof::BitVectorProof* bvp)
 {
   d_bvp = bvp;
 }
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 7f688b3ae..0b518ca4a 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -48,7 +48,7 @@ class EagerBitblastSolver {
   bool isInitialized();
   void initialize();
   bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
  private:
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
@@ -61,7 +61,7 @@ class EagerBitblastSolver {
   bool d_useAig;
 
   TheoryBV* d_bv;
-  proof::ResolutionBitVectorProof* d_bvp;
+  proof::BitVectorProof* d_bvp;
 };  // class EagerBitblastSolver
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 31c542e0b..e2b649841 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -26,7 +26,7 @@
 namespace CVC4 {
 
 namespace proof {
-class ResolutionBitVectorProof;
+class BitVectorProof;
 }
 
 namespace theory {
@@ -93,7 +93,7 @@ class SubtheorySolver {
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+  virtual void setProofLog(proof::BitVectorProof* bvp) {}
   AssertionQueue::const_iterator assertionsBegin() {
     return d_assertionQueue.begin();
   }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ff9dd52c2..ceb02af40 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -276,7 +276,7 @@ void BitblastSolver::setConflict(TNode conflict) {
   d_bv->setConflict(final_conflict);
 }
 
-void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BitblastSolver::setProofLog(proof::BitVectorProof* bvp)
 {
   d_bitblaster->setProofLog( bvp );
   bvp->setBitblaster(d_bitblaster.get());
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index aa2c90c43..e028dbbdc 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -79,7 +79,7 @@ public:
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module);
   uint64_t computeAtomWeight(TNode atom);
-  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+  void setProofLog(proof::BitVectorProof* bvp) override;
 };
 
 } /* namespace CVC4::theory::bv */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 949a3d738..04a6cf52c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -986,10 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
-void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp)
+void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
 {
   if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
-    d_eagerSolver->setResolutionProofLog(bvp);
+    d_eagerSolver->setProofLog(bvp);
   }else{
     for( unsigned i=0; i< d_subtheories.size(); i++ ){
       d_subtheories[i]->setProofLog( bvp );
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index afa9f4b4f..3d151cfb1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -31,6 +31,14 @@
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
+// Forward declarations, needed because the BV theory and the BV Proof classes
+// are cyclically dependent
+namespace CVC4 {
+namespace proof {
+class BitVectorProof;
+}
+}  // namespace CVC4
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -104,7 +112,7 @@ public:
 
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
  private: