BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
{
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";
- char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-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);
- r = mkstemp(optFormulaFilename);
- 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::string optFormulaFilename("cvc4-optimized-formula-XXXXXX");
+
+ std::fstream formStream = openTmpFile(&formulaFilename);
printDimacs(formStream, d_clauses, d_originalClauseIndices);
formStream.close();
- std::ofstream dratStream(dratFilename);
+ std::fstream dratStream = openTmpFile(&dratFilename);
dratStream << d_binaryDratProof.str();
dratStream.close();
+ std::fstream optDratStream = openTmpFile(&optDratFilename);
+ std::fstream optFormulaStream = openTmpFile(&optFormulaFilename);
+
#if CVC4_USE_DRAT2ER
int dratTrimExitCode =
drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
d_binaryDratProof.str("");
Assert(d_binaryDratProof.str().size() == 0);
- std::ifstream lratStream(optDratFilename);
- std::copy(std::istreambuf_iterator<char>(lratStream),
+ std::copy(std::istreambuf_iterator<char>(optDratStream),
std::istreambuf_iterator<char>(),
std::ostreambuf_iterator<char>(d_binaryDratProof));
if (options::bvOptimizeSatProof()
== theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
{
- std::ifstream optFormulaStream{optFormulaFilename};
std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
- optFormulaStream.close();
// Now we need to compute the clause indices for the UNSAT core. This is a
// bit difficult because drat-trim may have reordered clauses, and/or
d_coreClauseIndices = d_originalClauseIndices;
}
+ optFormulaStream.close();
+
Assert(d_coreClauseIndices.size() > 0);
- remove(formulaFilename);
- remove(dratFilename);
- remove(optDratFilename);
- remove(optFormulaFilename);
+ remove(formulaFilename.c_str());
+ remove(dratFilename.c_str());
+ remove(optDratFilename.c_str());
+ remove(optFormulaFilename.c_str());
Debug("bv::clausal") << "Optimized DRAT" << std::endl;
}
else
const std::vector<ClauseId>& usedIds,
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("cvc4-dimacs-XXXXXX");
+ std::string dratFilename("cvc4-drat-XXXXXX");
+ std::string tracecheckFilename("cvc4-tracecheck-er-XXXXXX");
// Write the formula
- std::ofstream formStream(formulaFilename);
+ std::fstream formStream = openTmpFile(&formulaFilename);
printDimacs(formStream, clauses, usedIds);
formStream.close();
// Write the (binary) DRAT proof
- std::ofstream dratStream(dratFilename);
+ std::fstream dratStream = openTmpFile(&dratFilename);
dratStream << dratBinary;
dratStream.close();
+ std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
+
// Invoke drat2er
#if CVC4_USE_DRAT2ER
drat2er::TransformDRATToExtendedResolution(formulaFilename,
false,
drat2er::options::QUIET,
false);
-
#else
Unimplemented(
"ER proof production requires drat2er.\n"
#endif
// Parse the resulting TRACECHECK proof into an ER proof.
- std::ifstream tracecheckStream(tracecheckFilename);
TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
ErProof proof(clauses, usedIds, std::move(pf));
tracecheckStream.close();
- remove(formulaFilename);
- remove(dratFilename);
- remove(tracecheckFilename);
+ remove(formulaFilename.c_str());
+ remove(dratFilename.c_str());
+ remove(tracecheckFilename.c_str());
return proof;
}
#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"
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);
"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;
}
statistics_registry.h
tuple.h
unsafe_interrupt_exception.h
+ utility.cpp
utility.h
)
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#include "base/cvc4_check.h"
+
+namespace CVC4 {
+
+std::fstream openTmpFile(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;
+ }
+ std::fstream tmpStream(tmpName);
+ close(r);
+ *pattern = std::string(tmpName);
+ delete[] tmpName;
+ return tmpStream;
+}
+
+} // namespace CVC4
#define CVC4__UTILITY_H
#include <algorithm>
-#include <utility>
+#include <fstream>
#include <functional>
+#include <string>
+#include <utility>
namespace CVC4 {
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 pattern The filename pattern. This string is modified to contain the
+ * name of the temporary file.
+ *
+ * @return A filestream for the temporary file.
+ */
+std::fstream openTmpFile(std::string* pattern);
+
}/* CVC4 namespace */
#endif /* CVC4__UTILITY_H */
#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 {}
void testOutputAsLfsc();
};
-void LfscProofBlack::testOutputAsLfsc()
+void LratProofBlack::testOutputAsLfsc()
{
std::vector<std::unique_ptr<LratInstruction>> instructions;
projects / cvc5.git / commitdiff