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.

2 files changed, 107 insertions, 0 deletions

diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 01dfd145f..3b4bac3f0 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -75,6 +75,69 @@ std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace)
   return o;
 }
 
+/**
+ * Print a list of clause indices to go to while doing UP.
+ *
+ * i.e. a value of type Trace
+ *
+ * @param o where to print to
+ * @param trace the trace (list of clauses) to print
+ */
+void printTrace(std::ostream& o, const LratUPTrace& trace)
+{
+  for (ClauseIdx idx : trace)
+  {
+    o << "(Tracec " << idx << " ";
+  }
+  o << "Tracen";
+  std::fill_n(std::ostream_iterator<char>(o), trace.size(), ')');
+}
+
+/**
+ * Print the RAT hints for a clause addition.
+ *
+ * i.e. prints an LFSC value of type RATHints
+ *
+ * @param o where to print to
+ * @param hints the RAT hints to print
+ */
+void printHints(std::ostream& o,
+                const std::vector<std::pair<ClauseIdx, LratUPTrace>>& hints)
+{
+  for (auto& hint : hints)
+  {
+    o << "\n    (RATHintsc " << hint.first << " ";
+    printTrace(o, hint.second);
+    o << " ";
+  }
+  o << "RATHintsn";
+  std::fill_n(std::ostream_iterator<char>(o), hints.size(), ')');
+}
+
+/**
+ * Print an index list
+ *
+ * i.e. prints an LFSC value of type CIList
+ *
+ * @param o where to print to
+ * @param indices the list of indices to print
+ */
+void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
+{
+  // Verify that the indices are sorted!
+  for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
+  {
+    Assert(indices[i] < indices[i + 1]);
+  }
+
+  for (ClauseIdx idx : indices)
+  {
+    o << "(CIListc " << idx << " ";
+  }
+  o << "CIListn";
+  std::fill_n(std::ostream_iterator<char>(o), indices.size(), ')');
+}
+
 }  // namespace
 
 // Prints the LRAT addition line in textual format
@@ -248,6 +311,17 @@ LratProof::LratProof(std::istream& textualProof)
   }
 }
 
+void LratProof::outputAsLfsc(std::ostream& o) const
+{
+  std::ostringstream closeParen;
+  for (const auto& i : d_instructions)
+  {
+    i->outputAsLfsc(o, closeParen);
+  }
+  o << "LRATProofn";
+  o << closeParen.str();
+}
+
 void LratAddition::outputAsText(std::ostream& o) const
 {
   o << d_idxOfClause << " ";
@@ -261,6 +335,18 @@ void LratAddition::outputAsText(std::ostream& o) const
   o << "0\n";
 }
 
+void LratAddition::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const
+{
+  o << "\n    (LRATProofa " << d_idxOfClause << " ";
+  closeParen << ")";
+  LFSCProofPrinter::printSatClause(d_clause, o, "bb");
+  o << " ";
+  printTrace(o, d_atTrace);
+  o << " ";
+  printHints(o, d_resolvants);
+  o << " ";
+}
+
 void LratDeletion::outputAsText(std::ostream& o) const
 {
   o << d_idxOfClause << " d ";
@@ -271,6 +357,14 @@ void LratDeletion::outputAsText(std::ostream& o) const
   o << "0\n";
 }
 
+void LratDeletion::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const
+{
+  o << "\n    (LRATProofd ";
+  closeParen << ")";
+  printIndices(o, d_clauses);
+  o << " ";
+}
+
 std::ostream& operator<<(std::ostream& o, const LratProof& p)
 {
   for (const auto& instr : p.getInstructions())
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;