Bit vector proof superclass (#2599)

* Split BitvectorProof into a sub/superclass

The superclass contains general printing knowledge.

The subclass contains CNF or Resolution-specific knowledge.

* Renames & code moves

* Nits cleaned in prep for PR

* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof

Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.

* Unique pointers, comments, and code movement.

Adjusted the distribution of code between BVP and RBVP.
  Notably, put the CNF proof in BVP because it isn't
  resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
  BVP's pointer to a CNF proof
  RBVP's pointer to a resolution proof

BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`

* clang-format

* Undo manual copyright modification

* s/superclass/base class/

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

* make LFSCBitVectorProof::printOwnedSort public

* Andres's Comments

Mostly cleaning up (or trying to clean up) includes.

* Cleaned up one header cycle

However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.

* Added single _s to header gaurds

* Fix Class name in debug output

Credits to Andres

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

* Reordered methods in BitVectorProof per original  ordering

13 files changed, 60 insertions, 37 deletions

diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 6d21b69e6..62e70d73d 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -20,6 +20,7 @@
 #define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
+#include "prop/sat_solver.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 9e2dac2f3..73b4d19c7 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -24,7 +24,8 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "prop/sat_solver.h"
+#include "prop/bv_sat_solver_notify.h"
+#include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
 #include "theory/theory_registrar.h"
 #include "theory/valuation.h"
@@ -59,8 +60,6 @@ class TBitblaster
   TermDefMap d_termCache;
   ModelCache d_modelCache;
 
-  BitVectorProof* d_bvp;
-
   void initAtomBBStrategies();
   void initTermBBStrategies();
 
@@ -94,7 +93,7 @@ class TBitblaster
   void invalidateModelCache();
 };
 
-class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify
+class MinisatEmptyNotify : public prop::BVSatSolverNotify
 {
  public:
   MinisatEmptyNotify() {}
@@ -172,7 +171,7 @@ void TBitblaster<T>::initTermBBStrategies()
 }
 
 template <class T>
-TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL)
+TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache()
 {
   initAtomBBStrategies();
   initTermBBStrategies();
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 01437cb64..33d5a1c80 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -19,7 +19,6 @@
 #include "theory/bv/bitblast/eager_bitblaster.h"
 
 #include "options/bv_options.h"
-#include "proof/bitvector_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
@@ -37,6 +36,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
       d_cnfStream(),
+      d_bvp(nullptr),
       d_bv(theory_bv),
       d_bbAtoms(),
       d_variables(),
@@ -268,10 +268,11 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
-  d_bvp = bvp;
-  d_satSolver->setProofLog(bvp);
-  bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+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) {
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 3e6190d76..3299ffc54 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -23,6 +23,8 @@
 
 #include "theory/bv/bitblast/bitblaster.h"
 
+#include "proof/bitvector_proof.h"
+#include "proof/resolution_bitvector_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 
@@ -53,7 +55,7 @@ class EagerBitblaster : public TBitblaster<Node>
   bool solve();
   bool solve(const std::vector<Node>& assumptions);
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog(BitVectorProof* bvp);
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
 
  private:
   context::Context* d_context;
@@ -65,6 +67,8 @@ class EagerBitblaster : public TBitblaster<Node>
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
   std::unique_ptr<prop::CnfStream> d_cnfStream;
 
+  BitVectorProof* d_bvp;
+
   TheoryBV* d_bv;
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index a50916413..529f0373b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -19,17 +19,16 @@
 #include "theory/bv/bitblast/lazy_bitblaster.h"
 
 #include "options/bv_options.h"
+#include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
-#include "proof/bitvector_proof.h"
-#include "proof/proof_manager.h"
-#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -65,6 +64,7 @@ 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()),
@@ -90,8 +90,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
 
   d_satSolverNotify.reset(
       d_emptyNotify
-          ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
-          : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
+          : (prop::BVSatSolverNotify*)new MinisatNotify(
                 d_cnfStream.get(), bv, this));
 
   d_satSolver->setNotify(d_satSolverNotify.get());
@@ -566,7 +566,8 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
+void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp)
+{
   d_bvp = bvp;
   d_satSolver->setProofLog( bvp );
   bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
@@ -590,8 +591,8 @@ void TLazyBitblaster::clearSolver() {
       d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
   d_satSolverNotify.reset(
       d_emptyNotify
-          ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
-          : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+          ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
+          : (prop::BVSatSolverNotify*)new MinisatNotify(
                 d_cnfStream.get(), d_bv, this));
   d_satSolver->setNotify(d_satSolverNotify.get());
 }
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 5e16b743a..1195d3590 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -19,13 +19,14 @@
 #ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
 #define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
 
+#include "proof/resolution_bitvector_proof.h"
 #include "theory/bv/bitblast/bitblaster.h"
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "prop/cnf_stream.h"
 #include "prop/registrar.h"
-#include "prop/sat_solver.h"
+#include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
 namespace CVC4 {
@@ -76,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(BitVectorProof* bvp);
+  void setProofLog(proof::ResolutionBitVectorProof* bvp);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
@@ -106,7 +107,7 @@ class TLazyBitblaster : public TBitblaster<Node>
                              prop::SatLiteralHashFunction>
       ExplanationMap;
   /** This class gets callbacks from minisat on propagations */
-  class MinisatNotify : public prop::BVSatSolverInterface::Notify
+  class MinisatNotify : public prop::BVSatSolverNotify
   {
     prop::CnfStream* d_cnf;
     TheoryBV* d_bv;
@@ -125,13 +126,14 @@ 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::BVSatSolverInterface::Notify> d_satSolverNotify;
+  std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
   std::unique_ptr<prop::CnfStream> d_cnfStream;
 
   AssertionList*
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 27a48875d..119195c4a 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -17,7 +17,6 @@
 #include "theory/bv/bv_eager_solver.h"
 
 #include "options/bv_options.h"
-#include "proof/bitvector_proof.h"
 #include "theory/bv/bitblast/aig_bitblaster.h"
 #include "theory/bv/bitblast/eager_bitblaster.h"
 
@@ -57,7 +56,7 @@ void EagerBitblastSolver::initialize() {
   } else {
     d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
     THEORY_PROOF(if (d_bvp) {
-      d_bitblaster->setProofLog(d_bvp);
+      d_bitblaster->setResolutionProofLog(d_bvp);
       d_bvp->setBitblaster(d_bitblaster.get());
     });
   }
@@ -128,7 +127,11 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
   return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
-void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; }
+void EagerBitblastSolver::setResolutionProofLog(
+    proof::ResolutionBitVectorProof* bvp)
+{
+  d_bvp = bvp;
+}
 
 }  // namespace bv
 }  // namespace theory
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index b17cd6ebc..7f688b3ae 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "proof/resolution_bitvector_proof.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
@@ -47,7 +48,7 @@ class EagerBitblastSolver {
   bool isInitialized();
   void initialize();
   bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
-  void setProofLog(BitVectorProof* bvp);
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
 
  private:
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
@@ -60,7 +61,7 @@ class EagerBitblastSolver {
   bool d_useAig;
 
   TheoryBV* d_bv;
-  BitVectorProof* d_bvp;
+  proof::ResolutionBitVectorProof* d_bvp;
 };  // class EagerBitblastSolver
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 3166401aa..31c542e0b 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -24,6 +24,11 @@
 #include "theory/theory.h"
 
 namespace CVC4 {
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
+
 namespace theory {
 
 class TheoryModel;
@@ -88,7 +93,7 @@ class SubtheorySolver {
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-  virtual void setProofLog(BitVectorProof* bvp) {}
+  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
   AssertionQueue::const_iterator assertionsBegin() {
     return d_assertionQueue.begin();
   }
@@ -103,7 +108,7 @@ class SubtheorySolver {
   /** The bit-vector theory */
   TheoryBV* d_bv;
   /** proof log */
-  BitVectorProof* d_bvp;
+  proof::ResolutionBitVectorProof* d_bvp;
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t> d_assertionIndex;
 }; /* class SubtheorySolver */
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ea2f8e4bf..ff9dd52c2 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -18,7 +18,6 @@
 #include "decision/decision_attributes.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
-#include "proof/bitvector_proof.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
@@ -277,7 +276,8 @@ void BitblastSolver::setConflict(TNode conflict) {
   d_bv->setConflict(final_conflict);
 }
 
-void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
+void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* 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 ac0d38815..aa2c90c43 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -23,6 +23,11 @@
 #include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
+
 namespace theory {
 namespace bv {
 
@@ -74,7 +79,7 @@ public:
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module);
   uint64_t computeAtomWeight(TNode atom);
-  void setProofLog(BitVectorProof* bvp) override;
+  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
 };
 
 } /* namespace CVC4::theory::bv */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d08405ef3..e60d60456 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -986,9 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
-void TheoryBV::setProofLog( BitVectorProof * bvp ) {
+void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp)
+{
   if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
-    d_eagerSolver->setProofLog( bvp );
+    d_eagerSolver->setResolutionProofLog(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 d5e3ad02e..afa9f4b4f 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -104,9 +104,9 @@ public:
 
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 
-  void setProofLog( BitVectorProof * bvp );
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
 
-private:
+ private:
 
   class Statistics {
   public: