diff options
Diffstat (limited to 'src/proof/lrat/lrat_proof.cpp')
| -rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index d2f347807..79a92fe73 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -127,7 +127,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices) LratProof LratProof::fromDratProof( const std::unordered_map<ClauseId, prop::SatClause>& clauses, const std::vector<ClauseId> usedIds, - const std::string& dratBinary) + const std::string& dratBinary, + TimerStat& toolTimer) { std::ostringstream cmd; std::string formulaFilename("cvc4-dimacs-XXXXXX"); @@ -144,14 +145,17 @@ LratProof LratProof::fromDratProof( std::fstream lratStream = openTmpFile(&lratFilename); + { + CodeTimer blockTimer{toolTimer}; #if CVC4_USE_DRAT2ER - drat2er::drat_trim::CheckAndConvertToLRAT( - formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); + drat2er::drat_trim::CheckAndConvertToLRAT( + formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); #else - Unimplemented( - "LRAT proof production requires drat2er.\n" - "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); + Unimplemented( + "LRAT proof production requires drat2er.\n" + "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); #endif + } LratProof lrat(lratStream); remove(formulaFilename.c_str()); |