From 517b6ba3bb029470bdb3f230188af1f398b14a91 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 9 Jan 2019 09:18:29 +0100 Subject: [PATCH] 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. --- src/proof/lfsc_proof_printer.cpp | 41 +++++++ src/proof/lfsc_proof_printer.h | 49 +++++++++ test/unit/proof/CMakeLists.txt | 1 + test/unit/proof/lfsc_proof_printer_black.h | 118 +++++++++++++++++++++ 4 files changed, 209 insertions(+) create mode 100644 test/unit/proof/lfsc_proof_printer_black.h diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp index e1fa3acdb..be1259837 100644 --- a/src/proof/lfsc_proof_printer.cpp +++ b/src/proof/lfsc_proof_printer.cpp @@ -16,7 +16,9 @@ #include "proof/lfsc_proof_printer.h" +#include #include +#include #include "prop/bvminisat/core/Solver.h" #include "prop/minisat/core/Solver.h" @@ -144,6 +146,45 @@ void LFSCProofPrinter::printResolutionEmptyClause(TSatProof* satProof, printResolution(satProof, satProof->getEmptyClauseId(), out, paren); } +void LFSCProofPrinter::printSatInputProof(const std::vector& clauses, + std::ostream& out, + const std::string& namingPrefix) +{ + for (auto i = clauses.begin(), end = clauses.end(); i != end; ++i) + { + out << "\n (cnfc_proof _ _ _ " + << ProofManager::getInputClauseName(*i, namingPrefix) << " "; + } + out << "cnfn_proof"; + std::fill_n(std::ostream_iterator(out), clauses.size(), ')'); +} + +void LFSCProofPrinter::printCMapProof(const std::vector& clauses, + std::ostream& out, + const std::string& namingPrefix) +{ + for (size_t i = 0, n = clauses.size(); i < n; ++i) + { + out << "\n (CMapc_proof " << (i + 1) << " _ _ _ " + << ProofManager::getInputClauseName(clauses[i], namingPrefix) << " "; + } + out << "CMapn_proof"; + std::fill_n(std::ostream_iterator(out), clauses.size(), ')'); +} + +void LFSCProofPrinter::printSatClause(const prop::SatClause& clause, + std::ostream& out, + const std::string& namingPrefix) +{ + for (auto i = clause.cbegin(); i != clause.cend(); ++i) + { + out << "(clc " << (i->isNegated() ? "(neg " : "(pos ") + << ProofManager::getVarName(i->getSatVariable(), namingPrefix) << ") "; + } + out << "cln"; + std::fill_n(std::ostream_iterator(out), clause.size(), ')'); +} + // Template specializations template void LFSCProofPrinter::printAssumptionsResolution( TSatProof* satProof, diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h index bf4bfabad..36a3490f7 100644 --- a/src/proof/lfsc_proof_printer.h +++ b/src/proof/lfsc_proof_printer.h @@ -74,7 +74,56 @@ class LFSCProofPrinter std::ostream& out, std::ostream& paren); + /** + * The SAT solver is given a list of clauses. + * Assuming that each clause has alreay been individually proven, + * defines a proof of the input to the SAT solver. + * + * Prints an LFSC value corresponding to the proof, i.e. a value of type + * (cnf_holds ...) + * + * @param clauses The clauses to print a proof of + * @param out The stream to print to + * @param namingPrefix The prefix for LFSC names + */ + static void printSatInputProof(const std::vector& clauses, + std::ostream& out, + const std::string& namingPrefix); + + /** + * The LRAT proof signature uses the concept of a _clause map_ (CMap), which + * represents an indexed collection of (conjoined) clauses. + * + * Specifically, the signatures rely on a proof that a CMap containing the + * clauses given to the SAT solver hold. + * + * Assuming that the individual clauses already have proofs, this function + * prints a proof of the CMap mapping 1 to the first clause, 2 to the second, + * and so on. + * + * That is, it prints a value of type (CMap_holds ...) + * + * @param clauses The clauses to print a proof of + * @param out The stream to print to + * @param namingPrefix The prefix for LFSC names + */ + static void printCMapProof(const std::vector& clauses, + std::ostream& out, + const std::string& namingPrefix); + + /** + * Prints a clause + * + * @param clause The clause to print + * @param out The stream to print to + * @param namingPrefix The prefix for LFSC names + */ + static void printSatClause(const prop::SatClause& clause, + std::ostream& out, + const std::string& namingPrefix); + private: + /** * Maps a clause id to a string identifier used in the LFSC proof. * 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 + +#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 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 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()); +} -- 2.30.2