diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-09 08:29:12 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-09 08:29:12 +0100 |
commit | 4ec1c04f28293386518582b0257345f84461350d (patch) | |
tree | a31887e11b477588bbfb96009bbff162ea7ff799 /test/unit | |
parent | 1f6fb54967659ff2ee3f8c29a8d306499fcf1299 (diff) |
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
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/proof/drat_proof_black.h | 65 |
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()); +} |