diff options
Diffstat (limited to 'src/proof/clausal_bitvector_proof.cpp')
| -rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 412 |
1 files changed, 0 insertions, 412 deletions
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp deleted file mode 100644 index 21e8056ca..000000000 --- a/src/proof/clausal_bitvector_proof.cpp +++ /dev/null @@ -1,412 +0,0 @@ -/********************* */ -/*! \file clausal_bitvector_proof.cpp - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Bitvector proof using the DRAT proof format - ** - ** Contains DRAT-specific printing logic. - **/ - -#include "cvc4_private.h" - -#include <algorithm> -#include <iostream> -#include <iterator> -#include <map> - -#include "options/bv_options.h" -#include "proof/clausal_bitvector_proof.h" -#include "proof/dimacs.h" -#include "proof/drat/drat_proof.h" -#include "proof/er/er_proof.h" -#include "proof/lfsc_proof_printer.h" -#include "proof/lrat/lrat_proof.h" -#include "prop/sat_solver_types.h" -#include "smt/smt_statistics_registry.h" -#include "theory/bv/theory_bv.h" - -#if CVC4_USE_DRAT2ER -#include "drat2er_options.h" -#include "drat_trim_interface.h" -#endif - -namespace CVC4 { - -namespace proof { - -ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv, - TheoryProofEngine* proofEngine) - : BitVectorProof(bv, proofEngine), - d_clauses(), - d_originalClauseIndices(), - d_binaryDratProof(), - d_coreClauseIndices(), - d_dratTranslationStatistics(), - d_dratOptimizationStatistics() -{ -} - -void ClausalBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver) -{ - sat_solver.setClausalProofLog(this); -} - -void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf, - prop::SatVariable trueVar, - prop::SatVariable falseVar) -{ - Assert(d_cnfProof == nullptr); - d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); - - // Create a clause which forces the true variable to be true, and register it - int trueClauseId = ClauseId(ProofManager::currentPM()->nextId()); - // with the CNF proof - d_cnfProof->registerTrueUnitClause(trueClauseId); - // and with (this) bit-vector proof - prop::SatClause c{prop::SatLiteral(trueVar, false)}; - registerUsedClause(trueClauseId, c); - - // The same for false. - int falseClauseId = ClauseId(ProofManager::currentPM()->nextId()); - d_cnfProof->registerFalseUnitClause(falseClauseId); - c[0] = prop::SatLiteral(falseVar, true); - registerUsedClause(falseClauseId, c); -} - -void ClausalBitVectorProof::registerUsedClause(ClauseId id, - prop::SatClause& clause) -{ - prop::SatClause& emplaced_clause = - d_clauses.emplace(id, clause).first->second; - canonicalizeClause(emplaced_clause); - d_originalClauseIndices.push_back(id); -}; - -void ClausalBitVectorProof::calculateAtomsInBitblastingProof() -{ - optimizeDratProof(); - - // Debug dump of DRAT Proof - if (Debug.isOn("bv::clausal")) - { - std::string serializedDratProof = d_binaryDratProof.str(); - Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof() - << std::endl; - Debug("bv::clausal") << "binary DRAT proof byte count: " - << serializedDratProof.size() << std::endl; - Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size() - << std::endl; - } - - // Empty any old record of which atoms were used - d_atomsInBitblastingProof.clear(); - Assert(d_atomsInBitblastingProof.size() == 0); - - // For each used clause, ask the CNF proof which atoms are used in it - for (const ClauseId usedIdx : d_coreClauseIndices) - { - d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof); - } -} - -struct SatClausePointerComparator -{ - inline bool operator()(const prop::SatClause* const& l, - const prop::SatClause* const& r) const - { - prop::SatClauseLessThan cmp; - return cmp(*l, *r); - } -}; - -void ClausalBitVectorProof::optimizeDratProof() -{ - TimerStat::CodeTimer optimizeDratProofTimer{ - d_dratOptimizationStatistics.d_totalTime}; - if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::PROOF - || options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) - { - Debug("bv::clausal") << "Optimizing DRAT" << std::endl; - 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::unique_ptr<std::fstream> formStream = openTmpFile(&formulaFilename); - const int64_t startPos = static_cast<int64_t>(formStream->tellp()); - printDimacs(*formStream, d_clauses, d_originalClauseIndices); - d_dratOptimizationStatistics.d_initialFormulaSize.setData( - static_cast<int64_t>(formStream->tellp()) - startPos); - formStream->close(); - } - - { - std::unique_ptr<std::fstream> dratStream = openTmpFile(&dratFilename); - const int64_t startPos = static_cast<int64_t>(dratStream->tellp()); - (*dratStream) << d_binaryDratProof.str(); - d_dratOptimizationStatistics.d_initialDratSize.setData( - static_cast<int64_t>(dratStream->tellp()) - startPos); - dratStream->close(); - } - - std::unique_ptr<std::fstream> optDratStream = openTmpFile(&optDratFilename); - std::unique_ptr<std::fstream> optFormulaStream = - openTmpFile(&optFormulaFilename); - -#if CVC4_USE_DRAT2ER - { - TimerStat::CodeTimer runDratTimeOptimizationTimer{ - d_dratOptimizationStatistics.d_toolTime}; - int dratTrimExitCode = - drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename, - dratFilename, - optFormulaFilename, - optDratFilename, - drat2er::options::QUIET); - AlwaysAssert(dratTrimExitCode == 0) - << "drat-trim exited with " << dratTrimExitCode; - } -#else - Unimplemented() - << "Proof production when using CryptoMiniSat requires drat2er.\n" - << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"; -#endif - - { - d_binaryDratProof.str(""); - Assert(d_binaryDratProof.str().size() == 0); - - const int64_t startPos = static_cast<int64_t>(d_binaryDratProof.tellp()); - std::ifstream lratStream(optDratFilename); - std::copy(std::istreambuf_iterator<char>(lratStream), - std::istreambuf_iterator<char>(), - std::ostreambuf_iterator<char>(d_binaryDratProof)); - d_dratOptimizationStatistics.d_optimizedDratSize.setData( - static_cast<int64_t>(d_binaryDratProof.tellp()) - startPos); - } - - if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) - { - std::ifstream optFormulaInStream{optFormulaFilename}; - const int64_t startPos = static_cast<int64_t>(optFormulaInStream.tellg()); - std::vector<prop::SatClause> core = parseDimacs(optFormulaInStream); - d_dratOptimizationStatistics.d_optimizedFormulaSize.setData( - static_cast<int64_t>(optFormulaInStream.tellg()) - startPos); - - CodeTimer clauseMatchingTimer{ - d_dratOptimizationStatistics.d_clauseMatchingTime}; - - // 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 - // removed duplicate literals. We use literal sets as the canonical clause - // form. - // - // TODO (aozdemir) It may be better to use a hash map instead of a tree - // map here. - std::map<const prop::SatClause*, ClauseId, SatClausePointerComparator> - cannonicalClausesToIndices; - for (const auto& kv : d_clauses) - { - cannonicalClausesToIndices[&kv.second] = kv.first; - } - - d_coreClauseIndices.clear(); - - for (prop::SatClause& coreClause : core) - { - canonicalizeClause(coreClause); - d_coreClauseIndices.push_back( - cannonicalClausesToIndices.at(&coreClause)); - } - Debug("bv::clausal") << "Optimizing the DRAT proof and the formula" - << std::endl; - } - else - { - Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula" - << std::endl; - d_coreClauseIndices = d_originalClauseIndices; - } - - optFormulaStream->close(); - - Assert(d_coreClauseIndices.size() > 0); - remove(formulaFilename.c_str()); - remove(dratFilename.c_str()); - remove(optDratFilename.c_str()); - remove(optFormulaFilename.c_str()); - Debug("bv::clausal") << "Optimized DRAT" << std::endl; - } - else - { - Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof" - << std::endl; - d_coreClauseIndices = d_originalClauseIndices; - } -} - -void ClausalBitVectorProof::canonicalizeClause(prop::SatClause& clause) -{ - std::sort(clause.begin(), clause.end()); - clause.erase(std::unique(clause.begin(), clause.end()), clause.end()); -} - -ClausalBitVectorProof::DratTranslationStatistics::DratTranslationStatistics() - : d_totalTime("proof::bv::dratTranslation::totalTime"), - d_toolTime("proof::bv::dratTranslation::toolTime") -{ - smtStatisticsRegistry()->registerStat(&d_totalTime); - smtStatisticsRegistry()->registerStat(&d_toolTime); -} - -ClausalBitVectorProof::DratTranslationStatistics::~DratTranslationStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_totalTime); - smtStatisticsRegistry()->unregisterStat(&d_toolTime); -} - -ClausalBitVectorProof::DratOptimizationStatistics::DratOptimizationStatistics() - : d_totalTime("proof::bv::dratOptimization::totalTime"), - d_toolTime("proof::bv::dratOptimization::toolTime"), - d_clauseMatchingTime("proof::bv::dratOptimization::clauseMatchingTime"), - d_initialDratSize("proof::bv::dratOptimization::initialDratSize", 0), - d_optimizedDratSize("proof::bv::dratOptimization::optimizedDratSize", 0), - d_initialFormulaSize("proof::bv::dratOptimization::initialFormulaSize", - 0), - d_optimizedFormulaSize( - "proof::bv::dratOptimization::optimizedFormulaSize", 0) -{ - smtStatisticsRegistry()->registerStat(&d_totalTime); - smtStatisticsRegistry()->registerStat(&d_toolTime); - smtStatisticsRegistry()->registerStat(&d_clauseMatchingTime); - smtStatisticsRegistry()->registerStat(&d_initialDratSize); - smtStatisticsRegistry()->registerStat(&d_optimizedDratSize); - smtStatisticsRegistry()->registerStat(&d_initialFormulaSize); - smtStatisticsRegistry()->registerStat(&d_optimizedFormulaSize); -} - -ClausalBitVectorProof::DratOptimizationStatistics::~DratOptimizationStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_totalTime); - smtStatisticsRegistry()->unregisterStat(&d_toolTime); - smtStatisticsRegistry()->unregisterStat(&d_clauseMatchingTime); - smtStatisticsRegistry()->unregisterStat(&d_initialDratSize); - smtStatisticsRegistry()->unregisterStat(&d_optimizedDratSize); - smtStatisticsRegistry()->unregisterStat(&d_initialFormulaSize); - smtStatisticsRegistry()->unregisterStat(&d_optimizedFormulaSize); -} - -void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) -{ - Unreachable() << "Clausal bit-vector proofs should only be used in " - "combination with eager " - "bitblasting, which **does not use theory lemmas**"; -} - -void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) -{ - os << "\n;; Bitblasting mappings\n"; - printBitblasting(os, paren); - - os << "\n;; BB-CNF mappings\n"; - d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); - - os << "\n;; BB-CNF proofs\n"; - for (const ClauseId id : d_coreClauseIndices) - { - d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren); - } -} - -void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, - std::ostream& paren) -{ - Assert(options::bitblastMode() == options::BitblastMode::EAGER) - << "the BV theory should only be proving bottom directly in the eager " - "bitblasting mode"; - - os << "\n;; Proof of input to SAT solver\n"; - os << "(@ proofOfSatInput "; - paren << ")"; - - LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb"); - - os << "\n;; DRAT Proof Value\n"; - os << "(@ dratProof "; - paren << ")"; - d_dratTranslationStatistics.d_totalTime.start(); - drat::DratProof pf = drat::DratProof::fromBinary(d_binaryDratProof.str()); - d_dratTranslationStatistics.d_totalTime.stop(); - pf.outputAsLfsc(os, 2); - os << "\n"; - - os << "\n;; Verification of DRAT Proof\n"; - os << "(drat_proof_of_bottom _ proofOfSatInput dratProof " - << "\n)"; -} - -void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os, - std::ostream& paren) -{ - Assert(options::bitblastMode() == options::BitblastMode::EAGER) - << "the BV theory should only be proving bottom directly in the eager " - "bitblasting mode"; - - os << "\n;; Proof of input to SAT solver\n"; - os << "(@ proofOfCMap "; - paren << ")"; - LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb"); - - os << "\n;; DRAT Proof Value\n"; - os << "(@ lratProof "; - paren << ")"; - d_dratTranslationStatistics.d_totalTime.start(); - lrat::LratProof pf = - lrat::LratProof::fromDratProof(d_clauses, - d_coreClauseIndices, - d_binaryDratProof.str(), - d_dratTranslationStatistics.d_toolTime); - d_dratTranslationStatistics.d_totalTime.stop(); - pf.outputAsLfsc(os); - os << "\n"; - - os << "\n;; Verification of DRAT Proof\n"; - os << "(lrat_proof_of_bottom _ proofOfCMap lratProof " - << "\n)"; -} - -void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os, - std::ostream& paren) -{ - Assert(options::bitblastMode() == options::BitblastMode::EAGER) - << "the BV theory should only be proving bottom directly in the eager " - "bitblasting mode"; - - d_dratTranslationStatistics.d_totalTime.start(); - er::ErProof pf = - er::ErProof::fromBinaryDratProof(d_clauses, - d_coreClauseIndices, - d_binaryDratProof.str(), - d_dratTranslationStatistics.d_toolTime); - d_dratTranslationStatistics.d_totalTime.stop(); - - pf.outputAsLfsc(os); -} - -} // namespace proof - -}; // namespace CVC4 |