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, 52 insertions, 13 deletions

diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
index 3d8a1b5e6..63c8839b9 100644
--- a/test/unit/proof/drat_proof_black.h
+++ b/test/unit/proof/drat_proof_black.h
@@ -14,9 +14,10 @@
  ** In particular, tests DRAT binary parsing.
  **/
 
-
 #include <cxxtest/TestSuite.h>
 
+#include <cctype>
+
 #include "proof/drat/drat_proof.h"
 
 using namespace CVC4::proof::drat;
@@ -37,6 +38,7 @@ class DratProofBlack : public CxxTest::TestSuite
   void testParseTwo();
 
   void testOutputTwoAsText();
+  void testOutputTwoAsLfsc();
 };
 
 void DratProofBlack::testParseOneAdd()
@@ -45,10 +47,10 @@ void DratProofBlack::testParseOneAdd()
   std::string input("a\x02\x00", 3);
   DratProof proof = DratProof::fromBinary(input);
 
-
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0], SatLiteral(0, false));
+  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
+                   SatLiteral(0, false));
 }
 
 void DratProofBlack::testParseOneMediumAdd()
@@ -57,10 +59,10 @@ void DratProofBlack::testParseOneMediumAdd()
   std::string input("a\xff\x01\x00", 4);
   DratProof proof = DratProof::fromBinary(input);
 
-
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0], SatLiteral(126, true));
+  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
+                   SatLiteral(126, true));
 }
 
 void DratProofBlack::testParseOneBigAdd()
@@ -69,15 +71,16 @@ void DratProofBlack::testParseOneBigAdd()
   std::string input("a\xff\xff\xff\xff\xff\x7f\x00", 8);
   DratProof proof = DratProof::fromBinary(input);
 
-
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0], SatLiteral(2199023255550, true));
+  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
+                   SatLiteral(2199023255550, true));
 }
 
 void DratProofBlack::testParseLiteralIsTooBig()
 {
-  std::string input("a\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f\x00", 14);
+  std::string input("a\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f\x00",
+                    14);
   TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException);
 }
 
@@ -100,16 +103,19 @@ void DratProofBlack::testParseTwo()
   std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
   DratProof proof = DratProof::fromBinary(input);
 
-
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, DELETION);
   TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 2);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0], SatLiteral(62, true));
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[1], SatLiteral(8192, true));
+  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
+                   SatLiteral(62, true));
+  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[1],
+                   SatLiteral(8192, true));
 
   TS_ASSERT_EQUALS(proof.getInstructions()[1].d_kind, ADDITION);
   TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause.size(), 2);
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[0], SatLiteral(128, false));
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[1], SatLiteral(8190, true));
+  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[0],
+                   SatLiteral(128, false));
+  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[1],
+                   SatLiteral(8190, true));
 }
 
 void DratProofBlack::testOutputTwoAsText()
@@ -146,3 +152,36 @@ void DratProofBlack::testOutputTwoAsText()
   tokens >> token;
   TS_ASSERT_EQUALS(token, "0");
 }
+
+void DratProofBlack::testOutputTwoAsLfsc()
+{
+  // d -63 -8193
+  // 129 -8191
+  std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
+  DratProof proof = DratProof::fromBinary(input);
+  std::ostringstream lfsc;
+  proof.outputAsLfsc(lfsc, 2);
+  std::ostringstream lfscWithoutWhitespace;
+  for (char c : lfsc.str())
+  {
+    if (!std::isspace(c))
+    {
+      lfscWithoutWhitespace << c;
+    }
+  }
+  std::string expectedLfsc =
+      "(DRATProofd (clc (neg .v62)  (clc (neg .v8192) cln))"
+      "(DRATProofa (clc (pos .v128) (clc (neg .v8190) cln))"
+      "DRATProofn))";
+  std::ostringstream expectedLfscWithoutWhitespace;
+  for (char c : expectedLfsc)
+  {
+    if (!std::isspace(c))
+    {
+      expectedLfscWithoutWhitespace << c;
+    }
+  }
+
+  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
+                   expectedLfscWithoutWhitespace.str());
+}