1 files changed, 94 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())