diff options
Diffstat (limited to 'src/proof/lrat/lrat_proof.h')
| -rw-r--r-- | src/proof/lrat/lrat_proof.h | 10 |
1 files changed, 4 insertions, 6 deletions
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 |