diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-07-22 18:39:12 -0400 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-07-22 15:39:12 -0700 |
commit | 5d203980cb011ce0a9aa5007d4792c1f80dd1e4b (patch) | |
tree | 2730abeaf4430217720d17aa3c5068901815291a /src/proof/clausal_bitvector_proof.cpp | |
parent | ed8f4388c859595178e303f65393105e99d4eb59 (diff) |
Avoid move constructor of std::fstream for GCC < 5 (#3098)
GCC < 5 does not support the move constructor of `std::fstream` (see
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details). This
commit wraps the `std::fstream` in an `std::unique_ptr` to work around
that issue.
Diffstat (limited to 'src/proof/clausal_bitvector_proof.cpp')
-rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 9d6d0d193..4e700a832 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -144,25 +144,26 @@ void ClausalBitVectorProof::optimizeDratProof() std::string optFormulaFilename("cvc4-optimized-formula-XXXXXX"); { - std::fstream formStream = openTmpFile(&formulaFilename); - const int64_t startPos = static_cast<int64_t>(formStream.tellp()); - printDimacs(formStream, d_clauses, d_originalClauseIndices); + std::unique_ptr<std::fstream> formStream = openTmpFile(&formulaFilename); + const int64_t startPos = static_cast<int64_t>(formStream->tellp()); + printDimacs(*formStream, d_clauses, d_originalClauseIndices); d_dratOptimizationStatistics.d_initialFormulaSize.setData( - static_cast<int64_t>(formStream.tellp()) - startPos); - formStream.close(); + static_cast<int64_t>(formStream->tellp()) - startPos); + formStream->close(); } { - std::fstream dratStream = openTmpFile(&dratFilename); - const int64_t startPos = static_cast<int64_t>(dratStream.tellp()); - dratStream << d_binaryDratProof.str(); + std::unique_ptr<std::fstream> dratStream = openTmpFile(&dratFilename); + const int64_t startPos = static_cast<int64_t>(dratStream->tellp()); + (*dratStream) << d_binaryDratProof.str(); d_dratOptimizationStatistics.d_initialDratSize.setData( - static_cast<int64_t>(dratStream.tellp()) - startPos); - dratStream.close(); + static_cast<int64_t>(dratStream->tellp()) - startPos); + dratStream->close(); } - std::fstream optDratStream = openTmpFile(&optDratFilename); - std::fstream optFormulaStream = openTmpFile(&optFormulaFilename); + std::unique_ptr<std::fstream> optDratStream = openTmpFile(&optDratFilename); + std::unique_ptr<std::fstream> optFormulaStream = + openTmpFile(&optFormulaFilename); #if CVC4_USE_DRAT2ER { @@ -204,7 +205,6 @@ void ClausalBitVectorProof::optimizeDratProof() std::vector<prop::SatClause> core = parseDimacs(optFormulaStream); d_dratOptimizationStatistics.d_optimizedFormulaSize.setData( static_cast<int64_t>(optFormulaStream.tellg()) - startPos); - optFormulaStream.close(); CodeTimer clauseMatchingTimer{ d_dratOptimizationStatistics.d_clauseMatchingTime}; @@ -241,7 +241,7 @@ void ClausalBitVectorProof::optimizeDratProof() d_coreClauseIndices = d_originalClauseIndices; } - optFormulaStream.close(); + optFormulaStream->close(); Assert(d_coreClauseIndices.size() > 0); remove(formulaFilename.c_str()); |