Enable CryptoMiniSat-backed BV proofs

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
   * Specifically, CNF proofs broke when proving tautological clauses.
     Now they don't.

9 files changed, 252 insertions, 20 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 90c0c9b30..b42a464ab 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -221,6 +221,14 @@ void BitVectorProof::printOwnedTerm(Expr term,
   }
 }
 
+void BitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                           std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+}
+
 void BitVectorProof::printBitOf(Expr term,
                                 std::ostream& os,
                                 const ProofLetMap& map)
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index bb875d1d8..c8b197598 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -19,10 +19,13 @@
 #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/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
+#include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
@@ -66,12 +69,12 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(
-      id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+  d_usedClauses.emplace_back(id, clause);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
@@ -84,7 +87,16 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
     Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
     dratProof.outputAsText(Debug("bv::clausal"));
   }
-  Unimplemented();
+
+  // Empty any old record of which atoms for used
+  d_atomsInBitblastingProof.clear();
+
+  // For each used clause, ask the CNF proof which atoms are used in it
+  for (const auto& usedIndexAndClause : d_usedClauses)
+  {
+    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
+                             d_atomsInBitblastingProof);
+  }
 }
 
 void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -101,13 +113,91 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
                                                          std::ostream& paren,
                                                          ProofLetMap& letMap)
 {
-  Unimplemented();
+  os << "\n;; Bitblasting mappings\n";
+  printBitblasting(os, paren);
+
+  os << "\n;; BB-CNF mappings\n";
+  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
+
+  os << "\n;; BB-CNF proofs\n";
+  for (const auto& idAndClause : d_usedClauses)
+  {
+    d_cnfProof->printCnfProofForClause(
+        idAndClause.first, &idAndClause.second, os, paren);
+  }
 }
 
-void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
-                                                      std::ostream& paren)
+void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
 {
-  Unimplemented();
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfSatInput ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ dratProof ";
+  paren << ")";
+  drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(drat_proof_of_bottom _ proofOfSatInput dratProof "
+     << "\n)";
+}
+
+void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfCMap ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ lratProof ";
+  paren << ")";
+  lrat::LratProof pf =
+      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  pf.outputAsLfsc(os);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(lrat_proof_of_bottom _ proofOfCMap lratProof "
+     << "\n)";
+}
+
+void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                 std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  er::ErProof pf =
+      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+
+  pf.outputAsLfsc(os);
 }
 
 }  // namespace proof
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index 85e409e0d..9e95bdb18 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -61,8 +61,7 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
-      d_usedClauses;
+  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
   // Stores the proof recieved from the SAT solver.
   std::ostringstream d_binaryDratProof;
 };
@@ -77,7 +76,6 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
                             TheoryProofEngine* proofEngine)
       : ClausalBitVectorProof(bv, proofEngine)
   {
-    // That's all!
   }
 
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -87,6 +85,49 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
   void printBBDeclarationAndCnf(std::ostream& os,
                                 std::ostream& paren,
                                 ProofLetMap& letMap) override;
+};
+
+/**
+ * A DRAT proof for a bitvector problem
+ */
+class LfscDratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An LRAT proof for a bitvector problem
+ */
+class LfscLratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An Extended Resolution proof for a bitvector problem
+ */
+class LfscErBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 };
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 4e8d20162..ea6df1cc8 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -349,6 +349,40 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
   }
 }
 
+// Actually returns std::optional<std::pair<unsigned, unsigned>>
+// First field is true if the option is filled.
+// Detects whether a clause has x v ~x for some x
+// If so, returns the positive occurence's idx first, then the negative's
+std::tuple<bool, unsigned, unsigned> CnfProof::detectTrivialTautology(
+    const prop::SatClause& clause)
+{
+  // a map from a SatVariable to its previous occurence's polarity and location
+  std::map<prop::SatVariable, std::pair<bool, unsigned>> varsToPolsAndIndices;
+  for (unsigned i = 0; i < clause.size(); ++i)
+  {
+    prop::SatLiteral lit = clause[i];
+    prop::SatVariable var = lit.getSatVariable();
+    bool polarity = !lit.isNegated();
+
+    // Check if this var has already occured w/ opposite polarity
+    auto iter = varsToPolsAndIndices.find(var);
+    if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
+    {
+      if (iter->second.first)
+      {
+        return std::make_tuple(true, iter->second.second, i);
+      }
+      else
+      {
+        return std::make_tuple(true, i, iter->second.second);
+      }
+    }
+    varsToPolsAndIndices[var] = std::make_pair(polarity, i);
+  }
+  return std::make_tuple(false, 0, 0);
+}
+
+
 void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
                                     std::ostream& os,
                                     std::ostream& paren) {
@@ -431,6 +465,31 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
   Assert( clause->size()>0 );
 
+  // If the clause contains x v ~x, it's easy!
+  //
+  // It's important to check for this case, because our other logic for
+  // recording the location of variables in the clause assumes the clause is
+  // not tautological
+  std::tuple<bool, unsigned, unsigned> isTrivialTaut =
+      detectTrivialTautology(*clause);
+  if (std::get<0>(isTrivialTaut))
+  {
+    unsigned posIndexInClause = std::get<1>(isTrivialTaut);
+    unsigned negIndexInClause = std::get<2>(isTrivialTaut);
+    Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
+                    << negIndexInClause << " (-) make this clause a taut"
+                    << std::endl;
+
+    std::string proofOfPos =
+        ProofManager::getLitName((*clause)[negIndexInClause], d_name);
+    std::string proofOfNeg =
+        ProofManager::getLitName((*clause)[posIndexInClause], d_name);
+    os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
+  }
+  else
+  {
+
+
   Node base_assertion = getDefinitionForClause(id);
 
   //get the assertion for the clause id
@@ -776,6 +835,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
     Trace("cnf-pf") << std::endl;
     os << "trust-bad";
   }
+  }
 
   os << ")" << clause_paren.str()
      << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 78ddeebd0..323a013a1 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -164,6 +164,12 @@ public:
                            std::ostream& paren,
                            ProofLetMap &letMap) = 0;
 
