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, 70 insertions, 2 deletions

diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 466efa6a7..4b897a6c6 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -24,14 +24,28 @@
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
+
 #include "expr/expr.h"
 #include "proof/cnf_proof.h"
 #include "proof/theory_proof.h"
-#include "theory/bv/bitblast/bitblaster.h"
+#include "prop/sat_solver.h"
 #include "theory/bv/theory_bv.h"
 
+// Since TBitblaster and BitVectorProof are cyclically dependent, we need this
+// forward declaration
+namespace CVC4 {
+namespace theory {
+namespace bv {
+template <class T>
+class TBitblaster;
+}
+}  // namespace theory
+}  // namespace CVC4
+
 namespace CVC4 {
 
+namespace proof {
+
 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
@@ -118,6 +132,8 @@ class BitVectorProof : public TheoryProof
    */
   std::unique_ptr<CnfProof> d_cnfProof;
 
+  theory::TheoryId getTheoryId() override;
+
  public:
   void printOwnedTerm(Expr term,
                       std::ostream& os,
@@ -132,6 +148,28 @@ class BitVectorProof : public TheoryProof
   virtual void calculateAtomsInBitblastingProof() = 0;
 
   /**
+   * Prints out a declaration of the bit-blasting, and the subsequent
+   * conversion of the result to CNF
+   *
+   * @param os the stream to print to
+   * @param paren a stream that will be placed at the back of the proof (for
+   *              closing parens)
+   * @param letMap The let-map, which contains information about LFSC
+   *               identifiers and the values they reference.
+   */
+  virtual void printBBDeclarationAndCnf(std::ostream& os,
+                                        std::ostream& paren,
+                                        ProofLetMap& letMap) = 0;
+
+  /**
+   * Prints a proof of the empty clause.
+   *
+   * @param os the stream to print to
+   * @param paren any parentheses to add to the end of the global proof
+   */
+  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+
+  /**
    * Read the d_atomsInBitblastingProof member.
    * See its documentation.
    */
@@ -153,13 +191,41 @@ class BitVectorProof : public TheoryProof
   /**
    * This must be done before registering any terms or atoms, since the CNF
    * proof must reflect the result of bitblasting those
+   *
+   * Feeds the SAT solver's true and false variables into the CNF stream.
    */
-  virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
+  virtual void initCnfProof(prop::CnfStream* cnfStream,
+                            context::Context* cnf,
+                            prop::SatVariable trueVar,
+                            prop::SatVariable falseVar) = 0;
 
   CnfProof* getCnfProof() { return d_cnfProof.get(); }
 
+  /**
+   * Attaches this BVP to the given SAT solver, initializing a SAT proof.
+   *
+   * This must be invoked before `initCnfProof` because a SAT proof must already
+   * exist to initialize a CNF proof.
+   */
+  virtual void attachToSatSolver(prop::SatSolver& sat_solver) = 0;
+
   void setBitblaster(theory::bv::TBitblaster<Node>* bb);
 
+  /**
+   * Kind of a mess. Used for resulution-based BVP's, where in eager mode this
+   * must be invoked before printing a proof of the empty clause. In lazy mode
+   * the behavior and purpose are both highly unclear.
+   *
+   * This exists as a virtual method of BitVectorProof, and not
+   * ResolutionBitVectorProof, because the machinery that invokes it is
+   * high-level enough that it doesn't know the difference between clausal and
+   * resolution proofs.
+   *
+   * TODO(aozdemir) figure out what is going on and clean this up
+   * Issue: https://github.com/CVC4/CVC4/issues/2789
+   */
+  virtual void finalizeConflicts(std::vector<Expr>& conflicts){};
+
  private:
   ExprToString d_exprToVariableName;
 
@@ -206,6 +272,8 @@ class BitVectorProof : public TheoryProof
                          const Node& n2) override;
 };
 
+}  // namespace proof
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__BITVECTOR__PROOF_H */