From: Andres Noetzli Date: Mon, 22 Jul 2019 22:39:12 +0000 (-0400) Subject: Avoid move constructor of std::fstream for GCC < 5 (#3098) X-Git-Tag: cvc5-1.0.0~4084 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d203980cb011ce0a9aa5007d4792c1f80dd1e4b;p=cvc5.git 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. --- 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(formStream.tellp()); - printDimacs(formStream, d_clauses, d_originalClauseIndices); + std::unique_ptr formStream = openTmpFile(&formulaFilename); + const int64_t startPos = static_cast(formStream->tellp()); + printDimacs(*formStream, d_clauses, d_originalClauseIndices); d_dratOptimizationStatistics.d_initialFormulaSize.setData( - static_cast(formStream.tellp()) - startPos); - formStream.close(); + static_cast(formStream->tellp()) - startPos); + formStream->close(); } { - std::fstream dratStream = openTmpFile(&dratFilename); - const int64_t startPos = static_cast(dratStream.tellp()); - dratStream << d_binaryDratProof.str(); + std::unique_ptr dratStream = openTmpFile(&dratFilename); + const int64_t startPos = static_cast(dratStream->tellp()); + (*dratStream) << d_binaryDratProof.str(); d_dratOptimizationStatistics.d_initialDratSize.setData( - static_cast(dratStream.tellp()) - startPos); - dratStream.close(); + static_cast(dratStream->tellp()) - startPos); + dratStream->close(); } - std::fstream optDratStream = openTmpFile(&optDratFilename); - std::fstream optFormulaStream = openTmpFile(&optFormulaFilename); + std::unique_ptr optDratStream = openTmpFile(&optDratFilename); + std::unique_ptr optFormulaStream = + openTmpFile(&optFormulaFilename); #if CVC4_USE_DRAT2ER { @@ -204,7 +205,6 @@ void ClausalBitVectorProof::optimizeDratProof() std::vector core = parseDimacs(optFormulaStream); d_dratOptimizationStatistics.d_optimizedFormulaSize.setData( static_cast(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()); diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index ab07875b2..9f22e236b 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -91,16 +91,17 @@ ErProof ErProof::fromBinaryDratProof( std::string tracecheckFilename("cvc4-tracecheck-er-XXXXXX"); // Write the formula - std::fstream formStream = openTmpFile(&formulaFilename); - printDimacs(formStream, clauses, usedIds); - formStream.close(); + std::unique_ptr formStream = openTmpFile(&formulaFilename); + printDimacs(*formStream, clauses, usedIds); + formStream->close(); // Write the (binary) DRAT proof - std::fstream dratStream = openTmpFile(&dratFilename); - dratStream << dratBinary; - dratStream.close(); + std::unique_ptr dratStream = openTmpFile(&dratFilename); + (*dratStream) << dratBinary; + dratStream->close(); - std::fstream tracecheckStream = openTmpFile(&tracecheckFilename); + std::unique_ptr tracecheckStream = + openTmpFile(&tracecheckFilename); // Invoke drat2er { @@ -120,9 +121,9 @@ ErProof ErProof::fromBinaryDratProof( } // Parse the resulting TRACECHECK proof into an ER proof. - TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream); + TraceCheckProof pf = TraceCheckProof::fromText(*tracecheckStream); ErProof proof(clauses, usedIds, std::move(pf)); - tracecheckStream.close(); + tracecheckStream->close(); remove(formulaFilename.c_str()); remove(dratFilename.c_str()); diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index 79a92fe73..1685ad1c3 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -135,15 +135,15 @@ LratProof LratProof::fromDratProof( std::string dratFilename("cvc4-drat-XXXXXX"); std::string lratFilename("cvc4-lrat-XXXXXX"); - std::fstream formStream = openTmpFile(&formulaFilename); - printDimacs(formStream, clauses, usedIds); - formStream.close(); + std::unique_ptr formStream = openTmpFile(&formulaFilename); + printDimacs(*formStream, clauses, usedIds); + formStream->close(); - std::fstream dratStream = openTmpFile(&dratFilename); - dratStream << dratBinary; - dratStream.close(); + std::unique_ptr dratStream = openTmpFile(&dratFilename); + (*dratStream) << dratBinary; + dratStream->close(); - std::fstream lratStream = openTmpFile(&lratFilename); + std::unique_ptr lratStream = openTmpFile(&lratFilename); { CodeTimer blockTimer{toolTimer}; @@ -157,7 +157,7 @@ LratProof LratProof::fromDratProof( #endif } - LratProof lrat(lratStream); + LratProof lrat(*lratStream); remove(formulaFilename.c_str()); remove(dratFilename.c_str()); remove(lratFilename.c_str()); diff --git a/src/util/utility.cpp b/src/util/utility.cpp index 9936504d2..97d5ef36b 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -25,7 +25,7 @@ namespace CVC4 { -std::fstream openTmpFile(std::string* pattern) +std::unique_ptr openTmpFile(std::string* pattern) { char* tmpDir = getenv("TMPDIR"); if (tmpDir != nullptr) @@ -46,7 +46,7 @@ std::fstream openTmpFile(std::string* pattern) { CVC4_FATAL() << "Could not create temporary file " << *pattern; } - std::fstream tmpStream(tmpName); + std::unique_ptr tmpStream(new std::fstream(tmpName)); close(r); *pattern = std::string(tmpName); delete[] tmpName; diff --git a/src/util/utility.h b/src/util/utility.h index a606648bd..4477fc7b2 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -22,6 +22,7 @@ #include #include #include +#include #include #include @@ -95,9 +96,13 @@ void container_to_stream(std::ostream& out, * @param pattern The filename pattern. This string is modified to contain the * name of the temporary file. * - * @return A filestream for the temporary file. + * @return A unique pointer to the filestream for the temporary file. + * + * Note: We use `std::unique_ptr` instead of `std::fstream` + * because GCC < 5 does not support the move constructor of `std::fstream`. See + * https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details. */ -std::fstream openTmpFile(std::string* pattern); +std::unique_ptr openTmpFile(std::string* pattern); }/* CVC4 namespace */