+  // Actually returns std::optional<std::pair<unsigned, unsigned>>
+  // First field is true if the option is filled.
+  // Detects whether a clause has x v ~x for some x
+  // If so, returns the positive occurence's idx first, then the negative's
+  static std::tuple<bool, unsigned, unsigned> detectTrivialTautology(
+      const prop::SatClause& clause);
   virtual void printClause(const prop::SatClause& clause,
                            std::ostream& os,
                            std::ostream& paren) = 0;
diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp
index c2f2fa49e..5b9487a00 100644
--- a/src/proof/drat/drat_proof.cpp
+++ b/src/proof/drat/drat_proof.cpp
@@ -259,12 +259,12 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     {
       case ADDITION:
       {
-        os << "DRATProofa";
+        os << "DRATProofa ";
         break;
       }
       case DELETION:
       {
-        os << "DRATProofd";
+        os << "DRATProofd ";
         break;
       }
       default: { Unreachable("Unrecognized DRAT instruction kind");
@@ -273,7 +273,7 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     for (const SatLiteral& l : i.d_clause)
     {
       os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
-         << ProofManager::getVarName(l.getSatVariable()) << ") ";
+         << ProofManager::getVarName(l.getSatVariable(), "bb") << ") ";
     }
     os << "cln";
     std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 452b64b11..63072ad96 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -132,8 +132,6 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   dratStream.close();
   tracecheckStream.close();
 
-
-
   return proof;
 }
 
@@ -156,6 +154,15 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     {
       Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
       Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          traceCheckClause{d_tracecheck.d_lines[i].d_clause.begin(),
+                           d_tracecheck.d_lines[i].d_clause.end()};
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          originalClause{usedClauses[i].second.begin(),
+                         usedClauses[i].second.end()};
+      Assert(traceCheckClause == originalClause);
+      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
       Assert(d_tracecheck.d_lines[i].d_clause.size()
              == usedClauses[i].second.size());
       for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
@@ -185,7 +192,7 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     // Look at the negation of the second literal in the second clause to get
     // the old literal
     AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
-        "Malformed definition in TRACECHECK proof from drat2er");
+                 "Malformed definition in TRACECHECK proof from drat2er");
     d_definitions.emplace_back(newVar,
                                ~d_tracecheck.d_lines[i + 1].d_clause[1],
                                std::move(otherLiterals));
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9878972bf..42396cd6a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -730,8 +730,7 @@ void LFSCProof::toStream(std::ostream& out) const
 
   out << ";; Printing final unsat proof \n";
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
-    proof::LFSCProofPrinter::printResolutionEmptyClause(
-        ProofManager::getBitVectorProof()->getSatProof(), out, paren);
+    ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
   } else {
     // print actual resolution proof
     proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index fe9acfef3..b5175e1f6 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -85,8 +85,29 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
             && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
         {
-          proof::BitVectorProof* bvp =
-              new proof::LfscClausalBitVectorProof(thBv, this);
+          proof::BitVectorProof* bvp = nullptr;
+          switch (options::bvProofFormat())
+          {
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT:
+              {
+                bvp = new proof::LfscDratBitVectorProof(thBv, this);
+                break;
+              }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT:
+              {
+                bvp = new proof::LfscLratBitVectorProof(thBv, this);
+                break;
+              }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER:
+              {
+                bvp = new proof::LfscErBitVectorProof(thBv, this);
+                break;
+              }
+            default:
+              {
+                Unreachable("Invalid BvProofFormat");
+              }
+          };
           d_theoryProofTable[id] = bvp;
         }
         else