From 4ec1c04f28293386518582b0257345f84461350d Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 9 Jan 2019 08:29:12 +0100 Subject: [PATCH] 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 --- src/proof/drat/drat_proof.cpp | 41 +++++++++++++++++++ src/proof/drat/drat_proof.h | 12 ++++++ test/unit/proof/drat_proof_black.h | 65 ++++++++++++++++++++++++------ 3 files changed, 105 insertions(+), 13 deletions(-) diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index 81688321e..c2f2fa49e 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -15,7 +15,12 @@ **/ #include "proof/drat/drat_proof.h" + +#include #include +#include + +#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(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(os), i.d_clause.size(), ')'); + os << "\n"; + } + os << "DRATProofn"; + std::fill_n(std::ostream_iterator(os), d_instructions.size(), ')'); +} } // namespace drat } // namespace proof } // namespace CVC4 diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h index 4bd4f4c04..4715b38f4 100644 --- a/src/proof/drat/drat_proof.h +++ b/src/proof/drat/drat_proof.h @@ -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. 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 +#include + #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()); +} -- 2.30.2