summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/clausal_bitvector_proof.cpp33
-rw-r--r--src/proof/er/er_proof.cpp33
-rw-r--r--src/proof/lrat/lrat_proof.cpp33
-rw-r--r--src/proof/lrat/lrat_proof.h4
-rw-r--r--src/util/CMakeLists.txt1
-rw-r--r--src/util/utility.cpp54
-rw-r--r--src/util/utility.h16
-rw-r--r--test/unit/proof/lrat_proof_black.h5
8 files changed, 114 insertions, 65 deletions
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index 25e519bfb..9e45bb42b 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -29,6 +29,7 @@
#include "proof/lfsc_proof_printer.h"
#include "proof/lrat/lrat_proof.h"
#include "theory/bv/theory_bv.h"
+#include "util/utility.h"
#if CVC4_USE_DRAT2ER
#include "drat2er_options.h"
@@ -111,24 +112,17 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
void ClausalBitVectorProof::optimizeDratProof()
{
Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
- char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
- char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
- char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
- int r;
- r = mkstemp(formulaFilename);
- AlwaysAssert(r > 0);
- close(r);
- r = mkstemp(dratFilename);
- AlwaysAssert(r > 0);
- close(r);
- r = mkstemp(optDratFilename);
- AlwaysAssert(r > 0);
- close(r);
- std::ofstream formStream(formulaFilename);
+ std::string formulaFilename("cvc4-dimacs-XXXXXX");
+ std::string dratFilename("cvc4-drat-XXXXXX");
+ std::string optDratFilename("cvc4-optimized-drat-XXXXXX");
+
+ std::fstream formStream;
+ openTmpFile(&formStream, &formulaFilename);
printDimacs(formStream, d_usedClauses);
formStream.close();
- std::ofstream dratStream(dratFilename);
+ std::fstream dratStream;
+ openTmpFile(&dratStream, &dratFilename);
dratStream << d_binaryDratProof.str();
dratStream.close();
@@ -144,13 +138,14 @@ void ClausalBitVectorProof::optimizeDratProof()
d_binaryDratProof = std::ostringstream{};
Assert(d_binaryDratProof.str().size() == 0);
- std::ifstream lratStream(optDratFilename);
+ std::fstream lratStream;
+ openTmpFile(&lratStream, &optDratFilename);
std::copy(std::istreambuf_iterator<char>(lratStream),
std::istreambuf_iterator<char>(),
std::ostreambuf_iterator<char>(d_binaryDratProof));
- remove(formulaFilename);
- remove(dratFilename);
- remove(optDratFilename);
+ remove(formulaFilename.c_str());
+ remove(dratFilename.c_str());
+ remove(optDratFilename.c_str());
Debug("bv::clausal") << "Optimized DRAT" << std::endl;
}
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;
}
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 0b7af7aa5..ba93209d1 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_printer.h"
#include "proof/lfsc_proof_printer.h"
+#include "util/utility.h"
#if CVC4_USE_DRAT2ER
#include "drat2er_options.h"
@@ -127,24 +128,17 @@ 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(&formStream, &formulaFilename);
printDimacs(formStream, usedClauses);
formStream.close();
- std::ofstream dratStream(dratFilename);
+ std::fstream dratStream;
+ openTmpFile(&dratStream, &dratFilename);
dratStream << dratBinary;
dratStream.close();
@@ -157,11 +151,12 @@ LratProof LratProof::fromDratProof(
"Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
#endif
- std::ifstream lratStream(lratFilename);
+ std::fstream lratStream;
+ openTmpFile(&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;
}
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index a999e5ca6..7cd773409 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -130,10 +130,6 @@ class LratProof
* @brief Construct an LRAT proof from a DRAT proof, using drat-trim
*
* @param usedClauses The CNF formula that we're deriving bottom from.
- * It's a map because other parts of the system represent
- * it this way.
- * @param clauseOrder A record of the order in which those clauses were
- * given to the SAT solver.
* @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
*/
static LratProof fromDratProof(
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index a17f7c510..f107ad95f 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -47,6 +47,7 @@ libcvc4_add_sources(
statistics_registry.h
tuple.h
unsafe_interrupt_exception.h
+ utility.cpp
utility.h
)
diff --git a/src/util/utility.cpp b/src/util/utility.cpp
new file mode 100644
index 000000000..93c36d662
--- /dev/null
+++ b/src/util/utility.cpp
@@ -0,0 +1,54 @@
+/********************* */
+/*! \file utility.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Some standard STL-related utility functions for CVC4
+ **
+ ** Some standard STL-related utility functions for CVC4.
+ **/
+
+#include "util/utility.h"
+
+#include <unistd.h>
+
+#include <cstdlib>
+
+#include "base/cvc4_check.h"
+
+namespace CVC4 {
+
+void openTmpFile(std::fstream* stream, std::string* pattern)
+{
+ char* tmpDir = getenv("TMPDIR");
+ if (tmpDir != nullptr)
+ {
+ *pattern = std::string(tmpDir) + "/" + *pattern;
+ }
+ else
+ {
+ *pattern = "/tmp/" + *pattern;
+ }
+
+ // Note: With C++17, we can avoid creating a copy using std::string::data().
+ char* tmpName = new char[pattern->size() + 1];
+ pattern->copy(tmpName, pattern->size());
+ tmpName[pattern->size()] = '\0';
+ int r = mkstemp(tmpName);
+ if (r == -1)
+ {
+ CVC4_FATAL() << "Could not create temporary file " << *pattern;
+ }
+ stream->open(tmpName);
+ close(r);
+ *pattern = std::string(tmpName);
+ delete[] tmpName;
+}
+
+} // namespace CVC4
diff --git a/src/util/utility.h b/src/util/utility.h
index 56a68ca40..524397ee6 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -20,8 +20,10 @@
#define __CVC4__UTILITY_H
#include <algorithm>
-#include <utility>
+#include <fstream>
#include <functional>
+#include <string>
+#include <utility>
namespace CVC4 {
@@ -85,6 +87,18 @@ void container_to_stream(std::ostream& out,
out << postfix;
}
+/**
+ * Opens a new temporary file with a given filename pattern and returns an
+ * fstream to it. The directory that the file is created in is either TMPDIR or
+ * /tmp/ if TMPDIR is not set.
+ *
+ * @param A filestream for the temporary file.
+ * @param pattern The filename pattern. This string is modified to contain the
+ * name of the temporary file.
+ *
+ */
+void openTmpFile(std::fstream* stream, std::string* pattern);
+
}/* CVC4 namespace */
#endif /* __CVC4__UTILITY_H */
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
index 398c551fe..b4b41922f 100644
--- a/test/unit/proof/lrat_proof_black.h
+++ b/test/unit/proof/lrat_proof_black.h
@@ -22,10 +22,11 @@
#include "prop/sat_solver_types.h"
#include "utils.h"
+using namespace CVC4;
using namespace CVC4::proof::lrat;
using namespace CVC4::prop;
-class LfscProofBlack : public CxxTest::TestSuite
+class LratProofBlack : public CxxTest::TestSuite
{
public:
void setUp() override {}
@@ -34,7 +35,7 @@ class LfscProofBlack : public CxxTest::TestSuite
void testOutputAsLfsc();
};
-void LfscProofBlack::testOutputAsLfsc()
+void LratProofBlack::testOutputAsLfsc()
{
std::vector<std::unique_ptr<LratInstruction>> instructions;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback