From f93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 28 Feb 2019 21:54:08 -0800 Subject: [PATCH] ErProof class with LFSC output (#2812) * ErProof class with LFSC output * Created a TraceCheckProof class * parsable from text * Created an ErProof class * constructible from a TraceCheckProof * writable as LFSC * A bunch of unit tests * Reponded to Mathias's first set of comments. Credits to Mathias for many of the fixes! * Responed to Andres's first set, fixed tests I accidentally deleted a "!" last time, causing stuff to fail. * Use Configuration::isAssertionBuild * Clarified comment * Responded to Andres's 2nd review * Gaurding against a memory error. * Renaming a file. * Aggressively unlinking temporary files. --- src/CMakeLists.txt | 2 + src/proof/er/er_proof.cpp | 383 +++++++++++++++++++++++++++ src/proof/er/er_proof.h | 208 +++++++++++++++ test/unit/proof/CMakeLists.txt | 1 + test/unit/proof/er_proof_black.h | 406 +++++++++++++++++++++++++++++ test/unit/proof/lrat_proof_black.h | 20 +- test/unit/proof/utils.h | 34 +++ 7 files changed, 1035 insertions(+), 19 deletions(-) create mode 100644 src/proof/er/er_proof.cpp create mode 100644 src/proof/er/er_proof.h create mode 100644 test/unit/proof/er_proof_black.h create mode 100644 test/unit/proof/utils.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0124bf4f9..e142ff46c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -139,6 +139,8 @@ libcvc4_add_sources( proof/dimacs_printer.h proof/drat/drat_proof.cpp proof/drat/drat_proof.h + proof/er/er_proof.cpp + proof/er/er_proof.h proof/lemma_proof.cpp proof/lemma_proof.h proof/lfsc_proof_printer.cpp diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp new file mode 100644 index 000000000..452b64b11 --- /dev/null +++ b/src/proof/er/er_proof.cpp @@ -0,0 +1,383 @@ +/********************* */ +/*! \file er_proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 ER Proof Format + ** + ** Declares C++ types that represent an ER/TRACECHECK proof. + ** Defines serialization for these types. + ** + ** You can find details about the way ER is encoded in the TRACECHECK + ** format at these locations: + ** https://github.com/benjaminkiesl/drat2er + ** http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf + **/ + +#include "proof/er/er_proof.h" + +#include +#include +#include +#include +#include +#include + +#include "base/cvc4_assert.h" +#include "base/map_util.h" +#include "proof/dimacs_printer.h" +#include "proof/lfsc_proof_printer.h" +#include "proof/proof_manager.h" + +#if CVC4_USE_DRAT2ER +#include "drat2er.h" +#include "drat2er_options.h" +#endif + +namespace CVC4 { +namespace proof { +namespace er { + +TraceCheckProof TraceCheckProof::fromText(std::istream& in) +{ + TraceCheckProof pf; + TraceCheckIdx idx = 0; + int64_t token = 0; + + // For each line of the proof, start with the idx + // If there is no idx, then you're done! + in >> idx; + for (; !in.eof(); in >> idx) + { + Assert(in.good()); + + // Then parse the clause (it's 0-terminated) + std::vector clause; + in >> token; + for (; token != 0; in >> token) + { + clause.emplace_back(std::abs(token) - 1, token < 0); + } + + // Then parse the chain of literals (it's also 0-terminated) + std::vector chain; + in >> token; + for (; token != 0; in >> token) + { + Assert(token > 0); + chain.push_back(token); + } + + // Add the line to the proof + pf.d_lines.emplace_back(idx, std::move(clause), std::move(chain)); + } + return pf; +} + +ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, + const std::string& dratBinary) +{ + std::ostringstream cmd; + char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX"; + char dratFilename[] = "/tmp/cvc4-drat-XXXXXX"; + char tracecheckFilename[] = "/tmp/cvc4-tracecheck-er-XXXXXX"; + + int r; + r = mkstemp(formulaFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(dratFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(tracecheckFilename); + AlwaysAssert(r > 0); + close(r); + + // Write the formula + std::ofstream formStream(formulaFilename); + printDimacs(formStream, usedClauses); + unlink(formulaFilename); + + // Write the (binary) DRAT proof + std::ofstream dratStream(dratFilename); + dratStream << dratBinary; + unlink(dratFilename); + + // Invoke drat2er +#if CVC4_USE_DRAT2ER + drat2er::TransformDRATToExtendedResolution(formulaFilename, + dratFilename, + tracecheckFilename, + false, + drat2er::options::QUIET); + +#else + Unimplemented( + "ER proof production requires drat2er.\n" + "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); +#endif + + // Parse the resulting TRACECHECK proof into an ER proof. + std::ifstream tracecheckStream(tracecheckFilename); + ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream)); + unlink(tracecheckFilename); + + formStream.close(); + dratStream.close(); + tracecheckStream.close(); + + + + return proof; +} + +ErProof::ErProof(const ClauseUseRecord& usedClauses, + TraceCheckProof&& tracecheck) + : d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck) +{ + // Step zero, save input clause Ids for future printing + std::transform(usedClauses.begin(), + usedClauses.end(), + std::back_inserter(d_inputClauseIds), + [](const std::pair& pair) { + return pair.first; + }); + + // Step one, verify the formula starts the proof + if (Configuration::isAssertionBuild()) + { + for (size_t i = 0, n = usedClauses.size(); i < n; ++i) + { + Assert(d_tracecheck.d_lines[i].d_idx = i + 1); + Assert(d_tracecheck.d_lines[i].d_chain.size() == 0); + Assert(d_tracecheck.d_lines[i].d_clause.size() + == usedClauses[i].second.size()); + for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j) + { + Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]); + } + } + } + + // Step two, identify definitions. They correspond to lines that follow the + // input lines, are in bounds, and have no justifying chain. + for (size_t i = usedClauses.size(), n = d_tracecheck.d_lines.size(); + i < n && d_tracecheck.d_lines[i].d_chain.size() == 0;) + { + prop::SatClause c = d_tracecheck.d_lines[i].d_clause; + Assert(c.size() > 0); + Assert(!c[0].isNegated()); + + // Get the new variable of the definition -- the first variable of the + // first clause + prop::SatVariable newVar = c[0].getSatVariable(); + + // The rest of the literals in the clause of the 'other literals' of the def + std::vector otherLiterals{++c.begin(), c.end()}; + + size_t nLinesForThisDef = 2 + otherLiterals.size(); + // Look at the negation of the second literal in the second clause to get + // the old literal + AlwaysAssert(d_tracecheck.d_lines.size() > i + 1, + "Malformed definition in TRACECHECK proof from drat2er"); + d_definitions.emplace_back(newVar, + ~d_tracecheck.d_lines[i + 1].d_clause[1], + std::move(otherLiterals)); + + // Advance over the lines for this definition + i += nLinesForThisDef; + } +} + +void ErProof::outputAsLfsc(std::ostream& os) const +{ + // How many parens to close? + size_t parenCount = 0; + std::unordered_set newVariables; + + // Print Definitions + for (const ErDefinition& def : d_definitions) + { + os << "\n (decl_rat_elimination_def (" + << (def.d_oldLiteral.isNegated() ? "neg " : "pos ") + << ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb") + << ") "; + LFSCProofPrinter::printSatClause(def.d_otherLiterals, os, "bb"); + os << " (\\ er.v" << def.d_newVariable << " (\\ er.def" + << def.d_newVariable; + newVariables.insert(def.d_newVariable); + } + parenCount += 3 * d_definitions.size(); + + // Clausify Definitions + TraceCheckIdx firstDefClause = d_inputClauseIds.size() + 1; + for (const ErDefinition& def : d_definitions) + { + os << "\n (clausify_rat_elimination_def _ _ _ " + << "er.def " << def.d_newVariable << " _ _ (\\ er.c" << firstDefClause + << " (\\ er.c" << (firstDefClause + 1) << " (\\ er.cnf" + << def.d_newVariable; + + firstDefClause += 2 + def.d_otherLiterals.size(); + } + parenCount += 4 * d_definitions.size(); + + // Unroll proofs of CNFs to proofs of clauses + firstDefClause = d_inputClauseIds.size() + 1; + for (const ErDefinition& def : d_definitions) + { + for (size_t i = 0, n = def.d_otherLiterals.size(); i < n; ++i) + { + os << "\n (cnfc_unroll _ _ "; + os << "er.cnf" << def.d_newVariable; + if (i != 0) + { + os << ".u" << i; + } + os << " (\\ er.c" << (firstDefClause + 2 + i); + os << " (\\ er.cnf" << def.d_newVariable << ".u" << (i + 1); + } + parenCount += 3 * def.d_otherLiterals.size(); + + firstDefClause += 2 + def.d_otherLiterals.size(); + } + + // NB: At this point `firstDefClause` points to the first clause resulting + // from a resolution chain + + // Now, elaborate each resolution chain + for (size_t cId = firstDefClause, nLines = d_tracecheck.d_lines.size(); + cId <= nLines; + ++cId) + { + const std::vector& chain = + d_tracecheck.d_lines[cId - 1].d_chain; + const std::vector pivots = computePivotsForChain(chain); + Assert(chain.size() > 0); + Assert(chain.size() == pivots.size() + 1); + + os << "\n (satlem_simplify _ _ _ "; + parenCount += 1; + + // Print resolution openings (reverse order) + for (int64_t i = pivots.size() - 1; i >= 0; --i) + { + prop::SatLiteral pivot = pivots[i]; + os << "(" << (pivot.isNegated() ? 'Q' : 'R') << " _ _ "; + } + + // Print resolution start + writeIdForClauseProof(os, chain[0]); + os << " "; + + // Print resolution closings (forward order) + for (size_t i = 0, n = pivots.size(); i < n; ++i) + { + prop::SatVariable pivotVar = pivots[i].getSatVariable(); + TraceCheckIdx clauseId = chain[i + 1]; + writeIdForClauseProof(os, clauseId); + os << " "; + if (ContainsKey(newVariables, pivotVar)) + { + // This is a defined variable + os << "er.v" << pivotVar; + } + else + { + os << ProofManager::getVarName(pivotVar, "bb"); + } + os << ") "; + } + os << "(\\ er.c" << cId; + parenCount += 1; + } + + // Write proof of bottom + Assert(d_tracecheck.d_lines.back().d_clause.size() == 0, + "The TRACECHECK proof from drat2er did not prove bottom."); + os << "\n er.c" << d_tracecheck.d_lines.back().d_idx + << " ; (holds cln)\n"; + + // Finally, close the parentheses! + std::fill_n(std::ostream_iterator(os), parenCount, ')'); +} + +namespace { +/** + * Resolves two clauses + * + * @param dest one of the inputs, and the output too. **This is an input and + * output** + * @param src the other input + * + * @return the unique literal that was resolved on, with the polarization that + * it originally had in `dest`. + * + * For example, if dest = (1 3 -4 5) and src = (1 -3 5), then 3 is returned and + * after the call dest = (1 -4 5). + */ +prop::SatLiteral resolveModify( + std::unordered_set& dest, + const prop::SatClause& src) +{ + bool foundPivot = false; + prop::SatLiteral pivot(0, false); + + for (prop::SatLiteral lit : src) + { + auto negationLocation = dest.find(~lit); + if (negationLocation != dest.end()) + { + Assert(!foundPivot); + foundPivot = true; + dest.erase(negationLocation); + pivot = ~lit; + } + dest.insert(lit); + } + + Assert(foundPivot); + return pivot; +} +} // namespace + +std::vector ErProof::computePivotsForChain( + const std::vector& chain) const +{ + std::vector pivots; + + const prop::SatClause& first = d_tracecheck.d_lines[chain[0] - 1].d_clause; + std::unordered_set + runningClause{first.begin(), first.end()}; + + for (auto idx = ++chain.cbegin(), end = chain.cend(); idx != end; ++idx) + { + pivots.push_back( + resolveModify(runningClause, d_tracecheck.d_lines[*idx - 1].d_clause)); + } + return pivots; +} + +void ErProof::writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const +{ + if (i <= d_inputClauseIds.size()) + { + // This clause is an input clause! Ask the ProofManager for its name + o << ProofManager::getInputClauseName(d_inputClauseIds[i - 1], "bb"); + } + else + { + // This clause was introduced by a definition or resolution chain + o << "er.c" << i; + } +} + +} // namespace er +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h new file mode 100644 index 000000000..0a0038738 --- /dev/null +++ b/src/proof/er/er_proof.h @@ -0,0 +1,208 @@ +/********************* */ +/*! \file er_proof.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 ER Proof Format + ** + ** Declares C++ types that represent an ER/TRACECHECK proof. + ** Defines serialization for these types. + ** + ** You can find details about the way ER is encoded in the TRACECHECK + ** format at these locations: + ** https://github.com/benjaminkiesl/drat2er + ** http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__ER__ER_PROOF_H +#define __CVC4__PROOF__ER__ER_PROOF_H + +#include +#include + +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" + +namespace CVC4 { +namespace proof { +namespace er { + +using ClauseUseRecord = std::vector>; + +/** + * A definition of the form: + * newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n) + */ +struct ErDefinition +{ + ErDefinition(prop::SatVariable newVariable, + prop::SatLiteral oldLiteral, + std::vector&& otherLiterals) + : d_newVariable(newVariable), + d_oldLiteral(oldLiteral), + d_otherLiterals(otherLiterals) + { + } + + // newVar + prop::SatVariable d_newVariable; + // p + prop::SatLiteral d_oldLiteral; + // A list of the x_i's + std::vector d_otherLiterals; +}; + +// For representing a clause's index within a TRACECHECK proof. +using TraceCheckIdx = size_t; + +/** + * A single line in a TRACECHECK proof. + * + * Consists of the index of a new clause, the literals of that clause, and the + * indices for preceding clauses which can be combined in a resolution chain to + * produce this new clause. + */ +struct TraceCheckLine +{ + TraceCheckLine(TraceCheckIdx idx, + std::vector&& clause, + std::vector&& chain) + : d_idx(idx), d_clause(clause), d_chain(chain) + { + } + + // The index of the new clause + TraceCheckIdx d_idx; + // The new clause + std::vector d_clause; + /** + * Indices of clauses which must be resolved to produce this new clause. + * While the TRACECHECK format does not specify the order, we require them to + * be in resolution-order. + */ + std::vector d_chain; +}; + +/** + * A TRACECHECK proof -- just a list of lines + */ +struct TraceCheckProof +{ + static TraceCheckProof fromText(std::istream& in); + TraceCheckProof() : d_lines() {} + + // The lines of this proof. + std::vector d_lines; +}; + +/** + * An extended resolution proof. + * It supports resolution, along with extensions of the form + * + * newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n) + */ +class ErProof +{ + public: + /** + * Construct an ER proof from a DRAT proof, using drat2er + * + * @param usedClauses The CNF formula that we're deriving bottom from. + * @param dratBinary The DRAT proof from the SAT solver, as a binary stream. + */ + static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses, + const std::string& dratBinary); + + /** + * Construct an ER proof from a TRACECHECK ER proof + * + * This basically just identifies groups of lines which correspond to + * definitions, and extracts them. + * + * @param usedClauses The CNF formula that we're deriving bottom from. + * @param tracecheck The TRACECHECK proof, as a stream. + */ + ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck); + + /** + * Write the ER proof as an LFSC value of type (holds cln). + * The format is from the LFSC signature er.plf + * + * Reads the current `ProofManager` to determine what the variables should be + * named. + * + * @param os the stream to write to + */ + void outputAsLfsc(std::ostream& os) const; + + const std::vector& getInputClauseIds() const + { + return d_inputClauseIds; + } + + const std::vector& getDefinitions() const + { + return d_definitions; + } + + const TraceCheckProof& getTraceCheckProof() const { return d_tracecheck; } + + private: + /** + * Creates an empty ErProof. + */ + ErProof() : d_inputClauseIds(), d_definitions(), d_tracecheck() {} + + /** + * Computes the pivots on the basis of which an in-order resolution chain is + * resolved. + * + * c0 c1 + * \ / Clauses c_i being resolved in a chain around + * v1 c2 pivots v_i. + * \ / + * v2 c3 + * \ / + * v3 c4 + * \ / + * v4 + * + * + * @param chain the chain, of N clause indices + * + * @return a list of N - 1 variables, the list ( v_i ) from i = 1 to N - 1 + */ + std::vector computePivotsForChain( + const std::vector& chain) const; + + /** + * Write the LFSC identifier for the proof of a clause + * + * @param o where to write to + * @param i the TRACECHECK index for the clause whose proof identifier to + * print + */ + void writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const; + + // A list of the Ids for the input clauses, in order. + std::vector d_inputClauseIds; + // A list of new variable definitions, in order. + std::vector d_definitions; + // The underlying TRACECHECK proof. + TraceCheckProof d_tracecheck; +}; + +} // namespace er +} // namespace proof +} // namespace CVC4 + +#endif // __CVC4__PROOF__ER__ER_PROOF_H diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt index 00c893bdb..315c78d6f 100644 --- a/test/unit/proof/CMakeLists.txt +++ b/test/unit/proof/CMakeLists.txt @@ -2,5 +2,6 @@ # 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/er_proof_black.h b/test/unit/proof/er_proof_black.h new file mode 100644 index 000000000..1620bb113 --- /dev/null +++ b/test/unit/proof/er_proof_black.h @@ -0,0 +1,406 @@ +/********************* */ +/*! \file er_proof_black.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 + +#include +#include +#include +#include +#include + +#include "proof/clause_id.h" +#include "proof/er/er_proof.h" +#include "prop/sat_solver_types.h" +#include "utils.h" + +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(); +}; + +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::vector> usedClauses; + usedClauses.emplace_back( + 1, + std::vector{ + SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); + usedClauses.emplace_back( + 2, + std::vector{ + SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); + usedClauses.emplace_back( + 3, + std::vector{ + SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); + usedClauses.emplace_back( + 4, + std::vector{ + SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); + usedClauses.emplace_back( + 5, + std::vector{ + SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); + usedClauses.emplace_back( + 6, + std::vector{ + SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 7, + std::vector{ + SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 8, + std::vector{ + SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); + ErProof pf(usedClauses, 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::vector> usedClauses; + usedClauses.emplace_back( + 1, + std::vector{ + SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); + usedClauses.emplace_back( + 2, + std::vector{ + SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); + usedClauses.emplace_back( + 3, + std::vector{ + SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); + usedClauses.emplace_back( + 4, + std::vector{ + SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); + usedClauses.emplace_back( + 5, + std::vector{ + SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); + usedClauses.emplace_back( + 6, + std::vector{ + SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 7, + std::vector{ + SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 8, + std::vector{ + SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); + ErProof pf(usedClauses, std::move(tc)); + + std::ostringstream lfsc; + pf.outputAsLfsc(lfsc); + + std::string out = R"EOF( + (decl_rat_elimination_def + (neg bb.v0) + cln + (\ er.v4 + (\ er.def4 + (clausify_rat_elimination_def _ _ _ 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::vector> usedClauses; + usedClauses.emplace_back( + 1, + std::vector{ + SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)}); + usedClauses.emplace_back( + 2, + std::vector{ + SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)}); + usedClauses.emplace_back( + 3, + std::vector{ + SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)}); + usedClauses.emplace_back( + 4, + std::vector{ + SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)}); + usedClauses.emplace_back( + 5, + std::vector{ + SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)}); + usedClauses.emplace_back( + 6, + std::vector{ + SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 7, + std::vector{ + SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)}); + usedClauses.emplace_back( + 8, + std::vector{ + SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); + ErProof pf(usedClauses, std::move(tc)); + + std::ostringstream lfsc; + pf.outputAsLfsc(lfsc); + + std::string out = R"EOF( + (decl_rat_elimination_def + (neg bb.v0) + (clc (pos bb.v1) (clc (pos bb.v3) cln)) + (\ er.v4 + (\ er.def4 + (decl_rat_elimination_def + (pos bb.v2) + cln + (\ er.v5 + (\ er.def5 + (clausify_rat_elimination_def _ _ _ er.def4 _ _ + (\ er.c9 + (\ er.c10 + (\ er.cnf4 + (clausify_rat_elimination_def _ _ _ er.def5 _ _ + (\ er.c13 + (\ er.c14 + (\ er.cnf5 + (cnfc_unroll _ _ er.cnf4 + (\ er.c11 + (\ er.cnf4.u1 + (cnfc_unroll _ _ er.cnf4.u1 + (\ er.c12 + (\ er.cnf4.u2 + (satlem_simplify _ _ _ + (R _ _ (R _ _ (Q _ _ (Q _ _ er.c11 bb.pb1 bb.v0) + er.c10 er.v4) + bb.pb7 bb.v0) + bb.pb4 bb.v1) (\ er.c15 + (satlem_simplify _ _ _ + (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c16 + (satlem_simplify _ _ _ + (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c17 + (satlem_simplify _ _ _ + (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c18 + (satlem_simplify _ _ _ + (R _ _ (Q _ _ bb.pb3 er.c17 bb.v3) er.c18 bb.v2) (\ er.c19 + (satlem_simplify _ _ _ + (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c17 bb.v2) er.c16 bb.v3) + er.c19 bb.v1) (\ er.c20 + er.c20 ; (holds cln) + )))))))))))) + ))) + ))) + ))) + ) + ))) + ) + )) + ) + )) + ) + )EOF"; + + TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out)); +} diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h index 49d18ac53..48f571841 100644 --- a/test/unit/proof/lrat_proof_black.h +++ b/test/unit/proof/lrat_proof_black.h @@ -16,13 +16,11 @@ #include -#include -#include #include -#include #include "proof/lrat/lrat_proof.h" #include "prop/sat_solver_types.h" +#include "utils.h" using namespace CVC4::proof::lrat; using namespace CVC4::prop; @@ -36,22 +34,6 @@ class LfscProofBlack : public CxxTest::TestSuite void testOutputAsLfsc(); }; -/** - * 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; -} - void LfscProofBlack::testOutputAsLfsc() { std::vector> instructions; diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h new file mode 100644 index 000000000..19b24f4c3 --- /dev/null +++ b/test/unit/proof/utils.h @@ -0,0 +1,34 @@ +/********************* */ +/*! \file utils.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 +#include +#include +#include + +/** + * 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; +} -- 2.30.2