Extract DIMACS Printing (#2800)

Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.

However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.

At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.

5 files changed, 151 insertions, 52 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d9fc80a92..0124bf4f9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -135,6 +135,8 @@ libcvc4_add_sources(
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
+  proof/dimacs_printer.cpp
+  proof/dimacs_printer.h
   proof/drat/drat_proof.cpp
   proof/drat/drat_proof.h
   proof/lemma_proof.cpp
diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs_printer.cpp
new file mode 100644
index 000000000..48199066e
--- /dev/null
+++ b/src/proof/dimacs_printer.cpp
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file dimacs_printer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization for SAT problems as DIMACS
+ **/
+
+#include "proof/dimacs_printer.h"
+
+#include <iostream>
+
+namespace CVC4 {
+namespace proof {
+
+// Prints the literal as a (+) or (-) int
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l)
+{
+  if (l.isNegated())
+  {
+    o << "-";
+  }
+  return o << l.getSatVariable() + 1;
+}
+
+// Prints the clause as a space-separated list of ints
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
+{
+  for (const auto& l : c)
+  {
+    textOut(o, l) << " ";
+  }
+  return o << "0";
+}
+
+void printDimacs(
+    std::ostream& o,
+    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses)
+{
+  size_t maxVar = 0;
+  for (const auto& c : usedClauses)
+  {
+    for (const auto& l : c.second)
+    {
+      if (l.getSatVariable() + 1 > maxVar)
+      {
+        maxVar = l.getSatVariable() + 1;
+      }
+    }
+  }
+  o << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
+  for (const auto& idAndClause : usedClauses)
+  {
+    for (const auto& l : idAndClause.second)
+    {
+      if (l.isNegated())
+      {
+        o << '-';
+      }
+      o << l.getSatVariable() + 1 << " ";
+    }
+    o << "0\n";
+  }
+}
+
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs_printer.h
new file mode 100644
index 000000000..d11adea3f
--- /dev/null
+++ b/src/proof/dimacs_printer.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file dimacs_printer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization for SAT problems as DIMACS
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__DIMACS_PRINTER_H
+#define __CVC4__PROOF__DIMACS_PRINTER_H
+
+#include <iosfwd>
+#include <memory>
+
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+namespace proof {
+
+/**
+ * Prints the literal as a (+) or (-) int
+ * Not operator<< b/c that represents negation as ~
+ *
+ * @param o where to print
+ * @param l the literal to print
+ *
+ * @return the original stream
+ */
+std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l);
+
+/**
+ * Prints the clause as a space-separated list of ints
+ * Not operator<< b/c that represents literal negation as ~
+ *
+ * @param o where to print
+ * @param c the clause to print
+ *
+ * @return the original stream
+ */
+std::ostream& textOut(std::ostream& o, const prop::SatClause& c);
+
+/**
+ * Prints a CNF formula in DIMACS format
+ *
+ * @param o where to print to
+ * @param usedClauses the CNF formula
+ */
+void printDimacs(
+    std::ostream& o,
+    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses);
+
+}  // namespace proof
+}  // namespace CVC4
+
+#endif  // __CVC4__PROOF__DIMACS_PRINTER_H
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 3b4bac3f0..0b7af7aa5 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -26,6 +26,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
+#include "proof/dimacs_printer.h"
 #include "proof/lfsc_proof_printer.h"
 
 #if CVC4_USE_DRAT2ER
@@ -42,27 +43,6 @@ using prop::SatLiteral;
 using prop::SatVariable;
 
 namespace {
-// Prints the literal as a (+) or (-) int
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const SatLiteral& l)
-{
-  if (l.isNegated())
-  {
-    o << "-";
-  }
-  return o << l.getSatVariable();
-}
-
-// Prints the clause as a space-separated list of ints
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const SatClause& c)
-{
-  for (const auto l : c)
-  {
-    textOut(o, l) << " ";
-  }
-  return o << "0";
-}
 
 // Prints the trace as a space-separated list of (+) ints with a space at the
 // end.
@@ -143,8 +123,7 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 // Prints the LRAT addition line in textual format
 
 LratProof LratProof::fromDratProof(
-    const std::unordered_map<ClauseId, SatClause*>& usedClauses,
-    const std::vector<ClauseId>& clauseOrder,
+    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
     const std::string& dratBinary)
 {
   std::ostringstream cmd;
@@ -162,32 +141,7 @@ LratProof LratProof::fromDratProof(
   AlwaysAssert(r > 0);
   close(r);
   std::ofstream formStream(formulaFilename);
-  size_t maxVar = 0;
-  for (auto& c : usedClauses)
-  {
-    for (auto l : *(c.second))
-    {
-      if (l.getSatVariable() + 1 > maxVar)
-      {
-        maxVar = l.getSatVariable() + 1;
-      }
-    }
-  }
-  formStream << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
-  for (auto ci : clauseOrder)
-  {
-    auto iterator = usedClauses.find(ci);
-    Assert(iterator != usedClauses.end());
-    for (auto l : *(iterator->second))
-    {
-      if (l.isNegated())
-      {
-        formStream << '-';
-      }
-      formStream << l.getSatVariable() + 1 << " ";
-    }
-    formStream << "0\n";
-  }
+  printDimacs(formStream, usedClauses);
   formStream.close();
 
   std::ofstream dratStream(dratFilename);
@@ -198,7 +152,8 @@ LratProof LratProof::fromDratProof(
   drat2er::drat_trim::CheckAndConvertToLRAT(
       formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
 #else
-  Unimplemented("LRAT proof production requires drat2er.\n"
+  Unimplemented(
+      "LRAT proof production requires drat2er.\n"
       "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
 #endif
 
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index fb05bd71b..a999e5ca6 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -137,8 +137,7 @@ class LratProof
    * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
    */
   static LratProof fromDratProof(
-      const std::unordered_map<ClauseId, prop::SatClause*>& usedClauses,
-      const std::vector<ClauseId>& clauseOrder,
+      const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
       const std::string& dratBinary);
   /**
    * @brief Construct an LRAT proof from its textual representation