Use TMPDIR environment variable for temp files (#2849)

Previously, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.

1 files changed, 10 insertions, 22 deletions

diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 7b966f2c6..9952e6b3e 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -85,32 +85,22 @@ ErProof ErProof::fromBinaryDratProof(
     const std::vector<ClauseId>& usedIds,
     const std::string& dratBinary)
 {
-  std::ostringstream cmd;
-  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
-  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
-  char tracecheckFilename[] = "/tmp/cvc4-tracecheck-er-XXXXXX";
-
-  int r;
-  r = mkstemp(formulaFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(dratFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(tracecheckFilename);
-  AlwaysAssert(r > 0);
-  close(r);
+  std::string formulaFilename("cvc4-dimacs-XXXXXX");
+  std::string dratFilename("cvc4-drat-XXXXXX");
+  std::string tracecheckFilename("cvc4-tracecheck-er-XXXXXX");
 
   // Write the formula
-  std::ofstream formStream(formulaFilename);
+  std::fstream formStream = openTmpFile(&formulaFilename);
   printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   // Write the (binary) DRAT proof
-  std::ofstream dratStream(dratFilename);
+  std::fstream dratStream = openTmpFile(&dratFilename);
   dratStream << dratBinary;
   dratStream.close();
 
+  std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
+
   // Invoke drat2er
 #if CVC4_USE_DRAT2ER
   drat2er::TransformDRATToExtendedResolution(formulaFilename,
@@ -119,7 +109,6 @@ ErProof ErProof::fromBinaryDratProof(
                                              false,
                                              drat2er::options::QUIET,
                                              false);
-
 #else
   Unimplemented(
       "ER proof production requires drat2er.\n"
@@ -127,14 +116,13 @@ ErProof ErProof::fromBinaryDratProof(
 #endif
 
   // Parse the resulting TRACECHECK proof into an ER proof.
-  std::ifstream tracecheckStream(tracecheckFilename);
   TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
   ErProof proof(clauses, usedIds, std::move(pf));
   tracecheckStream.close();
 
-  remove(formulaFilename);
-  remove(dratFilename);
-  remove(tracecheckFilename);
+  remove(formulaFilename.c_str());
+  remove(dratFilename.c_str());
+  remove(tracecheckFilename.c_str());
 
   return proof;
 }