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

1 files changed, 126 insertions, 93 deletions

diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 63f1cdf63..466efa6a7 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -9,118 +9,166 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Bitvector proof
+ ** \brief Bitvector proof base class
  **
- ** Bitvector proof
+ ** Contains code (e.g. proof printing code) which is common to all bitvector
+ *proofs.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BITVECTOR__PROOF_H
-#define __CVC4__BITVECTOR__PROOF_H
+#ifndef __CVC4__BITVECTOR_PROOF_H
+#define __CVC4__BITVECTOR_PROOF_H
 
-#include <iostream>
 #include <set>
-#include <sstream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
-
 #include "expr/expr.h"
+#include "proof/cnf_proof.h"
 #include "proof/theory_proof.h"
-#include "prop/bvminisat/core/Solver.h"
-
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
 
-namespace prop {
-class CnfStream;
-} /* namespace CVC4::prop */
-
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T> class TBitblaster;
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-
-class CnfProof;
-} /* namespace CVC4 */
-
-namespace CVC4 {
-
-template <class Solver> class TSatProof;
-typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
-
 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
 typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
 typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
 
-class BitVectorProof : public TheoryProof {
-protected:
+/**
+ * A bitvector proof is best understood as having
+ *
+ *    1. A declaration of a "bitblasted formulas" -- boolean formulas
+ *       that are each translations of a BV-literal (a comparison between BVs).
+ *
+ *       (and a proof that each "bitblasted formula" is implied by the
+ *       corresponding BV literal)
+ *
+ *    2. A declaration of a cnf formula equisatisfiable to the bitblasted
+ *       formula
+ *
+ *       (and a proof that each clause is implied by some bitblasted formula)
+ *
+ *    3. A proof of UNSAT from the clauses.
+ *
+ * This class is responsible for 1 & 2. The proof of UNSAT is delegated to a
+ * subclass.
+ */
+class BitVectorProof : public TheoryProof
+{
+ protected:
+  BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
+  virtual ~BitVectorProof(){};
+
+  // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ])
   ExprSet d_declarations;
 
-  ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof
+  // terms and formulas that are actually relevant to the proof
+  ExprSet d_usedBB;
+
+  ExprSet d_seenBBTerms;        // terms that need to be bit-blasted
+  std::vector<Expr> d_bbTerms;  // order of bit-blasting
 
-  ExprSet d_seenBBTerms; // terms that need to be bit-blasted
-  std::vector<Expr> d_bbTerms; // order of bit-blasting
-  ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted
+  /** atoms that need to be bit-blasted,
+   * BV-literals -> (BV-literals <=> bool formula)
+   * where a BV literal is a signed or unsigned comparison.
+   */
+  ExprToExpr d_bbAtoms;
 
   // map from Expr representing normalized lemma to ClauseId in SAT solver
   ExprToClauseId d_bbConflictMap;
-  BVSatProof* d_resolutionProof;
 
-  CnfProof* d_cnfProof;
-
-  bool d_isAssumptionConflict;
   theory::bv::TBitblaster<Node>* d_bitblaster;
+
+  /** In an LFSC proof the manifestation of this expression bit-level
+   * representation will have a string name. This method returns that name.
+   */
   std::string getBBTermName(Expr expr);
 
-  std::map<Expr,std::string> d_constantLetMap;
+  /** A mapping from constant BV terms to identifiers that will refer to them in
+   * an LFSC proof, if constant-letification is enabled.
+   */
+  std::map<Expr, std::string> d_constantLetMap;
+
+  /** Should we introduced identifiers to refer to BV constant terms?  It may
+   * reduce the textual size of a proof!
+   */
   bool d_useConstantLetification;
-  theory::TheoryId getTheoryId() override;
-  context::Context d_fakeContext;
-public:
-  BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
 
-  void initSatProof(CVC4::BVMinisat::Solver* solver);
-  void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
-  void setBitblaster(theory::bv::TBitblaster<Node>* bb);
+  /** Temporary storage for the set of nodes in the bitblasted formula which
+   * correspond to CNF variables eventually used in the proof of unsat on the
+   * CNF formula
+   */
+  std::set<Node> d_atomsInBitblastingProof;
 
-  BVSatProof* getSatProof();
-  CnfProof* getCnfProof() {return d_cnfProof; }
-  void finalizeConflicts(std::vector<Expr>& conflicts);
+  /**
+   * Prints out
+   *   (a) a declaration of bit-level interpretations corresponding to bits in
+   *       the input BV terms.
+   *   (b) a proof that the each BV literal entails a boolean formula on
+   *       bitof expressions.
+   */
+  void printBitblasting(std::ostream& os, std::ostream& paren);
 
-  void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
-  void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
   /**
-   * All the
-   *
-   * @param confl an inconsistent set of bv literals
+   * The proof that the bit-blasted SAT formula is correctly converted to CNF
    */
-  void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
-  void markAssumptionConflict() { d_isAssumptionConflict = true; }
-  bool isAssumptionConflict() { return d_isAssumptionConflict; }
+  std::unique_ptr<CnfProof> d_cnfProof;
+
+ public:
+  void printOwnedTerm(Expr term,
+                      std::ostream& os,
+                      const ProofLetMap& map) override;
+
+  void printOwnedSort(Type type, std::ostream& os) override;
+
+  /**
+   * Populate the d_atomsInBitblastingProof member.
+   * See its documentation
+   */
+  virtual void calculateAtomsInBitblastingProof() = 0;
+
+  /**
+   * Read the d_atomsInBitblastingProof member.
+   * See its documentation.
+   */
+  const std::set<Node>* getAtomsInBitblastingProof();
 
   void registerTermBB(Expr term);
+
+  /**
+   * Informs the proof that the `atom` predicate was bitblasted into the
+   * `atom_bb` term.
+   *
+   * The `atom` term must be a comparison of bitvectors, and the `atom_bb` term
+   * a boolean formula on bitof expressions
+   */
   void registerAtomBB(Expr atom, Expr atom_bb);
 
   void registerTerm(Expr term) override;
 
-  virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
-  virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
-  virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
+  /**
+   * This must be done before registering any terms or atoms, since the CNF
+   * proof must reflect the result of bitblasting those
+   */
+  virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
 
-  virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
-  virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0;
-  virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
-  virtual void calculateAtomsInBitblastingProof() = 0;
-};
+  CnfProof* getCnfProof() { return d_cnfProof.get(); }
+
+  void setBitblaster(theory::bv::TBitblaster<Node>* bb);
 
-class LFSCBitVectorProof: public BitVectorProof {
+ private:
+  ExprToString d_exprToVariableName;
+
+  ExprToString d_assignedAliases;
+  std::map<std::string, std::string> d_aliasToBindDeclaration;
+  std::string assignAlias(Expr expr);
+  bool hasAlias(Expr expr);
 
+  // Functions for printing various BV terms. Helpers for BV's `printOwnedTerm`
   void printConstant(Expr term, std::ostream& os);
   void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
   void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
@@ -128,29 +176,19 @@ class LFSCBitVectorProof: public BitVectorProof {
   void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
   void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
 
-  ExprToString d_exprToVariableName;
-  ExprToString d_assignedAliases;
-  std::map<std::string, std::string> d_aliasToBindDeclaration;
-  std::string assignAlias(Expr expr);
-  bool hasAlias(Expr expr);
+  /**
+   * Prints the LFSC construction of a bblast_term for `term`
+   */
+  void printTermBitblasting(Expr term, std::ostream& os);
 
-  std::set<Node> d_atomsInBitblastingProof;
+  /**
+   * For a given BV-atom (a comparison), prints a proof that that comparison
+   * holds iff the bitblasted equivalent of it holds.
+   * Uses a side-condidition to do the bit-blasting.
+   */
+  void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
+  void printAtomBitblastingToFalse(Expr term, std::ostream& os);
 
-public:
-  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
-    :BitVectorProof(bv, proofEngine)
-  {}
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
-  void printOwnedSort(Type type, std::ostream& os) override;
-  void printTermBitblasting(Expr term, std::ostream& os) override;
-  void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override;
-  void printAtomBitblastingToFalse(Expr term, std::ostream& os) override;
-  void printTheoryLemmaProof(std::vector<Expr>& lemma,
-                             std::ostream& os,
-                             std::ostream& paren,
-                             const ProofLetMap& map) override;
   void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
   void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
   void printDeferredDeclarations(std::ostream& os,
@@ -158,12 +196,7 @@ public:
   void printAliasingDeclarations(std::ostream& os,
                                  std::ostream& paren,
                                  const ProofLetMap& globalLetMap) override;
-  void printBitblasting(std::ostream& os, std::ostream& paren) override;
-  void printResolutionProof(std::ostream& os,
-                            std::ostream& paren,
-                            ProofLetMap& letMap) override;
-  void calculateAtomsInBitblastingProof() override;
-  const std::set<Node>* getAtomsInBitblastingProof() override;
+
   void printConstantDisequalityProof(std::ostream& os,
                                      Expr c1,
                                      Expr c2,