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

6 files changed, 48 insertions, 20 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 55710092b..57ef8ef30 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
-void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BVMinisatSatSolver::setResolutionProofLog(
+    proof::ResolutionBitVectorProof* bvp)
 {
   d_minisat->setProofLog( bvp );
 }
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 16489b172..efb90a3f0 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -119,7 +119,7 @@ public:
 
   void popAssumption() override;
 
-  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
 
  private:
   /* Disable the default constructor. */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index cdb850ce2..84c315547 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -79,19 +79,22 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
     }
   }
 
-  PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node););
+  if (PROOF_ON() && d_cnfProof)
+  {
+    d_cnfProof->pushCurrentDefinition(node);
+  }
 
   ClauseId clause_id = d_satSolver->addClause(c, d_removable);
   if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
 
-  PROOF
-    (
-     if (d_cnfProof) {
-       Assert (clause_id != ClauseIdError);
-       d_cnfProof->registerConvertedClause(clause_id);
-       d_cnfProof->popCurrentDefinition();
-     }
-    );
+  if (PROOF_ON() && d_cnfProof)
+  {
+    if (clause_id != ClauseIdError)
+    {
+      d_cnfProof->registerConvertedClause(clause_id);
+    }
+    d_cnfProof->popCurrentDefinition();
+  };
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index df5a20791..c04fb8b56 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -62,10 +62,11 @@ void toInternalClause(SatClause& clause,
 
 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
                                          const std::string& name)
-: d_solver(new CMSat::SATSolver())
-, d_numVariables(0)
-, d_okay(true)
-, d_statistics(registry, name)
+    : d_solver(new CMSat::SATSolver()),
+      d_bvp(nullptr),
+      d_numVariables(0),
+      d_okay(true),
+      d_statistics(registry, name)
 {
   d_true = newVar();
   d_false = newVar();
@@ -117,9 +118,17 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
-  bool res = d_solver->add_clause(internal_clause);
-  d_okay &= res;
-  return ClauseIdError;
+  bool nowOkay = d_solver->add_clause(internal_clause);
+  ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
+
+  THEORY_PROOF(
+      // If this clause results in a conflict, then `nowOkay` may be false, but
+      // we still need to register this clause as used. Thus, we look at
+      // `d_okay` instead
+      if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+
+  d_okay &= nowOkay;
+  return freshId;
 }
 
 bool CryptoMinisatSolver::ok() const {
@@ -193,6 +202,12 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const {
   return -1; 
 }
 
+void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
+{
+  d_bvp = bvp;
+  d_solver->set_drat(&bvp->getDratOstream(), false);
+}
+
 // Satistics for CryptoMinisatSolver
 
 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index c5345cb86..17cc1568c 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,6 +21,7 @@
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
+#include "proof/clausal_bitvector_proof.h"
 #include "prop/sat_solver.h"
 
 // Cryptominisat has name clashes with the other Minisat implementations since
@@ -39,6 +40,7 @@ class CryptoMinisatSolver : public SatSolver {
 
 private:
   std::unique_ptr<CMSat::SATSolver> d_solver;
+  proof::ClausalBitVectorProof* d_bvp;
   unsigned d_numVariables;
   bool d_okay;
   SatVariable d_true;
@@ -71,6 +73,7 @@ public:
   SatValue modelValue(SatLiteral l) override;
 
   unsigned getAssertionLevel() const override;
+  void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
 
   class Statistics {
   public:
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 49064c20f..70e46eceb 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,7 +26,6 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "proof/resolution_bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "prop/bv_sat_solver_notify.h"
@@ -34,6 +33,11 @@
 
 namespace CVC4 {
 
+namespace proof {
+class ClausalBitVectorProof;
+class ResolutionBitVectorProof;
+}  // namespace proof
+
 namespace prop {
 
 class TheoryProxy;
@@ -97,7 +101,9 @@ public:
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
 
-  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+  virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
+
+  virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
 
 };/* class SatSolver */