LFSC LRAT Output (#2787)

* LFSC ouput & unit test

* Renamed lrat unit test file

* s/DRAT/LRAT/

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Addressed Andres' comments

1. Extracted a filter whitespace function.
2. Added @param annotations.

* Addressing Yoni's comments

Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index d976c1279..fb05bd71b 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -52,6 +52,15 @@ class LratInstruction
    * @param out the stream to write to
    */
   virtual void outputAsText(std::ostream& out) const = 0;
+  /**
+   * Write this LRAT instruction as an LFSC value
+   *
+   * @param out the stream to write to
+   * @param closeParen the stream to write any closing parentheses to
+   *
+   */
+  virtual void outputAsLfsc(std::ostream& o,
+                            std::ostream& closeParen) const = 0;
   virtual ~LratInstruction() = default;
 };
 
@@ -67,6 +76,7 @@ class LratDeletion : public LratInstruction
   LratDeletion() = default;
 
   void outputAsText(std::ostream& out) const override;
+  void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
 
  private:
   // This idx doesn't really matter, but it's in the format anyway, so we parse
@@ -97,6 +107,7 @@ class LratAddition : public LratInstruction
   }
 
   void outputAsText(std::ostream& out) const override;
+  void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
 
  private:
   // The idx for the new clause
@@ -153,6 +164,8 @@ class LratProof
     return d_instructions;
   }
 
+  void outputAsLfsc(std::ostream& o) const;
+
  private:
   // The instructions in the proof. Each is a deletion or addition.
   std::vector<std::unique_ptr<LratInstruction>> d_instructions;