diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-06 13:26:43 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-06 14:28:33 -0800 |
commit | 65af88c6392f90d8e18ebe3957226b837e617581 (patch) | |
tree | 87bd094c02186cdbef81c8809aacf4038b59c03a /src/proof/er | |
parent | 6374d4154e6de85879567f5c1150c7d471440834 (diff) |
Use TMPDIR environment variable for temp filesup-fix-fix
Previosuly, 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.
Diffstat (limited to 'src/proof/er')
-rw-r--r-- | src/proof/er/er_proof.cpp | 33 |
1 files changed, 13 insertions, 20 deletions
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 7215312c7..9de48b018 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -34,6 +34,7 @@ #include "proof/dimacs_printer.h" #include "proof/lfsc_proof_printer.h" #include "proof/proof_manager.h" +#include "util/utility.h" #if CVC4_USE_DRAT2ER #include "drat2er.h" @@ -84,29 +85,20 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, 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("/tmp/cvc4-dimacs-XXXXXX"); + std::string dratFilename("/tmp/cvc4-drat-XXXXXX"); + std::string tracecheckFilename("/tmp/cvc4-tracecheck-er-XXXXXX"); // Write the formula - std::ofstream formStream(formulaFilename); + std::fstream formStream; + openTmpFile(&formStream, &formulaFilename); printDimacs(formStream, usedClauses); formStream.close(); // Write the (binary) DRAT proof - std::ofstream dratStream(dratFilename); + std::fstream dratStream; + openTmpFile(&dratStream, &dratFilename); dratStream << dratBinary; dratStream.close(); @@ -126,14 +118,15 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, #endif // Parse the resulting TRACECHECK proof into an ER proof. - std::ifstream tracecheckStream(tracecheckFilename); + std::fstream tracecheckStream; + openTmpFile(&tracecheckStream, &tracecheckFilename); TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream); ErProof proof(usedClauses, std::move(pf)); tracecheckStream.close(); - unlink(formulaFilename); - unlink(dratFilename); - unlink(tracecheckFilename); + remove(formulaFilename.c_str()); + remove(dratFilename.c_str()); + remove(tracecheckFilename.c_str()); return proof; } |