LFSC drat output (#2776)

* LFSC drat output

* Addressed Mathias' review

Addressing Mathias' review with the following changes:
* Added a few blank lines
* Added a unit test for LRAT output as LFSC

2 files changed, 53 insertions, 0 deletions

diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp
index 81688321e..c2f2fa49e 100644
--- a/src/proof/drat/drat_proof.cpp
+++ b/src/proof/drat/drat_proof.cpp
@@ -15,7 +15,12 @@
  **/
 
 #include "proof/drat/drat_proof.h"
+
+#include <algorithm>
 #include <bitset>
+#include <iostream>
+
+#include "proof/proof_manager.h"
 
 namespace CVC4 {
 namespace proof {
@@ -241,6 +246,42 @@ void DratProof::outputAsText(std::ostream& os) const
   }
 };
 
+void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
+{
+  for (const DratInstruction& i : d_instructions)
+  {
+    if (indentation > 0)
+    {
+      std::fill_n(std::ostream_iterator<char>(os), indentation, ' ');
+    }
+    os << "(";
+    switch (i.d_kind)
+    {
+      case ADDITION:
+      {
+        os << "DRATProofa";
+        break;
+      }
+      case DELETION:
+      {
+        os << "DRATProofd";
+        break;
+      }
+      default: { Unreachable("Unrecognized DRAT instruction kind");
+      }
+    }
+    for (const SatLiteral& l : i.d_clause)
+    {
+      os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
+         << ProofManager::getVarName(l.getSatVariable()) << ") ";
+    }
+    os << "cln";
+    std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
+    os << "\n";
+  }
+  os << "DRATProofn";
+  std::fill_n(std::ostream_iterator<char>(os), d_instructions.size(), ')');
+}
 }  // namespace drat
 }  // namespace proof
 }  // namespace CVC4
diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h
index 4bd4f4c04..4715b38f4 100644
--- a/src/proof/drat/drat_proof.h
+++ b/src/proof/drat/drat_proof.h
@@ -109,6 +109,18 @@ class DratProof
    */
   void outputAsText(std::ostream& os) const;
 
+  /**
+   * Write the DRAT proof as an LFSC value
+   * The format is from the LFSC signature drat.plf
+   *
+   * Reads the current `ProofManager` to determine what the variables should be
+   * named.
+   *
+   * @param os the stream to write to
+   * @param indentation the number of spaces to indent each proof instruction
+   */
+  void outputAsLfsc(std::ostream& os, uint8_t indentation) const;
+
  private:
   /**
    * Create an DRAT proof with no instructions.