From 5d0a5a729680a1db3f44e31037955390e86440ce Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 15 Mar 2019 18:51:47 -0700 Subject: [PATCH] Enable CryptoMiniSat-backed BV proofs (#2847) * Connect the plumbing so that BV proofs are enabled when using CryptoMiniSat * Also fixed a bug in CNF-proof generation * Specifically, CNF proofs broke when proving tautological clauses. Now they don't. --- proofs/signatures/CMakeLists.txt | 3 + src/base/configuration.cpp | 2 + src/base/configuration.h | 2 + src/options/bv_options.toml | 2 +- src/options/options_handler.cpp | 6 +- src/proof/bitvector_proof.cpp | 8 + src/proof/bitvector_proof.h | 2 +- src/proof/clausal_bitvector_proof.cpp | 104 ++++++++++++- src/proof/clausal_bitvector_proof.h | 47 +++++- src/proof/cnf_proof.cpp | 173 +++++++++++++++------ src/proof/cnf_proof.h | 5 + src/proof/drat/drat_proof.cpp | 6 +- src/proof/er/er_proof.cpp | 26 ++-- src/proof/proof_manager.cpp | 3 +- src/proof/theory_proof.cpp | 23 ++- test/regress/regress0/bv/ackermann2.smt2 | 5 + test/regress/regress0/bv/core/slice-12.smt | 6 + test/regress/regress0/bv/temp.lrat | 0 test/unit/proof/drat_proof_black.h | 4 +- test/unit/proof/lrat_proof_black.h | 3 +- 20 files changed, 346 insertions(+), 84 deletions(-) create mode 100644 test/regress/regress0/bv/temp.lrat diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index 8af026952..6e9c8947d 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -5,8 +5,11 @@ set(core_signature_files sat.plf + er.plf smt.plf th_base.plf + lrat.plf + drat.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index f154e5c90..79b0bff9c 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -250,6 +250,8 @@ bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } +bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; } + bool Configuration::isBuiltWithReadline() { return IS_READLINE_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index b6e2a1963..7900e877e 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -97,6 +97,8 @@ public: static bool isBuiltWithCryptominisat(); + static bool isBuiltWithDrat2Er(); + static bool isBuiltWithReadline(); static bool isBuiltWithLfsc(); diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index c4541f4e4..6dd755625 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -7,7 +7,7 @@ header = "options/bv_options.h" category = "expert" long = "bv-proof-format=MODE" type = "CVC4::theory::bv::BvProofFormat" - default = "CVC4::theory::bv::BITVECTOR_PROOF_LRAT" + default = "CVC4::theory::bv::BITVECTOR_PROOF_ER" handler = "stringToBvProofFormat" predicates = ["satSolverEnabledBuild"] includes = ["options/bv_bitblast_mode.h"] diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 84b9f3b4c..ad4fc8d48 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1769,10 +1769,11 @@ void OptionsHandler::proofEnabledBuild(std::string option, bool value) { #ifdef CVC4_PROOF if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER - && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT + && options::bvSatSolver() != theory::bv::SAT_SOLVER_CRYPTOMINISAT) { throw OptionException( - "Eager BV proofs only supported when minisat is used"); + "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used"); } #else if(value) { @@ -1938,6 +1939,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("glpk", Configuration::isBuiltWithGlpk()); print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); + print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("readline", Configuration::isBuiltWithReadline()); diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 90c0c9b30..b42a464ab 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -221,6 +221,14 @@ void BitVectorProof::printOwnedTerm(Expr term, } } +void BitVectorProof::printEmptyClauseProof(std::ostream& os, + std::ostream& paren) +{ + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER, + "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"); +} + void BitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4b897a6c6..d963f6d61 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -167,7 +167,7 @@ class BitVectorProof : public TheoryProof * @param os the stream to print to * @param paren any parentheses to add to the end of the global proof */ - virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0; + virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren); /** * Read the d_atomsInBitblastingProof member. diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index bb875d1d8..eed295b1a 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -19,10 +19,13 @@ #include #include #include + #include "options/bv_options.h" #include "proof/clausal_bitvector_proof.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 "theory/bv/theory_bv.h" namespace CVC4 { @@ -66,12 +69,12 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, void ClausalBitVectorProof::registerUsedClause(ClauseId id, prop::SatClause& clause) { - d_usedClauses.emplace_back( - id, std::unique_ptr(new prop::SatClause(clause))); + d_usedClauses.emplace_back(id, clause); }; void ClausalBitVectorProof::calculateAtomsInBitblastingProof() { + // Debug dump of DRAT Proof if (Debug.isOn("bv::clausal")) { std::string serializedDratProof = d_binaryDratProof.str(); @@ -84,7 +87,16 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof() Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl; dratProof.outputAsText(Debug("bv::clausal")); } - Unimplemented(); + + // Empty any old record of which atoms were used + d_atomsInBitblastingProof.clear(); + + // For each used clause, ask the CNF proof which atoms are used in it + for (const auto& usedIndexAndClause : d_usedClauses) + { + d_cnfProof->collectAtoms(&usedIndexAndClause.second, + d_atomsInBitblastingProof); + } } void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector& lemma, @@ -101,13 +113,91 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) { - Unimplemented(); + 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 auto& idAndClause : d_usedClauses) + { + d_cnfProof->printCnfProofForClause( + idAndClause.first, &idAndClause.second, os, paren); + } } -void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os, - std::ostream& paren) +void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, + std::ostream& paren) { - Unimplemented(); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_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 << ")"; + std::vector usedIds; + usedIds.reserve(d_usedClauses.size()); + for (const auto& idAnd : d_usedClauses) + { + usedIds.push_back(idAnd.first); + }; + LFSCProofPrinter::printSatInputProof(usedIds, os, "bb"); + + os << "\n;; DRAT Proof Value\n"; + os << "(@ dratProof "; + paren << ")"; + drat::DratProof::fromBinary(d_binaryDratProof.str()).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() == theory::bv::BITBLAST_MODE_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 << ")"; + std::vector usedIds; + usedIds.reserve(d_usedClauses.size()); + for (const auto& idAnd : d_usedClauses) + { + usedIds.push_back(idAnd.first); + }; + LFSCProofPrinter::printCMapProof(usedIds, os, "bb"); + + os << "\n;; DRAT Proof Value\n"; + os << "(@ lratProof "; + paren << ")"; + lrat::LratProof pf = + lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str()); + 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() == theory::bv::BITBLAST_MODE_EAGER, + "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"); + + er::ErProof pf = + er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str()); + + pf.outputAsLfsc(os); } } // namespace proof diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h index 85e409e0d..cd215da36 100644 --- a/src/proof/clausal_bitvector_proof.h +++ b/src/proof/clausal_bitvector_proof.h @@ -61,8 +61,7 @@ class ClausalBitVectorProof : public BitVectorProof protected: // A list of all clauses and their ids which are passed into the SAT solver - std::vector>> - d_usedClauses; + std::vector> d_usedClauses; // Stores the proof recieved from the SAT solver. std::ostringstream d_binaryDratProof; }; @@ -77,7 +76,6 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof TheoryProofEngine* proofEngine) : ClausalBitVectorProof(bv, proofEngine) { - // That's all! } void printTheoryLemmaProof(std::vector& lemma, @@ -87,6 +85,49 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof void printBBDeclarationAndCnf(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) override; +}; + +/** + * A DRAT proof for a bit-vector problem + */ +class LfscDratBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscDratBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; +}; + +/** + * An LRAT proof for a bit-vector problem + */ +class LfscLratBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscLratBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; +}; + +/** + * An Extended Resolution proof for a bit-vector problem + */ +class LfscErBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; }; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 4e8d20162..aed889e33 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -349,6 +349,39 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } +// Detects whether a clause has x v ~x for some x +// If so, returns the positive occurence's idx first, then the negative's +Maybe> CnfProof::detectTrivialTautology( + const prop::SatClause& clause) +{ + // a map from a SatVariable to its previous occurence's polarity and location + std::map> varsToPolsAndIndices; + for (size_t i = 0; i < clause.size(); ++i) + { + prop::SatLiteral lit = clause[i]; + prop::SatVariable var = lit.getSatVariable(); + bool polarity = !lit.isNegated(); + + // Check if this var has already occured w/ opposite polarity + auto iter = varsToPolsAndIndices.find(var); + if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity) + { + if (iter->second.first) + { + return Maybe>{ + std::make_pair(iter->second.second, i)}; + } + else + { + return Maybe>{ + std::make_pair(i, iter->second.second)}; + } + } + varsToPolsAndIndices[var] = std::make_pair(polarity, i); + } + return Maybe>{}; +} + void LFSCCnfProof::printAtomMapping(const std::set& atoms, std::ostream& os, std::ostream& paren) { @@ -431,61 +464,98 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Assert( clause->size()>0 ); - Node base_assertion = getDefinitionForClause(id); - - //get the assertion for the clause id - std::map childIndex; - std::map childPol; - Node assertion = clauseToNode( *clause, childIndex, childPol ); - //if there is no reason, construct assertion directly. This can happen for unit clauses. - if( base_assertion.isNull() ){ - base_assertion = assertion; + // If the clause contains x v ~x, it's easy! + // + // It's important to check for this case, because our other logic for + // recording the location of variables in the clause assumes the clause is + // not tautological + Maybe> isTrivialTaut = + detectTrivialTautology(*clause); + if (isTrivialTaut.just()) + { + size_t posIndexInClause = isTrivialTaut.value().first; + size_t negIndexInClause = isTrivialTaut.value().second; + Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and " + << negIndexInClause << " (-) make this clause a tautology" + << std::endl; + + std::string proofOfPos = + ProofManager::getLitName((*clause)[negIndexInClause], d_name); + std::string proofOfNeg = + ProofManager::getLitName((*clause)[posIndexInClause], d_name); + os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")"; } - //os_base is proof of base_assertion - std::stringstream os_base; - - // checks if tautological definitional clause or top-level clause - // and prints the proof of the top-level formula - bool is_input = printProofTopLevel(base_assertion, os_base); + else + { + Node base_assertion = getDefinitionForClause(id); + + // get the assertion for the clause id + std::map childIndex; + std::map childPol; + Node assertion = clauseToNode(*clause, childIndex, childPol); + // if there is no reason, construct assertion directly. This can happen + // for unit clauses. + if (base_assertion.isNull()) + { + base_assertion = assertion; + } + // os_base is proof of base_assertion + std::stringstream os_base; + + // checks if tautological definitional clause or top-level clause + // and prints the proof of the top-level formula + bool is_input = printProofTopLevel(base_assertion, os_base); + + if (is_input) + { + Debug("cnf-pf") << std::endl + << "; base assertion is input. proof: " << os_base.str() + << std::endl; + } - if (is_input) { - Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl; - } + // get base assertion with polarity + bool base_pol = base_assertion.getKind() != kind::NOT; + base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0] + : base_assertion; - //get base assertion with polarity - bool base_pol = base_assertion.getKind()!=kind::NOT; - base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; - - std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion ); - bool is_in_clause = itci!=childIndex.end(); - unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; - if (!is_input){ - Assert(is_in_clause); - prop::SatLiteral blit = (*clause)[ base_index ]; - os_base << ProofManager::getLitName(blit, d_name); - base_pol = !childPol[base_assertion]; // WHY? if the case is => - } - Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; - Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; - - bool success = false; - if( is_input && - is_in_clause && - childPol[base_assertion]==base_pol ){ - //if both in input and in clause, the proof is trivial. this is the case for unit clauses. - Trace("cnf-pf") << "; trivial" << std::endl; - os << "(contra _ "; - success = true; - prop::SatLiteral lit = (*clause)[itci->second]; - if( base_pol ){ - os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); - }else{ - os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); + std::map::iterator itci = childIndex.find(base_assertion); + bool is_in_clause = itci != childIndex.end(); + unsigned base_index = is_in_clause ? itci->second : 0; + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; input = " << is_input + << ", is_in_clause = " << is_in_clause << ", id = " << id + << ", assertion = " << assertion + << ", base assertion = " << base_assertion << std::endl; + if (!is_input) + { + Assert(is_in_clause); + prop::SatLiteral blit = (*clause)[base_index]; + os_base << ProofManager::getLitName(blit, d_name); + base_pol = !childPol[base_assertion]; // WHY? if the case is => } - os << ")"; - } else if ((base_assertion.getKind()==kind::AND && !base_pol) || + Trace("cnf-pf") << "; polarity of base assertion = " << base_pol + << std::endl; + Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; + + bool success = false; + if (is_input && is_in_clause && childPol[base_assertion] == base_pol) + { + // if both in input and in clause, the proof is trivial. this is the case + // for unit clauses. + Trace("cnf-pf") << "; trivial" << std::endl; + os << "(contra _ "; + success = true; + prop::SatLiteral lit = (*clause)[itci->second]; + if (base_pol) + { + os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); + } + else + { + os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); + } + os << ")"; + } else if ((base_assertion.getKind()==kind::AND && !base_pol) || ((base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES) && base_pol)) { Trace("cnf-pf") << "; and/or case 1" << std::endl; @@ -776,6 +846,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Trace("cnf-pf") << std::endl; os << "trust-bad"; } + } os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 78ddeebd0..481e77c75 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -29,6 +29,7 @@ #include "proof/clause_id.h" #include "proof/lemma_proof.h" #include "proof/sat_proof.h" +#include "util/maybe.h" #include "util/proof.h" namespace CVC4 { @@ -164,6 +165,10 @@ public: std::ostream& paren, ProofLetMap &letMap) = 0; + // Detects whether a clause has x v ~x for some x + // If so, returns the positive occurence's idx first, then the negative's + static Maybe> detectTrivialTautology( + const prop::SatClause& clause); virtual void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) = 0; diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index c2f2fa49e..5b9487a00 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -259,12 +259,12 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const { case ADDITION: { - os << "DRATProofa"; + os << "DRATProofa "; break; } case DELETION: { - os << "DRATProofd"; + os << "DRATProofd "; break; } default: { Unreachable("Unrecognized DRAT instruction kind"); @@ -273,7 +273,7 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const for (const SatLiteral& l : i.d_clause) { os << "(clc (" << (l.isNegated() ? "neg " : "pos ") - << ProofManager::getVarName(l.getSatVariable()) << ") "; + << ProofManager::getVarName(l.getSatVariable(), "bb") << ") "; } os << "cln"; std::fill_n(std::ostream_iterator(os), i.d_clause.size(), ')'); diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 452b64b11..22903c3c9 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -102,12 +102,12 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, // Write the formula std::ofstream formStream(formulaFilename); printDimacs(formStream, usedClauses); - unlink(formulaFilename); + formStream.close(); // Write the (binary) DRAT proof std::ofstream dratStream(dratFilename); dratStream << dratBinary; - unlink(dratFilename); + dratStream.close(); // Invoke drat2er #if CVC4_USE_DRAT2ER @@ -115,7 +115,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, dratFilename, tracecheckFilename, false, - drat2er::options::QUIET); + drat2er::options::QUIET, + false); #else Unimplemented( @@ -126,13 +127,11 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, // Parse the resulting TRACECHECK proof into an ER proof. std::ifstream tracecheckStream(tracecheckFilename); ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream)); - unlink(tracecheckFilename); - - formStream.close(); - dratStream.close(); tracecheckStream.close(); - + remove(formulaFilename); + remove(dratFilename); + remove(tracecheckFilename); return proof; } @@ -154,6 +153,15 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses, { for (size_t i = 0, n = usedClauses.size(); i < n; ++i) { + Assert(d_tracecheck.d_lines[i].d_idx = i + 1); + Assert(d_tracecheck.d_lines[i].d_chain.size() == 0); + std::unordered_set + traceCheckClause{d_tracecheck.d_lines[i].d_clause.begin(), + d_tracecheck.d_lines[i].d_clause.end()}; + std::unordered_set + originalClause{usedClauses[i].second.begin(), + usedClauses[i].second.end()}; + Assert(traceCheckClause == originalClause); Assert(d_tracecheck.d_lines[i].d_idx = i + 1); Assert(d_tracecheck.d_lines[i].d_chain.size() == 0); Assert(d_tracecheck.d_lines[i].d_clause.size() @@ -185,7 +193,7 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses, // Look at the negation of the second literal in the second clause to get // the old literal AlwaysAssert(d_tracecheck.d_lines.size() > i + 1, - "Malformed definition in TRACECHECK proof from drat2er"); + "Malformed definition in TRACECHECK proof from drat2er"); d_definitions.emplace_back(newVar, ~d_tracecheck.d_lines[i + 1].d_clause[1], std::move(otherLiterals)); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5f0ade86a..ace41892f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -734,8 +734,7 @@ void LFSCProof::toStream(std::ostream& out) const out << ";; Printing final unsat proof \n"; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - proof::LFSCProofPrinter::printResolutionEmptyClause( - ProofManager::getBitVectorProof()->getSatProof(), out, paren); + ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren); } else { // print actual resolution proof proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index fe9acfef3..66805ecd4 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -85,8 +85,27 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT) { - proof::BitVectorProof* bvp = - new proof::LfscClausalBitVectorProof(thBv, this); + proof::BitVectorProof* bvp = nullptr; + switch (options::bvProofFormat()) + { + case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT: + { + bvp = new proof::LfscDratBitVectorProof(thBv, this); + break; + } + case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT: + { + bvp = new proof::LfscLratBitVectorProof(thBv, this); + break; + } + case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER: + { + bvp = new proof::LfscErBitVectorProof(thBv, this); + break; + } + default: { Unreachable("Invalid BvProofFormat"); + } + }; d_theoryProofTable[id] = bvp; } else diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2 index b1aaa7d64..1799df63c 100644 --- a/test/regress/regress0/bv/ackermann2.smt2 +++ b/test/regress/regress0/bv/ackermann2.smt2 @@ -1,4 +1,9 @@ ; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores +; REQUIRES: cryptominisat +; REQUIRES: drat2er +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/bv/core/slice-12.smt b/test/regress/regress0/bv/core/slice-12.smt index 998dee663..261d55ec9 100644 --- a/test/regress/regress0/bv/core/slice-12.smt +++ b/test/regress/regress0/bv/core/slice-12.smt @@ -1,3 +1,9 @@ +; REQUIRES: cryptominisat +; REQUIRES: drat2er +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores +; EXPECT: unsat (benchmark slice :status unsat :logic QF_BV diff --git a/test/regress/regress0/bv/temp.lrat b/test/regress/regress0/bv/temp.lrat new file mode 100644 index 000000000..e69de29bb diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h index 946597bea..2859d0682 100644 --- a/test/unit/proof/drat_proof_black.h +++ b/test/unit/proof/drat_proof_black.h @@ -170,8 +170,8 @@ void DratProofBlack::testOutputTwoAsLfsc() } } std::string expectedLfsc = - "(DRATProofd (clc (neg .v62) (clc (neg .v8192) cln))" - "(DRATProofa (clc (pos .v128) (clc (neg .v8190) cln))" + "(DRATProofd (clc (neg bb.v62) (clc (neg bb.v8192) cln))" + "(DRATProofa (clc (pos bb.v128) (clc (neg bb.v8190) cln))" "DRATProofn))"; std::ostringstream expectedLfscWithoutWhitespace; for (char c : expectedLfsc) diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h index 48f571841..398c551fe 100644 --- a/test/unit/proof/lrat_proof_black.h +++ b/test/unit/proof/lrat_proof_black.h @@ -91,5 +91,6 @@ void LfscProofBlack::testOutputAsLfsc() " RATHintsn)) " "LRATProofn)))"; - TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(expectedLfsc)); + TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), + filterWhitespace(expectedLfsc)); } -- 2.30.2