LFSC drat output (#2776)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 9 Jan 2019 07:29:12 +0000 (08:29 +0100)
committerGitHub <noreply@github.com>
Wed, 9 Jan 2019 07:29:12 +0000 (08:29 +0100)
* 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

src/proof/drat/drat_proof.cpp
src/proof/drat/drat_proof.h
test/unit/proof/drat_proof_black.h

index 81688321ed0a0c6a91500b0b157ab2460c8f008e..c2f2fa49e3c60efab905b68ecfed78d46594b34e 100644 (file)
  **/
 
 #include "proof/drat/drat_proof.h"
+
+#include <algorithm>
 #include <bitset>
+#include <iostream>
+
+#include "proof/proof_manager.h"
 
 namespace CVC4 {
 namespace proof {
@@ -241,6 +246,42 @@ void DratProof::outputAsText(std::ostream& os) const
   }
 };
 
+void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
+{
+  for (const DratInstruction& i : d_instructions)
+  {
+    if (indentation > 0)
+    {
+      std::fill_n(std::ostream_iterator<char>(os), indentation, ' ');
+    }
+    os << "(";
+    switch (i.d_kind)
+    {
+      case ADDITION:
+      {
+        os << "DRATProofa";
+        break;
+      }
+      case DELETION:
+      {
+        os << "DRATProofd";
+        break;
+      }
+      default: { Unreachable("Unrecognized DRAT instruction kind");
+      }
+    }
+    for (const SatLiteral& l : i.d_clause)
+    {
+      os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
+         << ProofManager::getVarName(l.getSatVariable()) << ") ";
+    }
+    os << "cln";
+    std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
+    os << "\n";
+  }
+  os << "DRATProofn";
+  std::fill_n(std::ostream_iterator<char>(os), d_instructions.size(), ')');
+}
 }  // namespace drat
 }  // namespace proof
 }  // namespace CVC4
index 4bd4f4c04fa9a064b9460ae3f5b1669ab4e9a76c..4715b38f4e5d3e4305669dea47fe0cae961ea1f9 100644 (file)
@@ -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.
index 3d8a1b5e6e27742aac88b451844cb3cc70da9e13..63c8839b9921fb33bf4a06006db726231efff752 100644 (file)
  ** 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());
+}