** In particular, tests DRAT binary parsing.
**/
-
#include <cxxtest/TestSuite.h>
+#include <cctype>
+
#include "proof/drat/drat_proof.h"
using namespace CVC4::proof::drat;
void testParseTwo();
void testOutputTwoAsText();
+ void testOutputTwoAsLfsc();
};
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()
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()
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);
}
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()
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());
+}