diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 45 | ||||
-rw-r--r-- | src/proof/er/er_proof.cpp | 32 | ||||
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 31 |
3 files changed, 39 insertions, 69 deletions
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 07589fd07..5d6641e49 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -120,32 +120,22 @@ void ClausalBitVectorProof::optimizeDratProof() 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, @@ -164,17 +154,14 @@ void ClausalBitVectorProof::optimizeDratProof() 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 @@ -213,11 +200,13 @@ void ClausalBitVectorProof::optimizeDratProof() 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 diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 7b966f2c6..9952e6b3e 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -85,32 +85,22 @@ ErProof ErProof::fromBinaryDratProof( 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, @@ -119,7 +109,6 @@ ErProof ErProof::fromBinaryDratProof( false, drat2er::options::QUIET, false); - #else Unimplemented( "ER proof production requires drat2er.\n" @@ -127,14 +116,13 @@ ErProof ErProof::fromBinaryDratProof( #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; } 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; } |