diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/proof/CMakeLists.txt | 7 | ||||
-rw-r--r-- | test/unit/proof/drat_proof_black.h | 187 | ||||
-rw-r--r-- | test/unit/proof/er_proof_black.h | 464 | ||||
-rw-r--r-- | test/unit/proof/lfsc_proof_printer_black.h | 118 | ||||
-rw-r--r-- | test/unit/proof/lrat_proof_black.h | 97 | ||||
-rw-r--r-- | test/unit/proof/utils.h | 34 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 60 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 7 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 9 |
10 files changed, 25 insertions, 959 deletions
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index bd7c1ea22..bd7029c54 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -107,7 +107,6 @@ add_subdirectory(expr) add_subdirectory(main) add_subdirectory(parser) add_subdirectory(prop) -add_subdirectory(proof) add_subdirectory(theory) add_subdirectory(preprocessing) add_subdirectory(util) diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt deleted file mode 100644 index 315c78d6f..000000000 --- a/test/unit/proof/CMakeLists.txt +++ /dev/null @@ -1,7 +0,0 @@ -#-----------------------------------------------------------------------------# -# Add unit tests - -cvc4_add_unit_test_black(drat_proof_black proof) -cvc4_add_unit_test_black(er_proof_black proof) -cvc4_add_unit_test_black(lrat_proof_black proof) -cvc4_add_unit_test_black(lfsc_proof_printer_black proof) diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h deleted file mode 100644 index 4b593a588..000000000 --- a/test/unit/proof/drat_proof_black.h +++ /dev/null @@ -1,187 +0,0 @@ -/********************* */ -/*! \file drat_proof_black.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the DRAT proof class - ** - ** In particular, tests DRAT binary parsing. - **/ - -#include <cxxtest/TestSuite.h> - -#include <cctype> - -#include "proof/drat/drat_proof.h" - -using namespace CVC4::proof::drat; - -class DratProofBlack : public CxxTest::TestSuite -{ - public: - void setUp() override {} - void tearDown() override {} - - void testParseOneAdd(); - void testParseOneMediumAdd(); - void testParseOneBigAdd(); - void testParseLiteralIsTooBig(); - void testParseLiteralOverflow(); - void testParseClauseOverflow(); - - void testParseTwo(); - - void testOutputTwoAsText(); - void testOutputTwoAsLfsc(); -}; - -void DratProofBlack::testParseOneAdd() -{ - // a 1; - 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)); -} - -void DratProofBlack::testParseOneMediumAdd() -{ - // a -255; - 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)); -} - -void DratProofBlack::testParseOneBigAdd() -{ - // a -2199023255551; - 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)); -} - -void DratProofBlack::testParseLiteralIsTooBig() -{ - 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&); -} - -void DratProofBlack::testParseLiteralOverflow() -{ - std::string input("a\x80", 2); - TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&); -} - -void DratProofBlack::testParseClauseOverflow() -{ - std::string input("a\x80\x01", 3); - TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&); -} - -void DratProofBlack::testParseTwo() -{ - // 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); - - 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()[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)); -} - -void DratProofBlack::testOutputTwoAsText() -{ - // 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 output; - proof.outputAsText(output); - - std::istringstream tokens(output.str()); - std::string token; - - tokens >> token; - TS_ASSERT_EQUALS(token, "d"); - - tokens >> token; - TS_ASSERT_EQUALS(token, "-63"); - - tokens >> token; - TS_ASSERT_EQUALS(token, "-8193"); - - tokens >> token; - TS_ASSERT_EQUALS(token, "0"); - - tokens >> token; - TS_ASSERT_EQUALS(token, "129"); - - tokens >> token; - TS_ASSERT_EQUALS(token, "-8191"); - - 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 bb.v62) (clc (neg bb.v8192) cln))" - "(DRATProofa (clc (pos bb.v128) (clc (neg bb.v8190) cln))" - "DRATProofn))"; - std::ostringstream expectedLfscWithoutWhitespace; - for (char c : expectedLfsc) - { - if (!std::isspace(c)) - { - expectedLfscWithoutWhitespace << c; - } - } - - TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(), - expectedLfscWithoutWhitespace.str()); -} diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h deleted file mode 100644 index d9178e34e..000000000 --- a/test/unit/proof/er_proof_black.h +++ /dev/null @@ -1,464 +0,0 @@ -/********************* */ -/*! \file er_proof_black.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the ER proof class - ** - ** In particular, tests TRACECHECK parsing and ER LFSC output. - **/ - -#include <cxxtest/TestSuite.h> - -#include <algorithm> -#include <cctype> -#include <iostream> -#include <iterator> -#include <string> -#include <unordered_map> -#include <vector> - -#include "base/configuration_private.h" -#include "proof/clause_id.h" -#include "proof/er/er_proof.h" -#include "prop/sat_solver_types.h" -#include "utils.h" - -#if IS_LFSC_BUILD -#include "lfscc.h" - -namespace CVC4 { -namespace proof { -extern const char* const plf_signatures; -} // namespace proof -} // namespace CVC4 -#endif - - -using namespace CVC4; -using namespace CVC4::proof::er; -using namespace CVC4::prop; - -class ErProofBlack : public CxxTest::TestSuite -{ - public: - void setUp() override {} - void tearDown() override {} - - void testTraceCheckParse1Line(); - void testTraceCheckParse5Lines(); - void testErTraceCheckParse(); - void testErTraceCheckOutput(); - void testErTraceCheckOutputMedium(); -}; - -/** - * @brief Add a new clause to the clause store and list of used clauses - * - * @param clauses the clause store - * @param usedIds the used clauses - * @param id the id of the new clause - * @param clause the clause itself - */ -void addClause(std::unordered_map<ClauseId, SatClause>& clauses, - std::vector<ClauseId>& usedIds, - ClauseId id, - SatClause&& clause) -{ - clauses.emplace(id, std::move(clause)); - usedIds.push_back(id); -} - -void ErProofBlack::testTraceCheckParse1Line() -{ - std::string tracecheckText = "1 -2 3 0 4 2 0\n"; - std::istringstream stream(tracecheckText); - TraceCheckProof pf = TraceCheckProof::fromText(stream); - TS_ASSERT_EQUALS(pf.d_lines.size(), 1); - - TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 2); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(1, true)); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(2, false)); - TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 2); - TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[0], 4); - TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[1], 2); -} - -void ErProofBlack::testTraceCheckParse5Lines() -{ - std::string tracecheckText = - "1 1 -2 3 0 0\n" - "2 -1 0 0\n" - "3 2 0 0\n" - "4 -3 0 0\n" - "5 0 1 2 4 3 0\n"; - std::istringstream stream(tracecheckText); - TraceCheckProof pf = TraceCheckProof::fromText(stream); - TS_ASSERT_EQUALS(pf.d_lines.size(), 5); - - TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1); - TS_ASSERT_EQUALS(pf.d_lines[4].d_idx, 5); - - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 3); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(0, false)); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(1, true)); - TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[2], SatLiteral(2, false)); - TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 0); - - TS_ASSERT_EQUALS(pf.d_lines[4].d_chain.size(), 4); - TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[0], 1); - TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[1], 2); - TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[2], 4); - TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[3], 3); - TS_ASSERT_EQUALS(pf.d_lines[4].d_clause.size(), 0); -} - -void ErProofBlack::testErTraceCheckParse() -{ - std::string tracecheckText = - "1 1 2 -3 0 0\n" - "2 -1 -2 3 0 0\n" - "3 2 3 -4 0 0\n" - "4 -2 -3 4 0 0\n" - "5 -1 -3 -4 0 0\n" - "6 1 3 4 0 0\n" - "7 -1 2 4 0 0\n" - "8 1 -2 -4 0 0\n" - "9 5 0 0\n" - "10 5 1 0 0\n" - "11 4 5 2 0 10 7 0\n" - "12 -4 5 -3 0 10 5 0\n" - "13 3 5 -2 0 10 2 0\n" - "14 -2 -4 0 2 5 8 0\n" - "15 4 3 0 7 2 6 0\n" - "16 2 -3 0 7 5 1 0\n" - "17 2 0 3 15 16 0\n" - "18 0 4 15 14 17 0\n"; - std::istringstream stream(tracecheckText); - TraceCheckProof tc = TraceCheckProof::fromText(stream); - - std::unordered_map<ClauseId, SatClause> clauses; - std::vector<ClauseId> usedIds; - addClause( - clauses, - usedIds, - 1, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); - addClause( - clauses, - usedIds, - 2, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); - addClause( - clauses, - usedIds, - 3, - std::vector<SatLiteral>{ - SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 4, - std::vector<SatLiteral>{ - SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); - addClause(clauses, - usedIds, - 5, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 6, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 7, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 8, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); - ErProof pf(clauses, usedIds, std::move(tc)); - - TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1); - TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8); - - TS_ASSERT_EQUALS(pf.getDefinitions().size(), 1) - TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_newVariable, SatVariable(4)); - TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_oldLiteral, SatLiteral(0, true)); - TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_otherLiterals.size(), 0); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines.size(), 18); - - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_idx, 1); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17); - - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0], - SatLiteral(0, false)); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1], - SatLiteral(1, false)); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2], - SatLiteral(2, true)); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0); - - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0], - SatLiteral(1, false)); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15); - TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[2], 16); -} - -void ErProofBlack::testErTraceCheckOutput() -{ - std::string tracecheckText = - "1 1 2 -3 0 0\n" - "2 -1 -2 3 0 0\n" - "3 2 3 -4 0 0\n" - "4 -2 -3 4 0 0\n" - "5 -1 -3 -4 0 0\n" - "6 1 3 4 0 0\n" - "7 -1 2 4 0 0\n" - "8 1 -2 -4 0 0\n" - "9 5 0 0\n" - "10 5 1 0 0\n" - "11 4 5 2 0 10 7 0\n" - "12 -4 5 -3 0 10 5 0\n" - "13 3 5 -2 0 10 2 0\n" - "14 -2 -4 0 2 5 8 0\n" - "15 4 3 0 7 2 6 0\n" - "16 2 -3 0 7 5 1 0\n" - "17 2 0 3 15 16 0\n" - "18 0 4 15 14 17 0\n"; - std::istringstream stream(tracecheckText); - TraceCheckProof tc = TraceCheckProof::fromText(stream); - - std::unordered_map<ClauseId, SatClause> clauses; - std::vector<ClauseId> usedIds; - addClause( - clauses, - usedIds, - 1, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); - addClause( - clauses, - usedIds, - 2, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); - addClause( - clauses, - usedIds, - 3, - std::vector<SatLiteral>{ - SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 4, - std::vector<SatLiteral>{ - SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); - addClause(clauses, - usedIds, - 5, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 6, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 7, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 8, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); - ErProof pf(clauses, usedIds, std::move(tc)); - - std::ostringstream lfsc; - pf.outputAsLfsc(lfsc); - - std::string out = R"EOF( - (decl_definition - (neg bb.v0) - cln - (\ er.v4 - (\ er.def4 - (clausify_definition _ _ _ er.def4 _ - (\ er.c9 - (\ er.c10 - (\ er.cnf4 - (satlem_simplify _ _ _ - (R _ _ er.c10 bb.pb7 bb.v0) (\ er.c11 - (satlem_simplify _ _ _ - (R _ _ er.c10 bb.pb5 bb.v0) (\ er.c12 - (satlem_simplify _ _ _ - (R _ _ er.c10 bb.pb2 bb.v0) (\ er.c13 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c14 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c15 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c16 - (satlem_simplify _ _ _ - (R _ _ (Q _ _ bb.pb3 er.c15 bb.v3) er.c16 bb.v2) (\ er.c17 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c15 bb.v2) er.c14 bb.v3) - er.c17 bb.v1) (\ er.c18 - er.c18 ; (holds cln) - )))))))))))))))) - ))) - ) - )) - ) - )EOF"; - - TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out)); -} - -/** - * This proof has been specially constructed to stress-test the proof - * machinery, while still being short. It's a bit meandering... - */ -void ErProofBlack::testErTraceCheckOutputMedium() -{ - std::string tracecheckText = - "1 1 2 -3 0 0\n" - "2 -1 -2 3 0 0\n" - "3 2 3 -4 0 0\n" - "4 -2 -3 4 0 0\n" - "5 -1 -3 -4 0 0\n" - "6 1 3 4 0 0\n" - "7 -1 2 4 0 0\n" - "8 1 -2 -4 0 0\n" - - "9 5 2 4 0 0\n" // Definition with 2 other variables - "10 5 1 0 0\n" - "11 2 -5 -1 0 0\n" - "12 4 -5 -1 0 0\n" - - "13 6 0 0\n" // Definition with no other variables - "14 6 -3 0 0\n" - - "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses - - "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof - "17 4 3 0 7 2 6 0\n" - "18 2 -3 0 7 5 1 0\n" - "19 2 0 3 17 18 0\n" - "20 0 4 17 16 19 0\n"; - - std::istringstream stream(tracecheckText); - TraceCheckProof tc = TraceCheckProof::fromText(stream); - - std::unordered_map<ClauseId, SatClause> clauses; - std::vector<ClauseId> usedIds; - addClause( - clauses, - usedIds, - 1, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); - addClause( - clauses, - usedIds, - 2, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); - addClause( - clauses, - usedIds, - 3, - std::vector<SatLiteral>{ - SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 4, - std::vector<SatLiteral>{ - SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); - addClause(clauses, - usedIds, - 5, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); - addClause( - clauses, - usedIds, - 6, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 7, - std::vector<SatLiteral>{ - SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); - addClause( - clauses, - usedIds, - 8, - std::vector<SatLiteral>{ - SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); - ErProof pf(clauses, usedIds, std::move(tc)); - - std::ostringstream actual_pf_body; - pf.outputAsLfsc(actual_pf_body); - -#if IS_LFSC_BUILD - std::string pf_header = R"EOF( - (check - (% bb.v0 var - (% bb.v1 var - (% bb.v2 var - (% bb.v3 var - (% bb.pb1 (holds (clc (pos bb.v0) (clc (pos bb.v1) (clc (neg bb.v2) cln)))) - (% bb.pb2 (holds (clc (neg bb.v0) (clc (neg bb.v1) (clc (pos bb.v2) cln)))) - (% bb.pb3 (holds (clc (pos bb.v1) (clc (pos bb.v2) (clc (neg bb.v3) cln)))) - (% bb.pb4 (holds (clc (neg bb.v1) (clc (neg bb.v2) (clc (pos bb.v3) cln)))) - (% bb.pb5 (holds (clc (neg bb.v0) (clc (neg bb.v2) (clc (neg bb.v3) cln)))) - (% bb.pb6 (holds (clc (pos bb.v0) (clc (pos bb.v2) (clc (pos bb.v3) cln)))) - (% bb.pb7 (holds (clc (neg bb.v0) (clc (pos bb.v1) (clc (pos bb.v3) cln)))) - (% bb.pb8 (holds (clc (pos bb.v0) (clc (neg bb.v1) (clc (neg bb.v3) cln)))) - (: (holds cln) - )EOF"; - - std::string pf_footer = R"EOF( - ) - )))))))) - )))) - ) - )EOF"; - - std::stringstream actual_pf; - actual_pf << proof::plf_signatures << pf_header << actual_pf_body.str() << pf_footer; - - lfscc_init(); - lfscc_check_file(actual_pf, false, false, false, false, false, false, false); -#endif -} diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h deleted file mode 100644 index 74fda4996..000000000 --- a/test/unit/proof/lfsc_proof_printer_black.h +++ /dev/null @@ -1,118 +0,0 @@ -/********************* */ -/*! \file lfsc_proof_printer_black.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of LFSC proof printing - **/ - -#include <cxxtest/TestSuite.h> - -#include "proof/lfsc_proof_printer.h" -#include "prop/sat_solver_types.h" -#include "proof/clause_id.h" - -using namespace CVC4::proof; -using namespace CVC4::prop; - -class LfscProofPrinterBlack : public CxxTest::TestSuite -{ - public: - void setUp() override {} - void tearDown() override {} - - void testPrintClause(); - void testPrintSatInputProof(); - void testPrintCMapProof(); -}; - -void LfscProofPrinterBlack::testPrintClause() -{ - SatClause clause{ - SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, false)}; - std::ostringstream lfsc; - - LFSCProofPrinter::printSatClause(clause, lfsc, ""); - - std::string expectedLfsc = - "(clc (pos .v0) " - "(clc (neg .v1) " - "(clc (pos .v3) " - "cln)))"; - - TS_ASSERT_EQUALS(lfsc.str(), expectedLfsc); -} - -void LfscProofPrinterBlack::testPrintSatInputProof() -{ - std::vector<CVC4::ClauseId> ids{2, 40, 3}; - std::ostringstream lfsc; - - LFSCProofPrinter::printSatInputProof(ids, lfsc, ""); - - std::string expectedLfsc = - "(cnfc_proof _ _ _ .pb2 " - "(cnfc_proof _ _ _ .pb40 " - "(cnfc_proof _ _ _ .pb3 " - "cnfn_proof)))"; - - std::ostringstream lfscWithoutWhitespace; - for (char c : lfsc.str()) - { - if (!std::isspace(c)) - { - lfscWithoutWhitespace << c; - } - } - std::ostringstream expectedLfscWithoutWhitespace; - for (char c : expectedLfsc) - { - if (!std::isspace(c)) - { - expectedLfscWithoutWhitespace << c; - } - } - - TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(), - expectedLfscWithoutWhitespace.str()); -} - -void LfscProofPrinterBlack::testPrintCMapProof() -{ - std::vector<CVC4::ClauseId> ids{2, 40, 3}; - std::ostringstream lfsc; - - LFSCProofPrinter::printCMapProof(ids, lfsc, ""); - - std::string expectedLfsc = - "(CMapc_proof 1 _ _ _ .pb2 " - "(CMapc_proof 2 _ _ _ .pb40 " - "(CMapc_proof 3 _ _ _ .pb3 " - "CMapn_proof)))"; - - std::ostringstream lfscWithoutWhitespace; - for (char c : lfsc.str()) - { - if (!std::isspace(c)) - { - lfscWithoutWhitespace << c; - } - } - std::ostringstream expectedLfscWithoutWhitespace; - for (char c : expectedLfsc) - { - if (!std::isspace(c)) - { - expectedLfscWithoutWhitespace << c; - } - } - - TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(), - expectedLfscWithoutWhitespace.str()); -} diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h deleted file mode 100644 index 8d91fee33..000000000 --- a/test/unit/proof/lrat_proof_black.h +++ /dev/null @@ -1,97 +0,0 @@ -/********************* */ -/*! \file lrat_proof_black.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the LRAT proof class - ** - ** In particular, tests LRAT LFSC output. - **/ - -#include <cxxtest/TestSuite.h> - -#include <iostream> - -#include "proof/lrat/lrat_proof.h" -#include "prop/sat_solver_types.h" -#include "utils.h" - -using namespace CVC4; -using namespace CVC4::proof::lrat; -using namespace CVC4::prop; - -class LratProofBlack : public CxxTest::TestSuite -{ - public: - void setUp() override {} - void tearDown() override {} - - void testOutputAsLfsc(); -}; - -void LratProofBlack::testOutputAsLfsc() -{ - std::vector<std::unique_ptr<LratInstruction>> instructions; - - // 6 d 1 2 - std::vector<ClauseIdx> clausesToDelete{1, 2}; - std::unique_ptr<LratDeletion> deletion = std::unique_ptr<LratDeletion>( - new LratDeletion(6, std::move(clausesToDelete))); - instructions.push_back(std::move(deletion)); - - // 7 1 2 0 5 2 0 - std::vector<SatLiteral> firstAddedClause{SatLiteral(1, false), - SatLiteral(2, false)}; - LratUPTrace firstTrace{5, 2}; - std::vector<std::pair<ClauseIdx, LratUPTrace>> firstHints; - std::unique_ptr<LratAddition> add1 = - std::unique_ptr<LratAddition>(new LratAddition( - 7, std::move(firstAddedClause), std::move(firstTrace), firstHints)); - instructions.push_back(std::move(add1)); - - // 8 2 0 -1 3 -5 2 0 - std::vector<SatLiteral> secondAddedClause{SatLiteral(2, false)}; - LratUPTrace secondTrace; - std::vector<std::pair<ClauseIdx, LratUPTrace>> secondHints; - LratUPTrace secondHints0Trace{3}; - secondHints.emplace_back(1, secondHints0Trace); - LratUPTrace secondHints1Trace{2}; - secondHints.emplace_back(5, secondHints1Trace); - std::unique_ptr<LratAddition> add2 = std::unique_ptr<LratAddition>( - new LratAddition(8, - std::move(secondAddedClause), - std::move(secondTrace), - secondHints)); - instructions.push_back(std::move(add2)); - - LratProof proof(std::move(instructions)); - - std::ostringstream lfsc; - proof.outputAsLfsc(lfsc); - - // 6 d 1 2 - // 7 1 2 0 5 2 0 - // 8 2 0 -1 3 -5 2 0 - std::string expectedLfsc = - "(LRATProofd (CIListc 1 (CIListc 2 CIListn)) " - "(LRATProofa 7 " - " (clc (pos bb.v1) (clc (pos bb.v2) cln))" - " (Tracec 5 (Tracec 2 Tracen))" - " RATHintsn " - "(LRATProofa 8 " - " (clc (pos bb.v2) cln)" - " Tracen " - " (RATHintsc 1 (Tracec 3 Tracen)" - " (RATHintsc 5 (Tracec 2 Tracen)" - " RATHintsn)) " - "LRATProofn)))"; - - TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), - filterWhitespace(expectedLfsc)); -} diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h deleted file mode 100644 index 3db6e2171..000000000 --- a/test/unit/proof/utils.h +++ /dev/null @@ -1,34 +0,0 @@ -/********************* */ -/*! \file utils.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for proof testing - **/ - -#include <algorithm> -#include <string> -#include <cctype> -#include <iterator> - -/** - * Creates a new stream with whitespace removed. - * - * @param s the source string - * - * @return a string without whitespace - */ -std::string filterWhitespace(const std::string& s) -{ - std::string out; - std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) { - return !std::isspace(c); - }); - return out; -} diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index f0253fdbf..33fc15674 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -174,8 +174,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), - false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -189,26 +189,27 @@ class CnfStreamWhite : public CxxTest::TestSuite { Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( d_nodeManager->mkNode( - kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b), + kind::IMPLIES, + d_nodeManager->mkNode(kind::AND, a, b), d_nodeManager->mkNode( - kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d), + kind::EQUAL, + d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode(kind::NOT, d_nodeManager->mkNode(kind::XOR, e, f)))), - false, false, RULE_INVALID, Node::null()); + false, + false); TS_ASSERT(d_satSolver->addClauseCalled()); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false, - RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false, - RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -216,8 +217,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false, - false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::EQUAL, a, b), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -225,33 +226,16 @@ class CnfStreamWhite : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, a, b), - false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } - // ITEs should be removed before going to CNF - // void testIte() { - // NodeManagerScope nms(d_nodeManager); - // d_cnfStream->convertAndAssert( - // d_nodeManager->mkNode( - // kind::EQUAL, - // d_nodeManager->mkNode( - // kind::ITE, - // d_nodeManager->mkVar(d_nodeManager->booleanType()), - // d_nodeManager->mkVar(d_nodeManager->integerType()), - // d_nodeManager->mkVar(d_nodeManager->integerType()) - // ), - // d_nodeManager->mkVar(d_nodeManager->integerType()) - // ), false, false, RULE_INVALID, Node::null()); - // - //} - void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::NOT, a), false, - false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -260,8 +244,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::OR, a, b, c), - false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::OR, a, b, c), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -269,10 +253,10 @@ class CnfStreamWhite : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(a, false, false); TS_ASSERT(d_satSolver->addClauseCalled()); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(b, false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -280,8 +264,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::XOR, a, b), false, - false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::XOR, a, b), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index a67d0aeb2..ae4264aa2 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -41,7 +41,6 @@ #include "theory/theory_rewriter.h" #include "theory/valuation.h" #include "util/integer.h" -#include "util/proof.h" #include "util/rational.h" using namespace CVC4; @@ -55,13 +54,9 @@ using namespace CVC4::theory::bv; using namespace std; class FakeOutputChannel : public OutputChannel { - void conflict(TNode n, std::unique_ptr<Proof> pf) override - { - Unimplemented(); - } + void conflict(TNode n) override { Unimplemented(); } bool propagate(TNode n) override { Unimplemented(); } LemmaStatus lemma(TNode n, - ProofRule rule, LemmaProperty p = LemmaProperty::NONE) override { Unimplemented(); diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 9693000a3..e90bd56a2 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -26,7 +26,6 @@ #include "smt/smt_engine_scope.h" #include "theory/theory.h" #include "theory/theory_engine.h" -#include "util/proof.h" #include "util/resource_manager.h" using namespace CVC4; @@ -48,10 +47,7 @@ class TestOutputChannel : public OutputChannel { ~TestOutputChannel() override {} void safePoint(ResourceManager::Resource r) override {} - void conflict(TNode n, std::unique_ptr<Proof> pf) override - { - push(CONFLICT, n); - } + void conflict(TNode n) override { push(CONFLICT, n); } bool propagate(TNode n) override { push(PROPAGATE, n); @@ -59,7 +55,6 @@ class TestOutputChannel : public OutputChannel { } LemmaStatus lemma(TNode n, - ProofRule rule, LemmaProperty p = LemmaProperty::NONE) override { push(LEMMA, n); @@ -298,7 +293,7 @@ class TheoryBlack : public CxxTest::TestSuite { void testOutputChannel() { Node n = atom0.orNode(atom1); - d_outputChannel.lemma(n, RULE_INVALID); + d_outputChannel.lemma(n); d_outputChannel.split(atom0); Node s = atom0.orNode(atom0.notNode()); TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u); |