diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 10:55:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-21 10:55:03 -0700 |
commit | cf9dfb9be23b4f802989fecd18756ed62aecc8e4 (patch) | |
tree | 3f1f45759bf85b451b458aab98cf62892f7aef17 /src/proof/lrat | |
parent | 073335156ff7644364d12a91d4d41af776cfb91b (diff) |
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.
Diffstat (limited to 'src/proof/lrat')
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 31 |
1 files changed, 12 insertions, 19 deletions
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index e414c64c9..d2f347807 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -28,6 +28,7 @@ #include "base/output.h" #include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" +#include "util/utility.h" #if CVC4_USE_DRAT2ER #include "drat2er_options.h" @@ -129,27 +130,20 @@ LratProof LratProof::fromDratProof( const std::string& dratBinary) { std::ostringstream cmd; - char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX"; - char dratFilename[] = "/tmp/cvc4-drat-XXXXXX"; - char lratFilename[] = "/tmp/cvc4-lrat-XXXXXX"; - int r; - r = mkstemp(formulaFilename); - AlwaysAssert(r > 0); - close(r); - r = mkstemp(dratFilename); - AlwaysAssert(r > 0); - close(r); - r = mkstemp(lratFilename); - AlwaysAssert(r > 0); - close(r); - std::ofstream formStream(formulaFilename); + std::string formulaFilename("cvc4-dimacs-XXXXXX"); + std::string dratFilename("cvc4-drat-XXXXXX"); + std::string lratFilename("cvc4-lrat-XXXXXX"); + + std::fstream formStream = openTmpFile(&formulaFilename); printDimacs(formStream, clauses, usedIds); formStream.close(); - std::ofstream dratStream(dratFilename); + std::fstream dratStream = openTmpFile(&dratFilename); dratStream << dratBinary; dratStream.close(); + std::fstream lratStream = openTmpFile(&lratFilename); + #if CVC4_USE_DRAT2ER drat2er::drat_trim::CheckAndConvertToLRAT( formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); @@ -159,11 +153,10 @@ LratProof LratProof::fromDratProof( "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); #endif - std::ifstream lratStream(lratFilename); LratProof lrat(lratStream); - remove(formulaFilename); - remove(dratFilename); - remove(lratFilename); + remove(formulaFilename.c_str()); + remove(dratFilename.c_str()); + remove(lratFilename.c_str()); return lrat; } |