From 491a7c8d1889dfb848de31d5581d0c784167eaec Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 4 Jan 2019 09:57:27 +0100 Subject: [PATCH] [LRAT] A C++ data structure for LRAT. (#2737) * [LRAT] A C++ data structure for LRAT. Added a data structure for storing (abstract) LRAT proofs. The constructor will take a drat binary proof and convert it to LRAT using drat-trim. However, this is unimplemented in this PR. Subsequent PRs will add: * LFSC representation of LRAT * Bitvector Proofs based on LRAT * Enabled tests for those proofs * Documenting LRAT constructors * Apply suggestions from code review Co-Authored-By: alex-ozdemir * Responding to Andres' review Consisting of * Naming nits * Closed fds * Better implementation of disjoint union for LratInstruction * DRAT -> LRAT conversion is no longer an LratProof constructor * include reorder * Update src/proof/lrat/lrat_proof.h Co-Authored-By: alex-ozdemir * Addressed Andres' comments * ANonymous namespaces and name resolution? * Remove inlines, fix i negation Thanks Andres! * Use `std::abs` Credit to Andres Co-Authored-By: alex-ozdemir * Remove uneeded public --- src/CMakeLists.txt | 2 + src/proof/lrat/lrat_proof.cpp | 345 ++++++++++++++++++++++++++++++++++ src/proof/lrat/lrat_proof.h | 162 ++++++++++++++++ 3 files changed, 509 insertions(+) create mode 100644 src/proof/lrat/lrat_proof.cpp create mode 100644 src/proof/lrat/lrat_proof.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 889260045..a0d191f15 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -137,6 +137,8 @@ libcvc4_add_sources( proof/lemma_proof.h proof/lfsc_proof_printer.cpp proof/lfsc_proof_printer.h + proof/lrat/lrat_proof.cpp + proof/lrat/lrat_proof.h proof/proof.h proof/proof_manager.cpp proof/proof_manager.h diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp new file mode 100644 index 000000000..ea03a9e20 --- /dev/null +++ b/src/proof/lrat/lrat_proof.cpp @@ -0,0 +1,345 @@ +/********************* */ +/*! \file lrat_proof.cpp + ** \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 DRAT Proof Format + ** + ** Defines deserialization for DRAT proofs. + **/ + +#include "proof/lrat/lrat_proof.h" + +#include +#include +#include +#include +#include + +#include "base/cvc4_assert.h" +#include "base/output.h" + +namespace CVC4 { +namespace proof { +namespace lrat { + +using prop::SatClause; +using prop::SatLiteral; +using prop::SatVariable; + +namespace { +// Prints the literal as a (+) or (-) int +// Not operator<< b/c that represents negation as ~ +std::ostream& textOut(std::ostream& o, const SatLiteral& l) +{ + if (l.isNegated()) + { + o << "-"; + } + return o << l.getSatVariable(); +} + +// Prints the clause as a space-separated list of ints +// Not operator<< b/c that represents negation as ~ +std::ostream& textOut(std::ostream& o, const SatClause& c) +{ + for (const auto l : c) + { + textOut(o, l) << " "; + } + return o << "0"; +} + +// Prints the trace as a space-separated list of (+) ints with a space at the +// end. +std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace) +{ + for (const auto& i : trace) + { + o << i << " "; + } + return o; +} + +// Prints the LRAT addition line in textual format +std::ostream& operator<<(std::ostream& o, const LratAdditionData& add) +{ + o << add.d_idxOfClause << " "; + textOut(o, add.d_clause) << " "; + o << add.d_atTrace; // Inludes a space at the end. + for (const auto& rat : add.d_resolvants) + { + o << "-" << rat.first << " "; + o << rat.second; // Includes a space at the end. + } + o << "0\n"; + return o; +} + +// Prints the LRAT addition line in textual format +std::ostream& operator<<(std::ostream& o, const LratDeletionData& del) +{ + o << del.d_idxOfClause << " d "; + for (const auto& idx : del.d_clauses) + { + o << idx << " "; + } + return o << "0\n"; +} + +// Prints the LRAT line in textual format +std::ostream& operator<<(std::ostream& o, const LratInstruction& i) +{ + switch (i.d_kind) + { + case LRAT_ADDITION: return o << i.d_data.d_addition; + case LRAT_DELETION: return o << i.d_data.d_deletion; + default: return o; + } +} + +} + +LratInstruction::LratInstruction(LratInstruction&& instr) : d_kind(instr.d_kind) +{ + switch (d_kind) + { + case LRAT_ADDITION: + { + d_data.d_addition = instr.d_data.d_addition; + break; + } + case LRAT_DELETION: + { + d_data.d_deletion = instr.d_data.d_deletion; + break; + } + } +} + +LratInstruction::LratInstruction(LratInstruction& instr) : d_kind(instr.d_kind) +{ + switch (d_kind) + { + case LRAT_ADDITION: + { + d_data.d_addition = instr.d_data.d_addition; + break; + } + case LRAT_DELETION: + { + d_data.d_deletion = instr.d_data.d_deletion; + break; + } + } +} + +LratInstruction::LratInstruction(LratAdditionData&& addition) + : d_kind(LRAT_ADDITION) +{ + d_data.d_addition = std::move(addition); +} + +LratInstruction::LratInstruction(LratDeletionData&& deletion) + : d_kind(LRAT_DELETION) +{ + d_data.d_deletion = std::move(deletion); +} + +LratInstruction::~LratInstruction() +{ + switch (d_kind) + { + case LRAT_ADDITION: + { + d_data.d_addition.~LratAdditionData(); + break; + } + case LRAT_DELETION: + { + d_data.d_deletion.~LratDeletionData(); + break; + } + } +} + +LratProof LratProof::fromDratProof( + const std::unordered_map& usedClauses, + const std::vector& clauseOrder, + const std::string& dratBinary) +{ + std::ostringstream cmd; + char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX"; + char dratFilename[] = "/tmp/cvc4-drat-XXXXXX"; + char lratFilename[] = "/tmp/cvc4-lrat-XXXXXX"; + int r; + r = mkstemp(formulaFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(dratFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(lratFilename); + AlwaysAssert(r > 0); + close(r); + std::ofstream formStream(formulaFilename); + size_t maxVar = 0; + for (auto& c : usedClauses) + { + for (auto l : *(c.second)) + { + if (l.getSatVariable() + 1 > maxVar) + { + maxVar = l.getSatVariable() + 1; + } + } + } + formStream << "p cnf " << maxVar << " " << usedClauses.size() << '\n'; + for (auto ci : clauseOrder) + { + auto iterator = usedClauses.find(ci); + Assert(iterator != usedClauses.end()); + for (auto l : *(iterator->second)) + { + if (l.isNegated()) + { + formStream << '-'; + } + formStream << l.getSatVariable() + 1 << " "; + } + formStream << "0\n"; + } + formStream.close(); + + std::ofstream dratStream(dratFilename); + dratStream << dratBinary; + dratStream.close(); + + // TODO(aozdemir) Add invocation of DRAT trim, once I get CMake to bundle it + // into CVC4 correctly. + Unimplemented(); + + std::ifstream lratStream(lratFilename); + LratProof lrat(lratStream); + remove(formulaFilename); + remove(dratFilename); + remove(lratFilename); + return lrat; +} + +std::istream& operator>>(std::istream& in, SatLiteral& l) +{ + int64_t i; + in >> i; + l = SatLiteral(std::abs(i), i < 0); + return in; +} + +// This parser is implemented to parse the textual RAT format found in +// "Efficient Certified RAT Verification", by Cruz-Filipe et. All +LratProof::LratProof(std::istream& textualProof) +{ + for (size_t line = 0;; ++line) + { + // Read beginning of instruction. EOF indicates that we're done. + size_t clauseIdx; + textualProof >> clauseIdx; + if (textualProof.eof()) + { + return; + } + + // Read the first word of the instruction. A 'd' indicates deletion. + std::string first; + textualProof >> first; + Trace("pf::lrat") << "First word: " << first << std::endl; + Assert(textualProof.good()); + if (first == "d") + { + std::vector clauses; + while (true) + { + ClauseIdx di; + textualProof >> di; + Assert(textualProof.good()); + if (di == 0) + { + break; + } + clauses.push_back(di); + } + std::sort(clauses.begin(), clauses.end()); + d_instructions.emplace_back( + LratDeletionData(clauseIdx, std::move(clauses))); + } + else + { + // We need to reparse the first word as a literal to read the clause + // we're parsing. It ends with a 0; + std::istringstream firstS(first); + SatLiteral lit; + firstS >> lit; + Trace("pf::lrat") << "First lit: " << lit << std::endl; + Assert(!firstS.fail(), "Couldn't parse first literal from addition line"); + + SatClause clause; + for (; lit != 0; textualProof >> lit) + { + Assert(textualProof.good()); + clause.emplace_back(lit.getSatVariable() - 1, lit.isNegated()); + } + + // Now we read the AT UP trace. It ends at the first non-(+) # + std::vector atTrace; + int64_t i; + textualProof >> i; + for (; i > 0; textualProof >> i) + { + Assert(textualProof.good()); + atTrace.push_back(i); + } + + // For each RAT hint... (each RAT hint starts with a (-)). + std::vector> resolvants; + for (; i<0; textualProof>> i) + { + Assert(textualProof.good()); + // Create an entry in the RAT hint list + resolvants.emplace_back(-i, std::vector()); + + // Record the UP trace. It ends with a (-) or 0. + textualProof >> i; + for (; i > 0; textualProof >> i) + { + resolvants.back().second.push_back(i); + } + } + // Pairs compare based on the first element, so this sorts by the + // resolution target index + std::sort(resolvants.begin(), resolvants.end()); + d_instructions.emplace_back(LratAdditionData(clauseIdx, + std::move(clause), + std::move(atTrace), + std::move(resolvants))); + } + } +} + +std::ostream& operator<<(std::ostream& o, const LratProof& p) +{ + for (const auto& instr : p.getInstructions()) + { + o << instr; + } + return o; +} + +} // namespace lrat +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h new file mode 100644 index 000000000..384fbbdf4 --- /dev/null +++ b/src/proof/lrat/lrat_proof.h @@ -0,0 +1,162 @@ +/********************* */ +/*! \file lrat_proof.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 LRAT Proof Format + ** + ** Declares C++ types that represent a LRAT proof. + ** Defines serialization for these types. + ** + ** Represents an **abstract** LRAT proof. + ** Does **not** represent an LFSC LRAT proof, or an LRAT proof being used to + ** prove things about bit-vectors. + ** + ** Paper on LRAT: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H +#define __CVC4__PROOF__LRAT__LRAT_PROOF_H + +#include +#include +#include + +#include "proof/clause_id.h" +// Included because we need operator<< for the SAT types +#include "prop/sat_solver.h" + +namespace CVC4 { +namespace proof { +namespace lrat { + +// Refers to clause position within an LRAT proof +using ClauseIdx = size_t; + +enum LratInstructionKind +{ + LRAT_DELETION, + LRAT_ADDITION, +}; + +struct LratDeletionData +{ + LratDeletionData(ClauseIdx idxOfClause, std::vector&& clauses) + : d_idxOfClause(idxOfClause), d_clauses(clauses) + { + // Nothing left to do + } + + ~LratDeletionData() = default; + + // This idx doesn't really matter, but it's in the format anyway, so we parse + // it. + ClauseIdx d_idxOfClause; + + // Clauses to delete + std::vector d_clauses; +}; + +// A sequence of locations that will contain unit clauses during unit +// propegation +using LratUPTrace = std::vector; + +struct LratAdditionData +{ + LratAdditionData(ClauseIdx idxOfClause, + prop::SatClause&& clause, + LratUPTrace&& atTrace, + std::vector> resolvants) + : d_idxOfClause(idxOfClause), + d_clause(clause), + d_atTrace(atTrace), + d_resolvants(resolvants) + { + // Nothing left to do + } + + ~LratAdditionData() = default; + + // The idx for the new clause + ClauseIdx d_idxOfClause; + // The new clause + prop::SatClause d_clause; + // UP trace based on the negation of that clause + LratUPTrace d_atTrace; + + // Clauses that can resolve with `clause` on its first variable, + // together with a UP trace after that resolution. + // Used for RAT checks. + std::vector> d_resolvants; +}; + +// This is conceptually an Either +struct LratInstruction +{ + LratInstructionKind d_kind; + union LratInstructionData + { + LratAdditionData d_addition; + LratDeletionData d_deletion; + ~LratInstructionData(){/* Empty destructor */}; + LratInstructionData(){/* Empty constructor */}; + } d_data; + + LratInstruction(LratInstruction&& instr); + LratInstruction(LratInstruction& instr); + LratInstruction(LratAdditionData&& addition); + LratInstruction(LratDeletionData&& deletion); + ~LratInstruction(); +}; + +class LratProof +{ + public: + /** + * @brief Construct an LRAT proof from a DRAT proof, using drat-trim + * + * @param usedClauses The CNF formula that we're deriving bottom from. + * It's a map because other parts of the system represent + * it this way. + * @param clauseOrder A record of the order in which those clauses were + * given to the SAT solver. + * @param dratBinary The DRAT proof from the SAT solver, as a binary stream. + */ + static LratProof fromDratProof( + const std::unordered_map& usedClauses, + const std::vector& clauseOrder, + const std::string& dratBinary); + /** + * @brief Construct an LRAT proof from its textual representation + * + * @param textualProof the textual encoding of the LRAT proof. See the paper + * in the file's header comment. + */ + LratProof(std::istream& textualProof); + + const std::vector& getInstructions() const + { + return d_instructions; + } + + private: + // The instructions in the proof. Each is a deletion or addition. + std::vector d_instructions; +}; + +// Prints the LRAT proof in textual format +std::ostream& operator<<(std::ostream& o, const LratProof& p); + +} // namespace lrat +} // namespace proof +} // namespace CVC4 + +#endif -- 2.30.2