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

1 files changed, 19 insertions, 39 deletions

diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index ccb288f6e..6c2ae589f 100644
--- a/src/proof/resolution_bitvector_proof.h
+++ b/src/proof/resolution_bitvector_proof.h
@@ -24,32 +24,16 @@
 #include "context/context.h"
 #include "expr/expr.h"
 #include "proof/bitvector_proof.h"
+#include "proof/sat_proof.h"
 #include "proof/theory_proof.h"
 #include "prop/bvminisat/core/Solver.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
 
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T>
-class TBitblaster;
-}  // namespace bv
-}  // namespace theory
-
-// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
-// header cycle and remove this.
-namespace prop {
-class CnfStream;
-}
-
-} /* namespace CVC4 */
-
-
-namespace CVC4 {
-
-template <class Solver>
-class TSatProof;
 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
 
 namespace proof {
@@ -76,13 +60,7 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   BVSatProof* getSatProof();
 
-  /**
-   * Kind of a mess.
-   * In eager mode this must be invoked before printing a proof of the empty
-   * clause. In lazy mode the behavior is ???
-   * TODO(aozdemir) clean this up.
-   */
-  void finalizeConflicts(std::vector<Expr>& conflicts);
+  void finalizeConflicts(std::vector<Expr>& conflicts) override;
 
   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
@@ -91,13 +69,14 @@ class ResolutionBitVectorProof : public BitVectorProof
   void markAssumptionConflict() { d_isAssumptionConflict = true; }
   bool isAssumptionConflict() const { return d_isAssumptionConflict; }
 
-  virtual void printResolutionProof(std::ostream& os,
-                                    std::ostream& paren,
-                                    ProofLetMap& letMap) = 0;
-
-  void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
+  void initCnfProof(prop::CnfStream* cnfStream,
+                    context::Context* cnf,
+                    prop::SatVariable trueVar,
+                    prop::SatVariable falseVar) override;
 
  protected:
+  void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
   context::Context d_fakeContext;
 
   // The CNF formula that results from bit-blasting will need a proof.
@@ -106,13 +85,13 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   bool d_isAssumptionConflict;
 
-  theory::TheoryId getTheoryId() override;
 };
 
-class LFSCBitVectorProof : public ResolutionBitVectorProof
+class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
 {
  public:
-  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+  LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv,
+                               TheoryProofEngine* proofEngine)
       : ResolutionBitVectorProof(bv, proofEngine)
   {
   }
@@ -120,9 +99,10 @@ class LFSCBitVectorProof : public ResolutionBitVectorProof
                              std::ostream& os,
                              std::ostream& paren,
                              const ProofLetMap& map) override;
-  void printResolutionProof(std::ostream& os,
-                            std::ostream& paren,
-                            ProofLetMap& letMap) override;
+  void printBBDeclarationAndCnf(std::ostream& os,
+                                std::ostream& paren,
+                                ProofLetMap& letMap) override;
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
   void calculateAtomsInBitblastingProof() override;
 };