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 9d6d0d1934ab0148c09ff56a0bad9b04e68fa0ee..4e700a8325122cfe3f5190fba67aef0efe230234 100644 (file)
--- 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());

diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index ab07875b23d9be5f14c2d6f5a741215997de7f11..9f22e236b93b5d8141826c5853c3ac4dac6bc165 100644 (file)
--- 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<std::fstream> 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<std::fstream> dratStream = openTmpFile(&dratFilename);
+  (*dratStream) << dratBinary;
+  dratStream->close();
 
-  std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
+  std::unique_ptr<std::fstream> 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 79a92fe736ff7c49754c3e717537ffb9d2eeefe1..1685ad1c3067682660e3390e7601b1daa2ee6ca8 100644 (file)
--- 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<std::fstream> formStream = openTmpFile(&formulaFilename);
+  printDimacs(*formStream, clauses, usedIds);
+  formStream->close();
 
-  std::fstream dratStream = openTmpFile(&dratFilename);
-  dratStream << dratBinary;
-  dratStream.close();
+  std::unique_ptr<std::fstream> dratStream = openTmpFile(&dratFilename);
+  (*dratStream) << dratBinary;
+  dratStream->close();
 
-  std::fstream lratStream = openTmpFile(&lratFilename);
+  std::unique_ptr<std::fstream> 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 9936504d2f2cad08ed047a872e129f3f8b769194..97d5ef36b5c1e5a0a103b4071d6d555dd68cdcf7 100644 (file)
--- 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<std::fstream> 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<std::fstream> 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 a606648bdab873cc33d059369c2eef7da99bf62b..4477fc7b2439133e46f40552c679f66747f5aff6 100644 (file)
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -22,6 +22,7 @@
 #include <algorithm>
 #include <fstream>
 #include <functional>
+#include <memory>
 #include <string>
 #include <utility>
 
@@ -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<std::fstream>` 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<std::fstream> openTmpFile(std::string* pattern);
 
 }/* CVC4 namespace */