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, 115 insertions, 0 deletions

diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
new file mode 100644
index 000000000..bb875d1d8
--- /dev/null
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file clausal_bitvector_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitvector proof using the DRAT proof format
+ **
+ ** Contains DRAT-specific printing logic.
+ **/
+
+#include "cvc4_private.h"
+
+#include <algorithm>
+#include <iterator>
+#include <set>
+#include "options/bv_options.h"
+#include "proof/clausal_bitvector_proof.h"
+#include "proof/drat/drat_proof.h"
+#include "proof/lfsc_proof_printer.h"
+#include "theory/bv/theory_bv.h"
+
+namespace CVC4 {
+
+namespace proof {
+
+ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
+                                             TheoryProofEngine* proofEngine)
+    : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+{
+}
+
+void ClausalBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver)
+{
+  sat_solver.setClausalProofLog(this);
+}
+
+void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+                                         context::Context* cnf,
+                                         prop::SatVariable trueVar,
+                                         prop::SatVariable falseVar)
+{
+  Assert(d_cnfProof == nullptr);
+  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
+
+  // Create a clause which forces the true variable to be true, and register it
+  int trueClauseId = ClauseId(ProofManager::currentPM()->nextId());
+  // with the CNF proof
+  d_cnfProof->registerTrueUnitClause(trueClauseId);
+  // and with (this) bit-vector proof
+  prop::SatClause c{prop::SatLiteral(trueVar, false)};
+  registerUsedClause(trueClauseId, c);
+
+  // The same for false.
+  int falseClauseId = ClauseId(ProofManager::currentPM()->nextId());
+  d_cnfProof->registerFalseUnitClause(falseClauseId);
+  c[0] = prop::SatLiteral(falseVar, true);
+  registerUsedClause(falseClauseId, c);
+}
+
+void ClausalBitVectorProof::registerUsedClause(ClauseId id,
+                                               prop::SatClause& clause)
+{
+  d_usedClauses.emplace_back(
+      id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+};
+
+void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
+{
+  if (Debug.isOn("bv::clausal"))
+  {
+    std::string serializedDratProof = d_binaryDratProof.str();
+    Debug("bv::clausal") << "binary DRAT proof byte count: "
+                         << serializedDratProof.size() << std::endl;
+    Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
+    drat::DratProof dratProof =
+        drat::DratProof::fromBinary(serializedDratProof);
+
+    Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
+    dratProof.outputAsText(Debug("bv::clausal"));
+  }
+  Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                                      std::ostream& os,
+                                                      std::ostream& paren,
+                                                      const ProofLetMap& map)
+{
+  Unreachable(
+      "Clausal bit-vector proofs should only be used in combination with eager "
+      "bitblasting, which **does not use theory lemmas**");
+}
+
+void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
+                                                         std::ostream& paren,
+                                                         ProofLetMap& letMap)
+{
+  Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                      std::ostream& paren)
+{
+  Unimplemented();
+}
+
+}  // namespace proof
+
+};  // namespace CVC4