diff options
28 files changed, 510 insertions, 151 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 502db63f4..d9fc80a92 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -130,6 +130,8 @@ libcvc4_add_sources( proof/array_proof.h proof/bitvector_proof.cpp proof/bitvector_proof.h + proof/clausal_bitvector_proof.cpp + proof/clausal_bitvector_proof.h proof/clause_id.h proof/cnf_proof.cpp proof/cnf_proof.h diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index ba3533cc3..90c0c9b30 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -18,10 +18,13 @@ #include "options/proof_options.h" #include "proof/proof_output_channel.h" #include "proof/theory_proof.h" +#include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" namespace CVC4 { + +namespace proof { BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) : TheoryProof(bv, proofEngine), @@ -118,13 +121,6 @@ std::string BitVectorProof::getBBTermName(Expr expr) return os.str(); } -void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf) -{ - Assert(d_cnfProof == nullptr); - d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); -} - void BitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) @@ -709,6 +705,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) } } +theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } + const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof() { return &d_atomsInBitblastingProof; @@ -774,4 +772,6 @@ void BitVectorProof::printRewriteProof(std::ostream& os, os << ")"; } +} // namespace proof + } // namespace CVC4 diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 466efa6a7..4b897a6c6 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -24,14 +24,28 @@ #include <unordered_map> #include <unordered_set> #include <vector> + #include "expr/expr.h" #include "proof/cnf_proof.h" #include "proof/theory_proof.h" -#include "theory/bv/bitblast/bitblaster.h" +#include "prop/sat_solver.h" #include "theory/bv/theory_bv.h" +// Since TBitblaster and BitVectorProof are cyclically dependent, we need this +// forward declaration +namespace CVC4 { +namespace theory { +namespace bv { +template <class T> +class TBitblaster; +} +} // namespace theory +} // namespace CVC4 + namespace CVC4 { +namespace proof { + typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId; @@ -118,6 +132,8 @@ class BitVectorProof : public TheoryProof */ std::unique_ptr<CnfProof> d_cnfProof; + theory::TheoryId getTheoryId() override; + public: void printOwnedTerm(Expr term, std::ostream& os, @@ -132,6 +148,28 @@ class BitVectorProof : public TheoryProof virtual void calculateAtomsInBitblastingProof() = 0; /** + * Prints out a declaration of the bit-blasting, and the subsequent + * conversion of the result to CNF + * + * @param os the stream to print to + * @param paren a stream that will be placed at the back of the proof (for + * closing parens) + * @param letMap The let-map, which contains information about LFSC + * identifiers and the values they reference. + */ + virtual void printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) = 0; + + /** + * Prints a proof of the empty clause. + * + * @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; + + /** * Read the d_atomsInBitblastingProof member. * See its documentation. */ @@ -153,13 +191,41 @@ class BitVectorProof : public TheoryProof /** * This must be done before registering any terms or atoms, since the CNF * proof must reflect the result of bitblasting those + * + * Feeds the SAT solver's true and false variables into the CNF stream. */ - virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); + virtual void initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) = 0; CnfProof* getCnfProof() { return d_cnfProof.get(); } + /** + * Attaches this BVP to the given SAT solver, initializing a SAT proof. + * + * This must be invoked before `initCnfProof` because a SAT proof must already + * exist to initialize a CNF proof. + */ + virtual void attachToSatSolver(prop::SatSolver& sat_solver) = 0; + void setBitblaster(theory::bv::TBitblaster<Node>* bb); + /** + * Kind of a mess. Used for resulution-based BVP's, where in eager mode this + * must be invoked before printing a proof of the empty clause. In lazy mode + * the behavior and purpose are both highly unclear. + * + * This exists as a virtual method of BitVectorProof, and not + * ResolutionBitVectorProof, because the machinery that invokes it is + * high-level enough that it doesn't know the difference between clausal and + * resolution proofs. + * + * TODO(aozdemir) figure out what is going on and clean this up + * Issue: https://github.com/CVC4/CVC4/issues/2789 + */ + virtual void finalizeConflicts(std::vector<Expr>& conflicts){}; + private: ExprToString d_exprToVariableName; @@ -206,6 +272,8 @@ class BitVectorProof : public TheoryProof const Node& n2) override; }; +} // namespace proof + }/* CVC4 namespace */ #endif /* __CVC4__BITVECTOR__PROOF_H */ diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp new file mode 100644 index 000000000..bb875d1d8 --- /dev/null +++ b/src/proof/clausal_bitvector_proof.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file clausal_bitvector_proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** 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 Bitvector proof using the DRAT proof format + ** + ** Contains DRAT-specific printing logic. + **/ + +#include "cvc4_private.h" + +#include <algorithm> +#include <iterator> +#include <set> +#include "options/bv_options.h" +#include "proof/clausal_bitvector_proof.h" +#include "proof/drat/drat_proof.h" +#include "proof/lfsc_proof_printer.h" +#include "theory/bv/theory_bv.h" + +namespace CVC4 { + +namespace proof { + +ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof() +{ +} + +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) +{ + d_usedClauses.emplace_back( + id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause))); +}; + +void ClausalBitVectorProof::calculateAtomsInBitblastingProof() +{ + if (Debug.isOn("bv::clausal")) + { + std::string serializedDratProof = d_binaryDratProof.str(); + Debug("bv::clausal") << "binary DRAT proof byte count: " + << serializedDratProof.size() << std::endl; + Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl; + drat::DratProof dratProof = + drat::DratProof::fromBinary(serializedDratProof); + + Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl; + dratProof.outputAsText(Debug("bv::clausal")); + } + Unimplemented(); +} + +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) +{ + Unimplemented(); +} + +void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os, + std::ostream& paren) +{ + Unimplemented(); +} + +} // namespace proof + +}; // namespace CVC4 diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h new file mode 100644 index 000000000..85e409e0d --- /dev/null +++ b/src/proof/clausal_bitvector_proof.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \file clausal_bitvector_proof.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** 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 Bitvector proof for clausal (DRAT/LRAT) formats + ** + ** An internal string stream is hooked up to CryptoMiniSat, which spits out a + ** binary DRAT proof. Depending on which kind of proof we're going to turn + ** that into, we process it in different ways. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H +#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H + +#include <iostream> +#include <sstream> +#include <unordered_map> + +#include "expr/expr.h" +#include "proof/bitvector_proof.h" +#include "proof/drat/drat_proof.h" +#include "proof/lrat/lrat_proof.h" +#include "proof/theory_proof.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_types.h" +#include "theory/bv/theory_bv.h" + +namespace CVC4 { + +namespace proof { + +class ClausalBitVectorProof : public BitVectorProof +{ + public: + ClausalBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine); + + ~ClausalBitVectorProof() = default; + + void attachToSatSolver(prop::SatSolver& sat_solver) override; + + void initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) override; + + std::ostream& getDratOstream() { return d_binaryDratProof; } + + void registerUsedClause(ClauseId id, prop::SatClause& clause); + + void calculateAtomsInBitblastingProof() override; + + protected: + // A list of all clauses and their ids which are passed into the SAT solver + std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>> + d_usedClauses; + // Stores the proof recieved from the SAT solver. + std::ostringstream d_binaryDratProof; +}; + +/** + * A representation of a clausal proof of a bitvector problem's UNSAT nature + */ +class LfscClausalBitVectorProof : public ClausalBitVectorProof +{ + public: + LfscClausalBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : ClausalBitVectorProof(bv, proofEngine) + { + // That's all! + } + + void printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) override; + void printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; +}; + +} // namespace proof + +} // namespace CVC4 + +#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */ diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 016198735..4e8d20162 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -105,6 +105,30 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseDefinition(clause, current_expr); } +void CnfProof::registerTrueUnitClause(ClauseId clauseId) +{ + Node trueNode = NodeManager::currentNM()->mkConst<bool>(true); + pushCurrentAssertion(trueNode); + pushCurrentDefinition(trueNode); + registerConvertedClause(clauseId); + popCurrentAssertion(); + popCurrentDefinition(); + d_cnfStream->ensureLiteral(trueNode); + d_trueUnitClause = clauseId; +} + +void CnfProof::registerFalseUnitClause(ClauseId clauseId) +{ + Node falseNode = NodeManager::currentNM()->mkConst<bool>(false).notNode(); + pushCurrentAssertion(falseNode); + pushCurrentDefinition(falseNode); + registerConvertedClause(clauseId); + popCurrentAssertion(); + popCurrentDefinition(); + d_cnfStream->ensureLiteral(falseNode); + d_falseUnitClause = clauseId; +} + void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { Debug("proof:cnf") << "CnfProof::setClauseAssertion " << clause << " assertion " << expr << std::endl; diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 32833d9a1..78ddeebd0 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -78,6 +78,11 @@ protected: ClauseIdSet d_explanations; + // The clause ID of the unit clause defining the true SAT literal. + ClauseId d_trueUnitClause; + // The clause ID of the unit clause defining the false SAT literal. + ClauseId d_falseUnitClause; + bool isDefinition(Node node); Node getDefinitionForClause(ClauseId clause); @@ -110,6 +115,14 @@ public: // already in CNF void registerConvertedClause(ClauseId clause, bool explanation=false); + // The CNF proof has a special relationship to true and false. + // In particular, it need to know the identity of clauses defining + // canonical true and false literals in the underlying SAT solver. + void registerTrueUnitClause(ClauseId clauseId); + void registerFalseUnitClause(ClauseId clauseId); + inline ClauseId getTrueUnitClause() { return d_trueUnitClause; }; + inline ClauseId getFalseUnitClause() { return d_falseUnitClause; }; + /** Clause is one of the clauses defining the node expression*/ void setClauseDefinition(ClauseId clause, Node node); diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index 667d630f8..1db673949 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -26,6 +26,7 @@ #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" +#include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_rewrite_rules.h" @@ -54,32 +55,22 @@ void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true)); } -theory::TheoryId ResolutionBitVectorProof::getTheoryId() +void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) { - return theory::THEORY_BV; + Assert(d_resolutionProof != NULL); + Assert(d_cnfProof == nullptr); + d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); + + d_cnfProof->registerTrueUnitClause(d_resolutionProof->getTrueUnit()); + d_cnfProof->registerFalseUnitClause(d_resolutionProof->getFalseUnit()); } -void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf) +void ResolutionBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver) { - Assert(d_resolutionProof != NULL); - BitVectorProof::initCnfProof(cnfStream, cnf); - - // true and false have to be setup in a special way - Node true_node = NodeManager::currentNM()->mkConst<bool>(true); - Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode(); - - d_cnfProof->pushCurrentAssertion(true_node); - d_cnfProof->pushCurrentDefinition(true_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); - - d_cnfProof->pushCurrentAssertion(false_node); - d_cnfProof->pushCurrentDefinition(false_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); + sat_solver.setResolutionProofLog(this); } BVSatProof* ResolutionBitVectorProof::getSatProof() @@ -258,13 +249,15 @@ void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) } } -void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) +void LfscResolutionBitVectorProof::printTheoryLemmaProof( + std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) { - Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" - << std::endl; + Debug("pf::bv") + << "(pf::bv) LfscResolutionBitVectorProof::printTheoryLemmaProof called" + << std::endl; Expr conflict = utils::mkSortedExpr(kind::OR, lemma); Debug("pf::bv") << "\tconflict = " << conflict << std::endl; @@ -467,7 +460,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, } } -void LFSCBitVectorProof::calculateAtomsInBitblastingProof() +void LfscResolutionBitVectorProof::calculateAtomsInBitblastingProof() { // Collect the input clauses used IdToSatClause used_lemmas; @@ -477,9 +470,9 @@ void LFSCBitVectorProof::calculateAtomsInBitblastingProof() Assert(used_lemmas.empty()); } -void LFSCBitVectorProof::printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) +void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) { // print mapping between theory atoms and internal SAT variables os << std::endl << ";; BB atom mapping\n" << std::endl; @@ -517,6 +510,16 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren); } -} /* namespace proof */ +void LfscResolutionBitVectorProof::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"); + proof::LFSCProofPrinter::printResolutionEmptyClause( + d_resolutionProof.get(), os, paren); +} + +} // namespace proof } /* namespace CVC4 */ diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index ccb288f6e..6c2ae589f 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -24,32 +24,16 @@ #include "context/context.h" #include "expr/expr.h" #include "proof/bitvector_proof.h" +#include "proof/sat_proof.h" #include "proof/theory_proof.h" #include "prop/bvminisat/core/Solver.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_types.h" +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" namespace CVC4 { -namespace theory { -namespace bv { -class TheoryBV; -template <class T> -class TBitblaster; -} // namespace bv -} // namespace theory - -// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream -// header cycle and remove this. -namespace prop { -class CnfStream; -} - -} /* namespace CVC4 */ - - -namespace CVC4 { - -template <class Solver> -class TSatProof; typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof; namespace proof { @@ -76,13 +60,7 @@ class ResolutionBitVectorProof : public BitVectorProof BVSatProof* getSatProof(); - /** - * Kind of a mess. - * In eager mode this must be invoked before printing a proof of the empty - * clause. In lazy mode the behavior is ??? - * TODO(aozdemir) clean this up. - */ - void finalizeConflicts(std::vector<Expr>& conflicts); + void finalizeConflicts(std::vector<Expr>& conflicts) override; void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); @@ -91,13 +69,14 @@ class ResolutionBitVectorProof : public BitVectorProof void markAssumptionConflict() { d_isAssumptionConflict = true; } bool isAssumptionConflict() const { return d_isAssumptionConflict; } - virtual void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) = 0; - - void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override; + void initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf, + prop::SatVariable trueVar, + prop::SatVariable falseVar) override; protected: + void attachToSatSolver(prop::SatSolver& sat_solver) override; + context::Context d_fakeContext; // The CNF formula that results from bit-blasting will need a proof. @@ -106,13 +85,13 @@ class ResolutionBitVectorProof : public BitVectorProof bool d_isAssumptionConflict; - theory::TheoryId getTheoryId() override; }; -class LFSCBitVectorProof : public ResolutionBitVectorProof +class LfscResolutionBitVectorProof : public ResolutionBitVectorProof { public: - LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) : ResolutionBitVectorProof(bv, proofEngine) { } @@ -120,9 +99,10 @@ class LFSCBitVectorProof : public ResolutionBitVectorProof std::ostream& os, std::ostream& paren, const ProofLetMap& map) override; - void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) override; + void printBBDeclarationAndCnf(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; void calculateAtomsInBitblastingProof() override; }; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index ee06fbfa0..fe9acfef3 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -22,6 +22,7 @@ #include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" +#include "proof/clausal_bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" @@ -46,7 +47,7 @@ namespace CVC4 { -using proof::LFSCBitVectorProof; +using proof::LfscResolutionBitVectorProof; using proof::ResolutionBitVectorProof; unsigned CVC4::ProofLetCount::counter = 0; @@ -80,9 +81,20 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } if (id == theory::THEORY_BV) { - auto bv_theory = static_cast<theory::bv::TheoryBV*>(th); - ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this); - d_theoryProofTable[id] = bvp; + auto thBv = static_cast<theory::bv::TheoryBV*>(th); + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT) + { + proof::BitVectorProof* bvp = + new proof::LfscClausalBitVectorProof(thBv, this); + d_theoryProofTable[id] = bvp; + } + else + { + proof::BitVectorProof* bvp = + new proof::LfscResolutionBitVectorProof(thBv, this); + d_theoryProofTable[id] = bvp; + } return; } @@ -105,10 +117,11 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { if (th) { theory::TheoryId id = th->getId(); if (id == theory::THEORY_BV) { + theory::bv::TheoryBV* bv_th = static_cast<theory::bv::TheoryBV*>(th); Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); - ResolutionBitVectorProof* bvp = - (ResolutionBitVectorProof*)d_theoryProofTable[id]; - ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp); + proof::BitVectorProof* bvp = + static_cast<proof::BitVectorProof*>(d_theoryProofTable[id]); + bv_th->setProofLog(bvp); return; } } @@ -533,9 +546,8 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std } } - ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof(); + proof::BitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); - // bv->printResolutionProof(os, paren, letMap); } void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, @@ -550,7 +562,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } // finalizeBvConflicts(lemmas, os, paren, map); - ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map); + ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 55710092b..57ef8ef30 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } -void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp) +void BVMinisatSatSolver::setResolutionProofLog( + proof::ResolutionBitVectorProof* bvp) { d_minisat->setProofLog( bvp ); } diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 16489b172..efb90a3f0 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -119,7 +119,7 @@ public: void popAssumption() override; - void setProofLog(proof::ResolutionBitVectorProof* bvp) override; + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override; private: /* Disable the default constructor. */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index cdb850ce2..84c315547 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -79,19 +79,22 @@ void CnfStream::assertClause(TNode node, SatClause& c) { } } - PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node);); + if (PROOF_ON() && d_cnfProof) + { + d_cnfProof->pushCurrentDefinition(node); + } ClauseId clause_id = d_satSolver->addClause(c, d_removable); if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added) - PROOF - ( - if (d_cnfProof) { - Assert (clause_id != ClauseIdError); - d_cnfProof->registerConvertedClause(clause_id); - d_cnfProof->popCurrentDefinition(); - } - ); + if (PROOF_ON() && d_cnfProof) + { + if (clause_id != ClauseIdError) + { + d_cnfProof->registerConvertedClause(clause_id); + } + d_cnfProof->popCurrentDefinition(); + }; } void CnfStream::assertClause(TNode node, SatLiteral a) { diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index df5a20791..c04fb8b56 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -62,10 +62,11 @@ void toInternalClause(SatClause& clause, CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, const std::string& name) -: d_solver(new CMSat::SATSolver()) -, d_numVariables(0) -, d_okay(true) -, d_statistics(registry, name) + : d_solver(new CMSat::SATSolver()), + d_bvp(nullptr), + d_numVariables(0), + d_okay(true), + d_statistics(registry, name) { d_true = newVar(); d_false = newVar(); @@ -117,9 +118,17 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ std::vector<CMSat::Lit> internal_clause; toInternalClause(clause, internal_clause); - bool res = d_solver->add_clause(internal_clause); - d_okay &= res; - return ClauseIdError; + bool nowOkay = d_solver->add_clause(internal_clause); + ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId()); + + THEORY_PROOF( + // If this clause results in a conflict, then `nowOkay` may be false, but + // we still need to register this clause as used. Thus, we look at + // `d_okay` instead + if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); }) + + d_okay &= nowOkay; + return freshId; } bool CryptoMinisatSolver::ok() const { @@ -193,6 +202,12 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const { return -1; } +void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp) +{ + d_bvp = bvp; + d_solver->set_drat(&bvp->getDratOstream(), false); +} + // Satistics for CryptoMinisatSolver CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry, diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index c5345cb86..17cc1568c 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -21,6 +21,7 @@ #ifdef CVC4_USE_CRYPTOMINISAT +#include "proof/clausal_bitvector_proof.h" #include "prop/sat_solver.h" // Cryptominisat has name clashes with the other Minisat implementations since @@ -39,6 +40,7 @@ class CryptoMinisatSolver : public SatSolver { private: std::unique_ptr<CMSat::SATSolver> d_solver; + proof::ClausalBitVectorProof* d_bvp; unsigned d_numVariables; bool d_okay; SatVariable d_true; @@ -71,6 +73,7 @@ public: SatValue modelValue(SatLiteral l) override; unsigned getAssertionLevel() const override; + void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override; class Statistics { public: diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 49064c20f..70e46eceb 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -26,7 +26,6 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" -#include "proof/resolution_bitvector_proof.h" #include "proof/clause_id.h" #include "prop/sat_solver_types.h" #include "prop/bv_sat_solver_notify.h" @@ -34,6 +33,11 @@ namespace CVC4 { +namespace proof { +class ClausalBitVectorProof; +class ResolutionBitVectorProof; +} // namespace proof + namespace prop { class TheoryProxy; @@ -97,7 +101,9 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} + virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {} + + virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {} };/* class SatSolver */ diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 73b4d19c7..b1fc084ed 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -24,6 +24,7 @@ #include <vector> #include "expr/node.h" +#include "proof/bitvector_proof.h" #include "prop/bv_sat_solver_notify.h" #include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" @@ -31,6 +32,7 @@ #include "theory/valuation.h" #include "util/resource_manager.h" + namespace CVC4 { namespace theory { namespace bv { @@ -59,6 +61,10 @@ class TBitblaster // caches and mappings TermDefMap d_termCache; ModelCache d_modelCache; + // sat solver used for bitblasting and associated CnfStream + std::unique_ptr<context::Context> d_nullContext; + std::unique_ptr<prop::CnfStream> d_cnfStream; + proof::BitVectorProof* d_bvp; void initAtomBBStrategies(); void initTermBBStrategies(); @@ -69,6 +75,8 @@ class TBitblaster TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; + virtual prop::SatSolver* getSatSolver() = 0; + public: TBitblaster(); @@ -83,6 +91,8 @@ class TBitblaster bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; virtual void storeBBTerm(TNode term, const Bits& bits); + void setProofLog(proof::BitVectorProof* bvp); + /** * Return a constant representing the value of a in the model. * If fullModel is true set unconstrained bits to 0. If not return @@ -171,7 +181,12 @@ void TBitblaster<T>::initTermBBStrategies() } template <class T> -TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache() +TBitblaster<T>::TBitblaster() + : d_termCache(), + d_modelCache(), + d_nullContext(new context::Context()), + d_cnfStream(), + d_bvp(nullptr) { initAtomBBStrategies(); initTermBBStrategies(); @@ -202,6 +217,20 @@ void TBitblaster<T>::invalidateModelCache() } template <class T> +void TBitblaster<T>::setProofLog(proof::BitVectorProof* bvp) +{ + if (THEORY_PROOF_ON()) + { + d_bvp = bvp; + prop::SatSolver* satSolver = getSatSolver(); + bvp->attachToSatSolver(*satSolver); + prop::SatVariable t = satSolver->trueVar(); + prop::SatVariable f = satSolver->falseVar(); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f); + } +} + +template <class T> Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) { if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node]; diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 019918c2f..1e557bb64 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -32,11 +32,8 @@ namespace bv { EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) : TBitblaster<Node>(), d_context(c), - d_nullContext(new context::Context()), d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), - d_cnfStream(), - d_bvp(nullptr), d_bv(theory_bv), d_bbAtoms(), d_variables(), @@ -268,13 +265,6 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void EagerBitblaster::setResolutionProofLog( - proof::ResolutionBitVectorProof* bvp) -{ - THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());) -} - bool EagerBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 3299ffc54..1c183b509 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -55,19 +55,13 @@ class EagerBitblaster : public TBitblaster<Node> bool solve(); bool solve(const std::vector<Node>& assumptions); bool collectModelInfo(TheoryModel* m, bool fullModel); - void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); private: context::Context* d_context; - std::unique_ptr<context::Context> d_nullContext; typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - // sat solver used for bitblasting and associated CnfStream std::unique_ptr<prop::SatSolver> d_satSolver; std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar; - std::unique_ptr<prop::CnfStream> d_cnfStream; - - BitVectorProof* d_bvp; TheoryBV* d_bv; TNodeSet d_bbAtoms; @@ -77,6 +71,7 @@ class EagerBitblaster : public TBitblaster<Node> std::unique_ptr<MinisatEmptyNotify> d_notify; Node getModelFromSatSolver(TNode a, bool fullModel) override; + prop::SatSolver* getSatSolver() override { return d_satSolver.get(); } bool isSharedTerm(TNode node); }; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 529f0373b..2a47c2315 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -64,10 +64,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bool emptyNotify) : TBitblaster<Node>(), d_bv(bv), - d_bvp(nullptr), d_ctx(c), d_nullRegistrar(new prop::NullRegistrar()), - d_nullContext(new context::Context()), d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)), d_explanations(new (true) ExplanationMap(c)), d_variables(), @@ -566,11 +564,12 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp) +void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp) { - d_bvp = bvp; - d_satSolver->setProofLog( bvp ); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); + THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver); + prop::SatVariable t = d_satSolver->trueVar(); + prop::SatVariable f = d_satSolver->falseVar(); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f)); } void TLazyBitblaster::clearSolver() { diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 1195d3590..9af74d8db 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -77,7 +77,7 @@ class TLazyBitblaster : public TBitblaster<Node> * constants to equivalence classes that don't already have them */ bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(proof::ResolutionBitVectorProof* bvp); + void setProofLog(proof::BitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -126,15 +126,11 @@ class TLazyBitblaster : public TBitblaster<Node> }; TheoryBV* d_bv; - proof::ResolutionBitVectorProof* d_bvp; context::Context* d_ctx; std::unique_ptr<prop::NullRegistrar> d_nullRegistrar; - std::unique_ptr<context::Context> d_nullContext; - // sat solver used for bitblasting and associated CnfStream std::unique_ptr<prop::BVSatSolverInterface> d_satSolver; std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify; - std::unique_ptr<prop::CnfStream> d_cnfStream; AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms @@ -155,6 +151,7 @@ class TLazyBitblaster : public TBitblaster<Node> void addAtom(TNode atom); bool hasValue(TNode a); Node getModelFromSatSolver(TNode a, bool fullModel) override; + prop::SatSolver* getSatSolver() override { return d_satSolver.get(); } class Statistics { diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 119195c4a..336529dfd 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -56,7 +56,7 @@ void EagerBitblastSolver::initialize() { } else { d_bitblaster.reset(new EagerBitblaster(d_bv, d_context)); THEORY_PROOF(if (d_bvp) { - d_bitblaster->setResolutionProofLog(d_bvp); + d_bitblaster->setProofLog(d_bvp); d_bvp->setBitblaster(d_bitblaster.get()); }); } @@ -127,8 +127,7 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) return d_bitblaster->collectModelInfo(m, fullModel); } -void EagerBitblastSolver::setResolutionProofLog( - proof::ResolutionBitVectorProof* bvp) +void EagerBitblastSolver::setProofLog(proof::BitVectorProof* bvp) { d_bvp = bvp; } diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 7f688b3ae..0b518ca4a 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -48,7 +48,7 @@ class EagerBitblastSolver { bool isInitialized(); void initialize(); bool collectModelInfo(theory::TheoryModel* m, bool fullModel); - void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); + void setProofLog(proof::BitVectorProof* bvp); private: context::CDHashSet<Node, NodeHashFunction> d_assertionSet; @@ -61,7 +61,7 @@ class EagerBitblastSolver { bool d_useAig; TheoryBV* d_bv; - proof::ResolutionBitVectorProof* d_bvp; + proof::BitVectorProof* d_bvp; }; // class EagerBitblastSolver } // namespace bv diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 31c542e0b..e2b649841 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -26,7 +26,7 @@ namespace CVC4 { namespace proof { -class ResolutionBitVectorProof; +class BitVectorProof; } namespace theory { @@ -93,7 +93,7 @@ class SubtheorySolver { return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} + virtual void setProofLog(proof::BitVectorProof* bvp) {} AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ff9dd52c2..ceb02af40 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -276,7 +276,7 @@ void BitblastSolver::setConflict(TNode conflict) { d_bv->setConflict(final_conflict); } -void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* bvp) +void BitblastSolver::setProofLog(proof::BitVectorProof* bvp) { d_bitblaster->setProofLog( bvp ); bvp->setBitblaster(d_bitblaster.get()); diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index aa2c90c43..e028dbbdc 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -79,7 +79,7 @@ public: void bitblastQueue(); void setAbstraction(AbstractionModule* module); uint64_t computeAtomWeight(TNode atom); - void setProofLog(proof::ResolutionBitVectorProof* bvp) override; + void setProofLog(proof::BitVectorProof* bvp) override; }; } /* namespace CVC4::theory::bv */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 949a3d738..04a6cf52c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -986,10 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector return changed; } -void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) +void TheoryBV::setProofLog(proof::BitVectorProof* bvp) { if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ - d_eagerSolver->setResolutionProofLog(bvp); + d_eagerSolver->setProofLog(bvp); }else{ for( unsigned i=0; i< d_subtheories.size(); i++ ){ d_subtheories[i]->setProofLog( bvp ); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index afa9f4b4f..3d151cfb1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -31,6 +31,14 @@ #include "util/hash.h" #include "util/statistics_registry.h" +// Forward declarations, needed because the BV theory and the BV Proof classes +// are cyclically dependent +namespace CVC4 { +namespace proof { +class BitVectorProof; +} +} // namespace CVC4 + namespace CVC4 { namespace theory { namespace bv { @@ -104,7 +112,7 @@ public: bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); + void setProofLog(proof::BitVectorProof* bvp); private: |