From cf9dfb9be23b4f802989fecd18756ed62aecc8e4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 21 Jun 2019 10:55:03 -0700 Subject: 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. --- src/proof/lrat/lrat_proof.cpp | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) (limited to 'src/proof/lrat') 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; } -- cgit v1.2.3