diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 183 | ||||
| -rw-r--r-- | src/proof/clausal_bitvector_proof.h | 11 | ||||
| -rw-r--r-- | src/proof/dimacs.cpp (renamed from src/proof/dimacs_printer.cpp) | 63 | ||||
| -rw-r--r-- | src/proof/dimacs.h (renamed from src/proof/dimacs_printer.h) | 19 | ||||
| -rw-r--r-- | src/proof/er/er_proof.cpp | 39 | ||||
| -rw-r--r-- | src/proof/er/er_proof.h | 21 | ||||
| -rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 19 | ||||
| -rw-r--r-- | src/proof/lrat/lrat_proof.h | 10 |
8 files changed, 271 insertions, 94 deletions
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index eed295b1a..07589fd07 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -17,24 +17,35 @@ #include "cvc4_private.h" #include <algorithm> +#include <iostream> #include <iterator> -#include <set> +#include <unordered_set> #include "options/bv_options.h" #include "proof/clausal_bitvector_proof.h" +#include "proof/dimacs.h" #include "proof/drat/drat_proof.h" #include "proof/er/er_proof.h" #include "proof/lfsc_proof_printer.h" #include "proof/lrat/lrat_proof.h" #include "theory/bv/theory_bv.h" +#if CVC4_USE_DRAT2ER +#include "drat2er_options.h" +#include "drat_trim_interface.h" +#endif + namespace CVC4 { namespace proof { ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof() + : BitVectorProof(bv, proofEngine), + d_clauses(), + d_originalClauseIndices(), + d_binaryDratProof(), + d_coreClauseIndices() { } @@ -69,33 +80,151 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, void ClausalBitVectorProof::registerUsedClause(ClauseId id, prop::SatClause& clause) { - d_usedClauses.emplace_back(id, clause); + d_clauses.emplace(id, clause); + d_originalClauseIndices.push_back(id); }; void ClausalBitVectorProof::calculateAtomsInBitblastingProof() { + optimizeDratProof(); + // Debug dump of DRAT Proof if (Debug.isOn("bv::clausal")) { std::string serializedDratProof = d_binaryDratProof.str(); + Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof() + << std::endl; Debug("bv::clausal") << "binary DRAT proof byte count: " << serializedDratProof.size() << std::endl; - Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl; - drat::DratProof dratProof = - drat::DratProof::fromBinary(serializedDratProof); - - Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl; - dratProof.outputAsText(Debug("bv::clausal")); + Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size() + << std::endl; } // Empty any old record of which atoms were used d_atomsInBitblastingProof.clear(); + Assert(d_atomsInBitblastingProof.size() == 0); // For each used clause, ask the CNF proof which atoms are used in it - for (const auto& usedIndexAndClause : d_usedClauses) + for (const ClauseId usedIdx : d_coreClauseIndices) { - d_cnfProof->collectAtoms(&usedIndexAndClause.second, - d_atomsInBitblastingProof); + d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof); + } +} + +void ClausalBitVectorProof::optimizeDratProof() +{ + if (options::bvOptimizeSatProof() + == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF + || options::bvOptimizeSatProof() + == theory::bv::BvOptimizeSatProof:: + BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA) + { + Debug("bv::clausal") << "Optimizing DRAT" << std::endl; + char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX"; + char dratFilename[] = "/tmp/cvc4-drat-XXXXXX"; + char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX"; + char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX"; + int r; + r = mkstemp(formulaFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(dratFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(optDratFilename); + AlwaysAssert(r > 0); + close(r); + r = mkstemp(optFormulaFilename); + AlwaysAssert(r > 0); + close(r); + + std::ofstream formStream(formulaFilename); + printDimacs(formStream, d_clauses, d_originalClauseIndices); + formStream.close(); + + std::ofstream dratStream(dratFilename); + dratStream << d_binaryDratProof.str(); + dratStream.close(); + +#if CVC4_USE_DRAT2ER + int dratTrimExitCode = + drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename, + dratFilename, + optFormulaFilename, + optDratFilename, + drat2er::options::QUIET); + AlwaysAssert( + dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode); +#else + Unimplemented( + "Proof production when using CryptoMiniSat requires drat2er.\n" + "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); +#endif + + d_binaryDratProof.str(""); + Assert(d_binaryDratProof.str().size() == 0); + + std::ifstream lratStream(optDratFilename); + std::copy(std::istreambuf_iterator<char>(lratStream), + std::istreambuf_iterator<char>(), + std::ostreambuf_iterator<char>(d_binaryDratProof)); + + if (options::bvOptimizeSatProof() + == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA) + { + std::ifstream optFormulaStream{optFormulaFilename}; + std::vector<prop::SatClause> core = parseDimacs(optFormulaStream); + optFormulaStream.close(); + + // Now we need to compute the clause indices for the UNSAT core. This is a + // bit difficult because drat-trim may have reordered clauses, and/or + // removed duplicate literals. We use literal sets as the canonical clause + // form. + std::unordered_map< + std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>, + ClauseId, + prop::SatClauseSetHashFunction> + cannonicalClausesToIndices; + for (const auto& kv : d_clauses) + { + cannonicalClausesToIndices.emplace( + std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{ + kv.second.begin(), kv.second.end()}, + kv.first); + } + + d_coreClauseIndices.clear(); + std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction> + coreClauseCanonical; + for (const prop::SatClause& coreClause : core) + { + coreClauseCanonical.insert(coreClause.begin(), coreClause.end()); + d_coreClauseIndices.push_back( + cannonicalClausesToIndices.at(coreClauseCanonical)); + coreClauseCanonical.clear(); + } + Debug("bv::clausal") << "Optimizing the DRAT proof and the formula" + << std::endl; + } + else + { + Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula" + << std::endl; + d_coreClauseIndices = d_originalClauseIndices; + } + + Assert(d_coreClauseIndices.size() > 0); + remove(formulaFilename); + remove(dratFilename); + remove(optDratFilename); + remove(optFormulaFilename); + Debug("bv::clausal") << "Optimized DRAT" << std::endl; + } + else + { + Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof" + << std::endl; + d_coreClauseIndices = d_originalClauseIndices; } } @@ -120,10 +249,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); os << "\n;; BB-CNF proofs\n"; - for (const auto& idAndClause : d_usedClauses) + for (const ClauseId id : d_coreClauseIndices) { - d_cnfProof->printCnfProofForClause( - idAndClause.first, &idAndClause.second, os, paren); + d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren); } } @@ -137,13 +265,8 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, os << "\n;; Proof of input to SAT solver\n"; os << "(@ proofOfSatInput "; paren << ")"; - std::vector<ClauseId> usedIds; - usedIds.reserve(d_usedClauses.size()); - for (const auto& idAnd : d_usedClauses) - { - usedIds.push_back(idAnd.first); - }; - LFSCProofPrinter::printSatInputProof(usedIds, os, "bb"); + + LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb"); os << "\n;; DRAT Proof Value\n"; os << "(@ dratProof "; @@ -166,19 +289,13 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os, os << "\n;; Proof of input to SAT solver\n"; os << "(@ proofOfCMap "; paren << ")"; - std::vector<ClauseId> usedIds; - usedIds.reserve(d_usedClauses.size()); - for (const auto& idAnd : d_usedClauses) - { - usedIds.push_back(idAnd.first); - }; - LFSCProofPrinter::printCMapProof(usedIds, os, "bb"); + LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb"); os << "\n;; DRAT Proof Value\n"; os << "(@ lratProof "; paren << ")"; - lrat::LratProof pf = - lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str()); + lrat::LratProof pf = lrat::LratProof::fromDratProof( + d_clauses, d_coreClauseIndices, d_binaryDratProof.str()); pf.outputAsLfsc(os); os << "\n"; @@ -194,8 +311,8 @@ void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os, "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"); - er::ErProof pf = - er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str()); + er::ErProof pf = er::ErProof::fromBinaryDratProof( + d_clauses, d_coreClauseIndices, d_binaryDratProof.str()); pf.outputAsLfsc(os); } diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h index b10b1ad1c..a410b5b38 100644 --- a/src/proof/clausal_bitvector_proof.h +++ b/src/proof/clausal_bitvector_proof.h @@ -61,9 +61,16 @@ class ClausalBitVectorProof : public BitVectorProof protected: // A list of all clauses and their ids which are passed into the SAT solver - std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses; + std::unordered_map<ClauseId, prop::SatClause> d_clauses{}; + std::vector<ClauseId> d_originalClauseIndices{}; // Stores the proof recieved from the SAT solver. - std::ostringstream d_binaryDratProof; + std::ostringstream d_binaryDratProof{}; + std::vector<ClauseId> d_coreClauseIndices{}; + + private: + // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list + // of clause actually needed to check that proof (a smaller UNSAT core) + void optimizeDratProof(); }; /** diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs.cpp index 04f880e11..cced98660 100644 --- a/src/proof/dimacs_printer.cpp +++ b/src/proof/dimacs.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file dimacs_printer.cpp +/*! \file dimacs.cpp ** \verbatim ** Top contributors (to current version): ** Alex Ozdemir @@ -14,7 +14,9 @@ ** Defines serialization for SAT problems as DIMACS **/ -#include "proof/dimacs_printer.h" +#include "proof/dimacs.h" + +#include "base/cvc4_assert.h" #include <iostream> @@ -43,14 +45,15 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c) return o << "0"; } -void printDimacs( - std::ostream& o, - const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses) +void printDimacs(std::ostream& o, + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIndices) { size_t maxVar = 0; - for (const auto& c : usedClauses) + for (const ClauseId i : usedIndices) { - for (const auto& l : c.second) + const prop::SatClause& c = clauses.at(i); + for (const auto& l : c) { if (l.getSatVariable() + 1 > maxVar) { @@ -58,10 +61,11 @@ void printDimacs( } } } - o << "p cnf " << maxVar << " " << usedClauses.size() << '\n'; - for (const auto& idAndClause : usedClauses) + o << "p cnf " << maxVar << " " << usedIndices.size() << '\n'; + for (const ClauseId i : usedIndices) { - for (const auto& l : idAndClause.second) + const prop::SatClause& c = clauses.at(i); + for (const auto& l : c) { if (l.isNegated()) { @@ -73,5 +77,44 @@ void printDimacs( } } +std::vector<prop::SatClause> parseDimacs(std::istream& in) +{ + std::string tag; + uint64_t nVars; + uint64_t nClauses; + + in >> tag; + Assert(in.good()); + Assert(tag == "p"); + + in >> tag; + Assert(in.good()); + Assert(tag == "cnf"); + + in >> nVars; + Assert(nVars >= 0); + + in >> nClauses; + Assert(nClauses >= 0); + + std::vector<prop::SatClause> cnf; + for (uint64_t i = 0; i < nClauses; ++i) + { + cnf.emplace_back(); + int64_t lit; + in >> lit; + Assert(in.good()); + while (lit != 0) + { + cnf.back().emplace_back(std::abs(lit) - 1, lit < 0); + in >> lit; + Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars); + Assert(in.good()); + } + } + + return cnf; +} + } // namespace proof } // namespace CVC4 diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs.h index 2ae4abefa..5956c5d26 100644 --- a/src/proof/dimacs_printer.h +++ b/src/proof/dimacs.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file dimacs_printer.h +/*! \file dimacs.h ** \verbatim ** Top contributors (to current version): ** Alex Ozdemir @@ -11,16 +11,17 @@ ** ** \brief DIMACS SAT Problem Format ** - ** Defines serialization for SAT problems as DIMACS + ** Defines serialization/deserialization for SAT problems as DIMACS **/ #include "cvc4_private.h" -#ifndef CVC4__PROOF__DIMACS_PRINTER_H -#define CVC4__PROOF__DIMACS_PRINTER_H +#ifndef CVC4__PROOF__DIMACS_H +#define CVC4__PROOF__DIMACS_H #include <iosfwd> #include <memory> +#include <unordered_map> #include "proof/clause_id.h" #include "prop/sat_solver_types.h" @@ -56,11 +57,13 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c); * @param o where to print to * @param usedClauses the CNF formula */ -void printDimacs( - std::ostream& o, - const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses); +void printDimacs(std::ostream& o, + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIndices); + +std::vector<prop::SatClause> parseDimacs(std::istream& i); } // namespace proof } // namespace CVC4 -#endif // CVC4__PROOF__DIMACS_PRINTER_H +#endif // CVC4__PROOF__DIMACS_H diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 22903c3c9..9160546f9 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -31,7 +31,7 @@ #include "base/cvc4_assert.h" #include "base/map_util.h" -#include "proof/dimacs_printer.h" +#include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" #include "proof/proof_manager.h" @@ -80,8 +80,10 @@ TraceCheckProof TraceCheckProof::fromText(std::istream& in) return pf; } -ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, - const std::string& dratBinary) +ErProof ErProof::fromBinaryDratProof( + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIds, + const std::string& dratBinary) { std::ostringstream cmd; char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX"; @@ -101,7 +103,7 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, // Write the formula std::ofstream formStream(formulaFilename); - printDimacs(formStream, usedClauses); + printDimacs(formStream, clauses, usedIds); formStream.close(); // Write the (binary) DRAT proof @@ -126,7 +128,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, // Parse the resulting TRACECHECK proof into an ER proof. std::ifstream tracecheckStream(tracecheckFilename); - ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream)); + TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream); + ErProof proof(clauses, usedIds, std::move(pf)); tracecheckStream.close(); remove(formulaFilename); @@ -136,17 +139,21 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, return proof; } -ErProof::ErProof(const ClauseUseRecord& usedClauses, +ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIds, 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<ClauseId, prop::SatClause>& pair) { - return pair.first; - }); + d_inputClauseIds = usedIds; + + // Make a list of (idx, clause pairs), the used ones. + std::vector<std::pair<ClauseId, prop::SatClause>> usedClauses; + std::transform( + usedIds.begin(), + usedIds.end(), + std::back_inserter(usedClauses), + [&](const ClauseId& i) { return make_pair(i, clauses.at(i)); }); // Step one, verify the formula starts the proof if (Configuration::isAssertionBuild()) @@ -162,14 +169,6 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses, originalClause{usedClauses[i].second.begin(), usedClauses[i].second.end()}; Assert(traceCheckClause == originalClause); - 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]); - } } } diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h index f5af0783b..d6cbd9213 100644 --- a/src/proof/er/er_proof.h +++ b/src/proof/er/er_proof.h @@ -27,6 +27,7 @@ #define CVC4__PROOF__ER__ER_PROOF_H #include <memory> +#include <unordered_map> #include <vector> #include "proof/clause_id.h" @@ -36,8 +37,6 @@ namespace CVC4 { namespace proof { namespace er { -using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>; - /** * A definition of the form: * newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n) @@ -116,11 +115,14 @@ class ErProof /** * 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. + * @param clauses A store of clauses that might be in our formula + * @param usedIds the ids of clauses that are actually in our formula + * @param dratBinary The DRAT proof from the SAT solver, as a binary stream */ - static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses, - const std::string& dratBinary); + static ErProof fromBinaryDratProof( + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIds, + const std::string& dratBinary); /** * Construct an ER proof from a TRACECHECK ER proof @@ -128,10 +130,13 @@ class ErProof * 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 clauses A store of clauses that might be in our formula + * @param usedIds the ids of clauses that are actually in our formula * @param tracecheck The TRACECHECK proof, as a stream. */ - ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck); + ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId>& usedIds, + TraceCheckProof&& tracecheck); /** * Write the ER proof as an LFSC value of type (holds cln). diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index a1939ec92..e414c64c9 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -26,7 +26,7 @@ #include "base/cvc4_assert.h" #include "base/output.h" -#include "proof/dimacs_printer.h" +#include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" #if CVC4_USE_DRAT2ER @@ -104,6 +104,7 @@ void printHints(std::ostream& o, */ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices) { + Assert(indices.size() > 0); // Verify that the indices are sorted! for (size_t i = 0, n = indices.size() - 1; i < n; ++i) { @@ -123,7 +124,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices) // Prints the LRAT addition line in textual format LratProof LratProof::fromDratProof( - const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses, + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId> usedIds, const std::string& dratBinary) { std::ostringstream cmd; @@ -141,7 +143,7 @@ LratProof LratProof::fromDratProof( AlwaysAssert(r > 0); close(r); std::ofstream formStream(formulaFilename); - printDimacs(formStream, usedClauses); + printDimacs(formStream, clauses, usedIds); formStream.close(); std::ofstream dratStream(dratFilename); @@ -206,10 +208,13 @@ LratProof::LratProof(std::istream& textualProof) } clauses.push_back(di); } - std::sort(clauses.begin(), clauses.end()); - std::unique_ptr<LratInstruction> instr( - new LratDeletion(clauseIdx, std::move(clauses))); - d_instructions.push_back(std::move(instr)); + if (clauses.size() > 0) + { + std::sort(clauses.begin(), clauses.end()); + std::unique_ptr<LratInstruction> instr( + new LratDeletion(clauseIdx, std::move(clauses))); + d_instructions.push_back(std::move(instr)); + } } else { diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h index 33b2fad3f..54db1837d 100644 --- a/src/proof/lrat/lrat_proof.h +++ b/src/proof/lrat/lrat_proof.h @@ -129,15 +129,13 @@ class LratProof /** * @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 clauses A store of clauses that might be in our formula + * @param usedIds the ids of clauses that are actually in our formula * @param dratBinary The DRAT proof from the SAT solver, as a binary stream. */ static LratProof fromDratProof( - const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses, + const std::unordered_map<ClauseId, prop::SatClause>& clauses, + const std::vector<ClauseId> usedIds, const std::string& dratBinary); /** * @brief Construct an LRAT proof from its textual representation |