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

1 files changed, 12 insertions, 0 deletions

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.