diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-09 09:18:29 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-09 09:18:29 +0100 |
commit | 517b6ba3bb029470bdb3f230188af1f398b14a91 (patch) | |
tree | fb20cff576d97e148d03c40d4543b7ddc8fc0f22 /test/unit/proof | |
parent | 4ec1c04f28293386518582b0257345f84461350d (diff) |
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
Diffstat (limited to 'test/unit/proof')
-rw-r--r-- | test/unit/proof/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/proof/lfsc_proof_printer_black.h | 118 |
2 files changed, 119 insertions, 0 deletions
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt index 9f462f756..8d76644dc 100644 --- a/test/unit/proof/CMakeLists.txt +++ b/test/unit/proof/CMakeLists.txt @@ -2,3 +2,4 @@ # Add unit tests cvc4_add_unit_test_black(drat_proof_black proof) +cvc4_add_unit_test_black(lfsc_proof_printer_black proof) diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h new file mode 100644 index 000000000..27372b62d --- /dev/null +++ b/test/unit/proof/lfsc_proof_printer_black.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \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-2018 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()); +} |