summaryrefslogtreecommitdiff
path: root/src/proof/lrat
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-06-21 10:55:03 -0700
committerGitHub <noreply@github.com>2019-06-21 10:55:03 -0700
commitcf9dfb9be23b4f802989fecd18756ed62aecc8e4 (patch)
tree3f1f45759bf85b451b458aab98cf62892f7aef17 /src/proof/lrat
parent073335156ff7644364d12a91d4d41af776cfb91b (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.cpp31
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback