diff options
Diffstat (limited to 'src/proof/er/er_proof.h')
-rw-r--r-- | src/proof/er/er_proof.h | 21 |
1 files changed, 13 insertions, 8 deletions
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). |