#include "proof/lfsc_proof_printer.h"
+#include <algorithm>
#include <iostream>
+#include <iterator>
#include "prop/bvminisat/core/Solver.h"
#include "prop/minisat/core/Solver.h"
printResolution(satProof, satProof->getEmptyClauseId(), out, paren);
}
+void LFSCProofPrinter::printSatInputProof(const std::vector<ClauseId>& 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<char>(out), clauses.size(), ')');
+}
+
+void LFSCProofPrinter::printCMapProof(const std::vector<ClauseId>& 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<char>(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<char>(out), clause.size(), ')');
+}
+
// Template specializations
template void LFSCProofPrinter::printAssumptionsResolution(
TSatProof<CVC4::Minisat::Solver>* satProof,
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<ClauseId>& 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<ClauseId>& 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.
*
# Add unit tests
cvc4_add_unit_test_black(drat_proof_black proof)
+cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
--- /dev/null
+/********************* */
+/*! \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());
+}
projects / cvc5.git / commitdiff