From: Alex Ozdemir Date: Mon, 3 Dec 2018 19:56:47 +0000 (-0800) Subject: Bit vector proof superclass (#2599) X-Git-Tag: cvc5-1.0.0~4339 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa0a875dfd40bd9dfa810238327db51498b74677;p=cvc5.git Bit vector proof superclass (#2599) * Split BitvectorProof into a sub/superclass The superclass contains general printing knowledge. The subclass contains CNF or Resolution-specific knowledge. * Renames & code moves * Nits cleaned in prep for PR * Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should be stored in `BitVectorProof`. * Unique pointers, comments, and code movement. Adjusted the distribution of code between BVP and RBVP. Notably, put the CNF proof in BVP because it isn't resolution-specific. Added comments to the headers of both files -- mostly BVP. Changed two owned pointers into unique_ptr. BVP's pointer to a CNF proof RBVP's pointer to a resolution proof BVP: `BitVectorProof` RBVP: `ResolutionBitVectorProof` * clang-format * Undo manual copyright modification * s/superclass/base class/ Co-Authored-By: alex-ozdemir * make LFSCBitVectorProof::printOwnedSort public * Andres's Comments Mostly cleaning up (or trying to clean up) includes. * Cleaned up one header cycle However, this only allowed me to move the forward-decl, not eliminate it, because there were actually two underlying include cycles that the forward-decl solved. * Added single _s to header gaurds * Fix Class name in debug output Credits to Andres Co-Authored-By: alex-ozdemir * Reordered methods in BitVectorProof per original ordering --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9a1cfe9e7..9e93bd953 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -142,6 +142,8 @@ libcvc4_add_sources( proof/proof_output_channel.h proof/proof_utils.cpp proof/proof_utils.h + proof/resolution_bitvector_proof.cpp + proof/resolution_bitvector_proof.h proof/sat_proof.h proof/sat_proof_implementation.h proof/simplify_boolean_node.cpp @@ -202,6 +204,7 @@ libcvc4_add_sources( prop/sat_solver.h prop/sat_solver_factory.cpp prop/sat_solver_factory.h + prop/bv_sat_solver_notify.h prop/sat_solver_types.h prop/theory_proxy.cpp prop/theory_proxy.h diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 8f001ffa1..c9e98d170 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -9,31 +9,19 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ + ** Contains implementions (e.g. code for printing bitblasting bindings that is + ** common to all kinds of bitvector proofs. + **/ #include "proof/bitvector_proof.h" #include "options/bv_options.h" #include "options/proof_options.h" -#include "proof/array_proof.h" -#include "proof/clause_id.h" -#include "proof/lfsc_proof_printer.h" #include "proof/proof_output_channel.h" -#include "proof/proof_utils.h" -#include "proof/sat_proof_implementation.h" -#include "prop/bvminisat/bvminisat.h" +#include "proof/theory_proof.h" #include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/theory_bv_rewrite_rules.h" - -using namespace CVC4::theory; -using namespace CVC4::theory::bv; namespace CVC4 { - BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) : TheoryProof(bv, proofEngine), @@ -41,73 +29,44 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, d_seenBBTerms(), d_bbTerms(), d_bbAtoms(), - d_resolutionProof(NULL), - d_cnfProof(NULL), - d_isAssumptionConflict(false), - d_bitblaster(NULL), - d_useConstantLetification(false) {} - -void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { - Assert (d_resolutionProof == NULL); - d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true); -} - -theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } -void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf) { - Assert (d_resolutionProof != NULL); - Assert (d_cnfProof == NULL); - d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb"); - - // true and false have to be setup in a special way - Node true_node = NodeManager::currentNM()->mkConst(true); - Node false_node = NodeManager::currentNM()->mkConst(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(); + d_bitblaster(nullptr), + d_useConstantLetification(false), + d_cnfProof() +{ } -void BitVectorProof::setBitblaster(bv::TBitblaster* bb) { - Assert (d_bitblaster == NULL); +void BitVectorProof::setBitblaster(theory::bv::TBitblaster* bb) +{ + Assert(d_bitblaster == NULL); d_bitblaster = bb; } -BVSatProof* BitVectorProof::getSatProof() { - Assert (d_resolutionProof != NULL); - return d_resolutionProof; -} - -void BitVectorProof::registerTermBB(Expr term) { - Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl; +void BitVectorProof::registerTermBB(Expr term) +{ + Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term + << " )" << std::endl; - if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) - return; + if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return; d_seenBBTerms.insert(term); d_bbTerms.push_back(term); - // If this term gets used in the final proof, we will want to register it. However, - // we don't know this at this point; and when the theory proof engine sees it, if it belongs - // to another theory, it won't register it with this proof. So, we need to tell the - // engine to inform us. + // If this term gets used in the final proof, we will want to register it. + // However, we don't know this at this point; and when the theory proof engine + // sees it, if it belongs to another theory, it won't register it with this + // proof. So, we need to tell the engine to inform us. - if (theory::Theory::theoryOf(term) != theory::THEORY_BV) { - Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl; + if (theory::Theory::theoryOf(term) != theory::THEORY_BV) + { + Debug("pf::bv") << "\tMarking term " << term + << " for future BV registration" << std::endl; d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV); } } void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { - Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl; + Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom + << ", " << atom_bb << " )" << std::endl; Expr def = atom.iffExpr(atom_bb); d_bbAtoms.insert(std::make_pair(atom, def)); @@ -119,7 +78,8 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { } void BitVectorProof::registerTerm(Expr term) { - Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; + Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" + << std::endl; if (options::lfscLetification() && term.isConst()) { if (d_constantLetMap.find(term) == d_constantLetMap.end()) { @@ -131,8 +91,8 @@ void BitVectorProof::registerTerm(Expr term) { d_usedBB.insert(term); - if (Theory::isLeafOf(term, theory::THEORY_BV) && - !term.isConst()) { + if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) + { d_declarations.insert(term); } @@ -147,149 +107,32 @@ void BitVectorProof::registerTerm(Expr term) { } } -std::string BitVectorProof::getBBTermName(Expr expr) { - Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl; +std::string BitVectorProof::getBBTermName(Expr expr) +{ + Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" + << expr.getId() << std::endl; std::ostringstream os; - os << "bt"<< expr.getId(); + os << "bt" << expr.getId(); return os.str(); } -void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TCRef cr) { - d_resolutionProof->startResChain(cr); -} - -void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) { - d_resolutionProof->startResChain(lit); -} - -void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) { - Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl; - - std::vector expr_confl; - for (int i = 0; i < confl.size(); ++i) { - prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); - Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); - Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; - expr_confl.push_back(expr_lit); - } - - Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); - Debug("pf::bv") << "Make conflict for " << conflict << std::endl; - - if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { - Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl; - // This can only happen when we have eager explanations in the bv solver - // if we don't get to propagate p before ~p is already asserted - d_resolutionProof->cancelResChain(); - return; - } - - // we don't need to check for uniqueness in the sat solver then - ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); - d_bbConflictMap[conflict] = clause_id; - d_resolutionProof->endResChain(clause_id); - Debug("pf::bv") << "BitVectorProof::endBVConflict id" < " << conflict << "\n"; - d_isAssumptionConflict = false; -} - -void BitVectorProof::finalizeConflicts(std::vector& conflicts) { - - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - Debug("pf::bv") << "Construct full proof." << std::endl; - d_resolutionProof->constructProof(); - return; - } - - for (unsigned i = 0; i < conflicts.size(); ++i) { - Expr confl = conflicts[i]; - Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; - - // Special case: if the conflict has a (true) or a (not false) in it, it is trivial... - bool ignoreConflict = false; - if ((confl.isConst() && confl.getConst()) || - (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst())) { - ignoreConflict = true; - } else if (confl.getKind() == kind::OR) { - for (unsigned k = 0; k < confl.getNumChildren(); ++k) { - if ((confl[k].isConst() && confl[k].getConst()) || - (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst())) { - ignoreConflict = true; - } - } - } - if (ignoreConflict) { - Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl; - continue; - } - - if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) { - ClauseId id = d_bbConflictMap[confl]; - d_resolutionProof->collectClauses(id); - } else { - // There is no exact match for our conflict, but maybe it is a subset of another conflict - ExprToClauseId::const_iterator it; - bool matchFound = false; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - Expr possibleMatch = it->first; - if (possibleMatch.getKind() != kind::OR) { - // This is a single-node conflict. If this node is in the conflict we're trying to prove, - // we have a match. - for (unsigned k = 0; k < confl.getNumChildren(); ++k) { - if (confl[k] == possibleMatch) { - matchFound = true; - d_resolutionProof->collectClauses(it->second); - break; - } - } - } else { - if (possibleMatch.getNumChildren() > confl.getNumChildren()) - continue; - - unsigned k = 0; - bool matching = true; - for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { - // j is the index in possibleMatch - // k is the index in confl - while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) { - ++k; - } - if (k == confl.getNumChildren()) { - // We couldn't find a match for possibleMatch[j], so not a match - matching = false; - break; - } - } - - if (matching) { - Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl; - d_resolutionProof->collectClauses(it->second); - matchFound = true; - break; - } - } - } - - if (!matchFound) { - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl - << "Dumping existing conflicts:" << std::endl; - - i = 0; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - ++i; - Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; - } - - Unreachable(); - } - } - } +void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf) +{ + Assert(d_cnfProof == nullptr); + d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); } -void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: " - << Theory::theoryOf(term) << std::endl; +void BitVectorProof::printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ + Debug("pf::bv") << std::endl + << "(pf::bv) BitVectorProof::printOwnedTerm( " << term + << " ), theory is: " << theory::Theory::theoryOf(term) + << std::endl; - Assert (Theory::theoryOf(term) == THEORY_BV); + Assert(theory::Theory::theoryOf(term) == theory::THEORY_BV); // peel off eager bit-blasting trick if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) { @@ -380,21 +223,24 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const Proof } } -void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printBitOf(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ Assert (term.getKind() == kind::BITVECTOR_BITOF); unsigned bit = term.getOperator().getConst().bitIndex; Expr var = term[0]; - Debug("pf::bv") << "LFSCBitVectorProof::printBitOf( " << term << " ), " - << "bit = " << bit - << ", var = " << var << std::endl; + Debug("pf::bv") << "BitVectorProof::printBitOf( " << term << " ), " + << "bit = " << bit << ", var = " << var << std::endl; os << "(bitof "; os << d_exprToVariableName[var]; os << " " << bit << ")"; } -void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { +void BitVectorProof::printConstant(Expr term, std::ostream& os) +{ Assert (term.isConst()); os << "(a_bv " << utils::getSize(term) << " "; @@ -413,7 +259,10 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorNary(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ std::string op = utils::toLFSCKindTerm(term); std::ostringstream paren; std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; @@ -431,7 +280,10 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr } } -void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorUnary(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os << " "; @@ -439,7 +291,10 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P os <<")"; } -void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printPredicate(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" "; os << " "; @@ -449,7 +304,10 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof os <<")"; } -void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorParametric(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os <<" "; @@ -477,185 +335,25 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co os <<")"; } -void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { - Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl; +void BitVectorProof::printOwnedSort(Type type, std::ostream& os) +{ + Debug("pf::bv") << std::endl + << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )" + << std::endl; Assert (type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec " << width << ")"; } -void LFSCBitVectorProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { - Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl; - Expr conflict = utils::mkSortedExpr(kind::OR, lemma); - Debug("pf::bv") << "\tconflict = " << conflict << std::endl; - - if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { - std::ostringstream lemma_paren; - for (unsigned i = 0; i < lemma.size(); ++i) { - Expr lit = lemma[i]; - - if (lit.getKind() == kind::NOT) { - os << "(intro_assump_t _ _ _ "; - } else { - os << "(intro_assump_f _ _ _ "; - } - lemma_paren <<")"; - // print corresponding literal in main sat solver - ProofManager* pm = ProofManager::currentPM(); - CnfProof* cnf = pm->getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<first; - - if (possibleMatch.getKind() != kind::OR) { - // This is a single-node conflict. If this node is in the conflict we're trying to prove, - // we have a match. - matching = false; - - for (unsigned k = 0; k < conflict.getNumChildren(); ++k) { - if (conflict[k] == possibleMatch) { - matching = true; - break; - } - } - } else { - if (possibleMatch.getNumChildren() > conflict.getNumChildren()) - continue; - - unsigned k = 0; - - matching = true; - for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { - // j is the index in possibleMatch - // k is the index in conflict - while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) { - ++k; - } - if (k == conflict.getNumChildren()) { - // We couldn't find a match for possibleMatch[j], so not a match - matching = false; - break; - } - } - } - - if (matching) { - Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl; - // The rest is just a copy of the usual handling, if a precise match is found. - // We only use the literals that appear in the matching conflict, though, and not in the - // original lemma - as these may not have even been bit blasted! - std::ostringstream lemma_paren; - - if (possibleMatch.getKind() == kind::OR) { - for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) { - Expr lit = possibleMatch[i]; - - if (lit.getKind() == kind::NOT) { - os << "(intro_assump_t _ _ _ "; - } else { - os << "(intro_assump_f _ _ _ "; - } - lemma_paren <<")"; - // print corresponding literal in main sat solver - ProofManager* pm = ProofManager::currentPM(); - CnfProof* cnf = pm->getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<second; - proof::LFSCProofPrinter::printAssumptionsResolution( - d_resolutionProof, lemma_id, os, lemma_paren); - os <first << std::endl; - } - - Unreachable(); - } -} - -void LFSCBitVectorProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printSortDeclarations(std::ostream& os, + std::ostream& paren) +{ // Nothing to do here at this point. } -void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printTermDeclarations(std::ostream& os, + std::ostream& paren) +{ ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { @@ -671,7 +369,9 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p } } -void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printDeferredDeclarations(std::ostream& os, + std::ostream& paren) +{ if (options::lfscLetification()) { os << std::endl << ";; BV const letification\n" << std::endl; std::map::const_iterator it; @@ -694,7 +394,10 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea } } -void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { +void BitVectorProof::printAliasingDeclarations(std::ostream& os, + std::ostream& paren, + const ProofLetMap& globalLetMap) +{ // Print "trust" statements to bind complex bv variables to their associated terms ExprToString::const_iterator it = d_assignedAliases.begin(); @@ -720,13 +423,15 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea os << "\n"; } -void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { +void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os) +{ // TODO: once we have the operator elimination rules remove those that we // eliminated Assert (term.getType().isBitVector()); Kind kind = term.getKind(); - if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) { + if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) + { // A term is a leaf if it has no children, or if it belongs to another theory os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term]; os << " _)"; @@ -857,12 +562,14 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { return; } - default: - Unreachable("LFSCBitVectorProof Unknown operator"); + default: Unreachable("BitVectorProof Unknown operator"); } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { +void BitVectorProof::printAtomBitblasting(Expr atom, + std::ostream& os, + bool swap) +{ Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -888,12 +595,12 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool return; } - default: - Unreachable("LFSCBitVectorProof Unknown atom kind"); + default: Unreachable("BitVectorProof Unknown atom kind"); } } -void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { +void BitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) +{ Assert(atom.getKind() == kind::EQUAL); os << "(bv_bbl_=_false"; @@ -907,10 +614,13 @@ void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os os << ")"; } -void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) +{ // bit-blast terms { - Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl; + Debug("pf::bv") + << "BitVectorProof::printBitblasting: the bitblasted terms are: " + << std::endl; std::vector::const_iterator it = d_bbTerms.begin(); std::vector::const_iterator end = d_bbTerms.end(); @@ -999,52 +709,13 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) } } -void LFSCBitVectorProof::calculateAtomsInBitblastingProof() { - // Collect the input clauses used - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); - d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); - Assert(used_lemmas.empty()); -} - -const std::set* LFSCBitVectorProof::getAtomsInBitblastingProof() { +const std::set* BitVectorProof::getAtomsInBitblastingProof() +{ return &d_atomsInBitblastingProof; } -void LFSCBitVectorProof::printResolutionProof(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; - - std::set::iterator atomIt; - Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; - for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) { - Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; - } - Debug("pf::bv") << std::endl; - - // first print bit-blasting - printBitblasting(os, paren); - - // print CNF conversion proof for bit-blasted facts - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); - - d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); - os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; - for (IdToSatClause::iterator it = used_inputs.begin(); - it != used_inputs.end(); ++it) { - d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); - } - - os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; - proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren); -} - -std::string LFSCBitVectorProof::assignAlias(Expr expr) { +std::string BitVectorProof::assignAlias(Expr expr) +{ Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); std::stringstream ss; @@ -1054,11 +725,14 @@ std::string LFSCBitVectorProof::assignAlias(Expr expr) { return ss.str(); } -bool LFSCBitVectorProof::hasAlias(Expr expr) { +bool BitVectorProof::hasAlias(Expr expr) +{ return d_assignedAliases.find(expr) != d_assignedAliases.end(); } -void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { +void BitVectorProof::printConstantDisequalityProof( + std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap) +{ Assert (c1.isConst()); Assert (c2.isConst()); Assert (utils::getSize(c1) == utils::getSize(c2)); @@ -1088,7 +762,10 @@ void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1 os << ")"; } -void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) { +void BitVectorProof::printRewriteProof(std::ostream& os, + const Node& n1, + const Node& n2) +{ ProofLetMap emptyMap; os << "(rr_bv_default "; d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap); @@ -1097,4 +774,4 @@ void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, con os << ")"; } -} /* namespace CVC4 */ +} // namespace CVC4 diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 63f1cdf63..466efa6a7 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -9,118 +9,166 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Bitvector proof + ** \brief Bitvector proof base class ** - ** Bitvector proof + ** Contains code (e.g. proof printing code) which is common to all bitvector + *proofs. **/ #include "cvc4_private.h" -#ifndef __CVC4__BITVECTOR__PROOF_H -#define __CVC4__BITVECTOR__PROOF_H +#ifndef __CVC4__BITVECTOR_PROOF_H +#define __CVC4__BITVECTOR_PROOF_H -#include #include -#include #include #include #include - #include "expr/expr.h" +#include "proof/cnf_proof.h" #include "proof/theory_proof.h" -#include "prop/bvminisat/core/Solver.h" - +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" namespace CVC4 { -namespace prop { -class CnfStream; -} /* namespace CVC4::prop */ - -namespace theory { -namespace bv { -class TheoryBV; -template class TBitblaster; -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ - -class CnfProof; -} /* namespace CVC4 */ - -namespace CVC4 { - -template class TSatProof; -typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; - typedef std::unordered_set ExprSet; typedef std::unordered_map ExprToClauseId; typedef std::unordered_map ExprToId; typedef std::unordered_map ExprToExpr; typedef std::unordered_map ExprToString; -class BitVectorProof : public TheoryProof { -protected: +/** + * A bitvector proof is best understood as having + * + * 1. A declaration of a "bitblasted formulas" -- boolean formulas + * that are each translations of a BV-literal (a comparison between BVs). + * + * (and a proof that each "bitblasted formula" is implied by the + * corresponding BV literal) + * + * 2. A declaration of a cnf formula equisatisfiable to the bitblasted + * formula + * + * (and a proof that each clause is implied by some bitblasted formula) + * + * 3. A proof of UNSAT from the clauses. + * + * This class is responsible for 1 & 2. The proof of UNSAT is delegated to a + * subclass. + */ +class BitVectorProof : public TheoryProof +{ + protected: + BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); + virtual ~BitVectorProof(){}; + + // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ]) ExprSet d_declarations; - ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof + // terms and formulas that are actually relevant to the proof + ExprSet d_usedBB; + + ExprSet d_seenBBTerms; // terms that need to be bit-blasted + std::vector d_bbTerms; // order of bit-blasting - ExprSet d_seenBBTerms; // terms that need to be bit-blasted - std::vector d_bbTerms; // order of bit-blasting - ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted + /** atoms that need to be bit-blasted, + * BV-literals -> (BV-literals <=> bool formula) + * where a BV literal is a signed or unsigned comparison. + */ + ExprToExpr d_bbAtoms; // map from Expr representing normalized lemma to ClauseId in SAT solver ExprToClauseId d_bbConflictMap; - BVSatProof* d_resolutionProof; - CnfProof* d_cnfProof; - - bool d_isAssumptionConflict; theory::bv::TBitblaster* d_bitblaster; + + /** In an LFSC proof the manifestation of this expression bit-level + * representation will have a string name. This method returns that name. + */ std::string getBBTermName(Expr expr); - std::map d_constantLetMap; + /** A mapping from constant BV terms to identifiers that will refer to them in + * an LFSC proof, if constant-letification is enabled. + */ + std::map d_constantLetMap; + + /** Should we introduced identifiers to refer to BV constant terms? It may + * reduce the textual size of a proof! + */ bool d_useConstantLetification; - theory::TheoryId getTheoryId() override; - context::Context d_fakeContext; -public: - BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); - void initSatProof(CVC4::BVMinisat::Solver* solver); - void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - void setBitblaster(theory::bv::TBitblaster* bb); + /** Temporary storage for the set of nodes in the bitblasted formula which + * correspond to CNF variables eventually used in the proof of unsat on the + * CNF formula + */ + std::set d_atomsInBitblastingProof; - BVSatProof* getSatProof(); - CnfProof* getCnfProof() {return d_cnfProof; } - void finalizeConflicts(std::vector& conflicts); + /** + * Prints out + * (a) a declaration of bit-level interpretations corresponding to bits in + * the input BV terms. + * (b) a proof that the each BV literal entails a boolean formula on + * bitof expressions. + */ + void printBitblasting(std::ostream& os, std::ostream& paren); - void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); - void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); /** - * All the - * - * @param confl an inconsistent set of bv literals + * The proof that the bit-blasted SAT formula is correctly converted to CNF */ - void endBVConflict(const BVMinisat::Solver::TLitVec& confl); - void markAssumptionConflict() { d_isAssumptionConflict = true; } - bool isAssumptionConflict() { return d_isAssumptionConflict; } + std::unique_ptr d_cnfProof; + + public: + void printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; + + void printOwnedSort(Type type, std::ostream& os) override; + + /** + * Populate the d_atomsInBitblastingProof member. + * See its documentation + */ + virtual void calculateAtomsInBitblastingProof() = 0; + + /** + * Read the d_atomsInBitblastingProof member. + * See its documentation. + */ + const std::set* getAtomsInBitblastingProof(); void registerTermBB(Expr term); + + /** + * Informs the proof that the `atom` predicate was bitblasted into the + * `atom_bb` term. + * + * The `atom` term must be a comparison of bitvectors, and the `atom_bb` term + * a boolean formula on bitof expressions + */ void registerAtomBB(Expr atom, Expr atom_bb); void registerTerm(Expr term) override; - virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; + /** + * This must be done before registering any terms or atoms, since the CNF + * proof must reflect the result of bitblasting those + */ + virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; - virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0; - virtual const std::set* getAtomsInBitblastingProof() = 0; - virtual void calculateAtomsInBitblastingProof() = 0; -}; + CnfProof* getCnfProof() { return d_cnfProof.get(); } + + void setBitblaster(theory::bv::TBitblaster* bb); -class LFSCBitVectorProof: public BitVectorProof { + private: + ExprToString d_exprToVariableName; + + ExprToString d_assignedAliases; + std::map d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); + // Functions for printing various BV terms. Helpers for BV's `printOwnedTerm` void printConstant(Expr term, std::ostream& os); void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map); void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map); @@ -128,29 +176,19 @@ class LFSCBitVectorProof: public BitVectorProof { void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map); void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map); - ExprToString d_exprToVariableName; - ExprToString d_assignedAliases; - std::map d_aliasToBindDeclaration; - std::string assignAlias(Expr expr); - bool hasAlias(Expr expr); + /** + * Prints the LFSC construction of a bblast_term for `term` + */ + void printTermBitblasting(Expr term, std::ostream& os); - std::set d_atomsInBitblastingProof; + /** + * For a given BV-atom (a comparison), prints a proof that that comparison + * holds iff the bitblasted equivalent of it holds. + * Uses a side-condidition to do the bit-blasting. + */ + void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + void printAtomBitblastingToFalse(Expr term, std::ostream& os); -public: - LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - :BitVectorProof(bv, proofEngine) - {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; - void printOwnedSort(Type type, std::ostream& os) override; - void printTermBitblasting(Expr term, std::ostream& os) override; - void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override; - void printAtomBitblastingToFalse(Expr term, std::ostream& os) override; - void printTheoryLemmaProof(std::vector& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) override; void printSortDeclarations(std::ostream& os, std::ostream& paren) override; void printTermDeclarations(std::ostream& os, std::ostream& paren) override; void printDeferredDeclarations(std::ostream& os, @@ -158,12 +196,7 @@ public: void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap& globalLetMap) override; - void printBitblasting(std::ostream& os, std::ostream& paren) override; - void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) override; - void calculateAtomsInBitblastingProof() override; - const std::set* getAtomsInBitblastingProof() override; + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e7b00068a..5b26432dd 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -21,11 +21,11 @@ #include "context/context.h" #include "options/bv_options.h" #include "options/proof_options.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/lfsc_proof_printer.h" #include "proof/proof_utils.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof_implementation.h" #include "proof/theory_proof.h" #include "smt/smt_engine.h" @@ -116,10 +116,11 @@ UFProof* ProofManager::getUfProof() { return (UFProof*)pf; } -BitVectorProof* ProofManager::getBitVectorProof() { +proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof() +{ Assert (options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); - return (BitVectorProof*)pf; + return static_cast(pf); } ArrayProof* ProofManager::getArrayProof() { diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0342288fe..82efbab0f 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -69,7 +69,10 @@ class TheoryProof; class UFProof; class ArithProof; class ArrayProof; -class BitVectorProof; + +namespace proof { +class ResolutionBitVectorProof; +} template class LFSCSatProof; typedef TSatProof CoreSatProof; @@ -77,7 +80,6 @@ typedef TSatProof CoreSatProof; class LFSCCnfProof; class LFSCTheoryProofEngine; class LFSCUFProof; -class LFSCBitVectorProof; class LFSCRewriterProof; namespace prop { @@ -189,7 +191,7 @@ public: static TheoryProofEngine* getTheoryProofEngine(); static TheoryProof* getTheoryProof( theory::TheoryId id ); static UFProof* getUfProof(); - static BitVectorProof* getBitVectorProof(); + static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp new file mode 100644 index 000000000..667d630f8 --- /dev/null +++ b/src/proof/resolution_bitvector_proof.cpp @@ -0,0 +1,522 @@ +/********************* */ +/*! \file resolution_bitvector_proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Guy Katz, Paul Meng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + +**/ + +#include "proof/resolution_bitvector_proof.h" +#include "options/bv_options.h" +#include "options/proof_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" +#include "proof/clause_id.h" +#include "proof/lfsc_proof_printer.h" +#include "proof/proof_output_channel.h" +#include "proof/proof_utils.h" +#include "proof/sat_proof_implementation.h" +#include "prop/bvminisat/bvminisat.h" +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_rewrite_rules.h" + +#include +#include + +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +namespace CVC4 { + +namespace proof { + +ResolutionBitVectorProof::ResolutionBitVectorProof( + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : BitVectorProof(bv, proofEngine), + d_resolutionProof(), + d_isAssumptionConflict(false) +{ +} + +void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) +{ + Assert(d_resolutionProof == NULL); + d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true)); +} + +theory::TheoryId ResolutionBitVectorProof::getTheoryId() +{ + return theory::THEORY_BV; +} + +void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf) +{ + 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(true); + Node false_node = NodeManager::currentNM()->mkConst(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(); +} + +BVSatProof* ResolutionBitVectorProof::getSatProof() +{ + Assert(d_resolutionProof != NULL); + return d_resolutionProof.get(); +} + +void ResolutionBitVectorProof::startBVConflict( + CVC4::BVMinisat::Solver::TCRef cr) +{ + d_resolutionProof->startResChain(cr); +} + +void ResolutionBitVectorProof::startBVConflict( + CVC4::BVMinisat::Solver::TLit lit) +{ + d_resolutionProof->startResChain(lit); +} + +void ResolutionBitVectorProof::endBVConflict( + const CVC4::BVMinisat::Solver::TLitVec& confl) +{ + Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict called" + << std::endl; + + std::vector expr_confl; + for (int i = 0; i < confl.size(); ++i) + { + prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); + Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; + expr_confl.push_back(expr_lit); + } + + Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); + Debug("pf::bv") << "Make conflict for " << conflict << std::endl; + + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) + { + Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl; + // This can only happen when we have eager explanations in the bv solver + // if we don't get to propagate p before ~p is already asserted + d_resolutionProof->cancelResChain(); + return; + } + + // we don't need to check for uniqueness in the sat solver then + ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); + d_bbConflictMap[conflict] = clause_id; + d_resolutionProof->endResChain(clause_id); + Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict id" << clause_id + << " => " << conflict << "\n"; + d_isAssumptionConflict = false; +} + +void ResolutionBitVectorProof::finalizeConflicts(std::vector& conflicts) +{ + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { + Debug("pf::bv") << "Construct full proof." << std::endl; + d_resolutionProof->constructProof(); + return; + } + + for (unsigned i = 0; i < conflicts.size(); ++i) + { + Expr confl = conflicts[i]; + Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; + + // Special case: if the conflict has a (true) or a (not false) in it, it is + // trivial... + bool ignoreConflict = false; + if ((confl.isConst() && confl.getConst()) + || (confl.getKind() == kind::NOT && confl[0].isConst() + && !confl[0].getConst())) + { + ignoreConflict = true; + } + else if (confl.getKind() == kind::OR) + { + for (unsigned k = 0; k < confl.getNumChildren(); ++k) + { + if ((confl[k].isConst() && confl[k].getConst()) + || (confl[k].getKind() == kind::NOT && confl[k][0].isConst() + && !confl[k][0].getConst())) + { + ignoreConflict = true; + } + } + } + if (ignoreConflict) + { + Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" + << std::endl; + continue; + } + + if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) + { + ClauseId id = d_bbConflictMap[confl]; + d_resolutionProof->collectClauses(id); + } + else + { + // There is no exact match for our conflict, but maybe it is a subset of + // another conflict + ExprToClauseId::const_iterator it; + bool matchFound = false; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + Expr possibleMatch = it->first; + if (possibleMatch.getKind() != kind::OR) + { + // This is a single-node conflict. If this node is in the conflict + // we're trying to prove, we have a match. + for (unsigned k = 0; k < confl.getNumChildren(); ++k) + { + if (confl[k] == possibleMatch) + { + matchFound = true; + d_resolutionProof->collectClauses(it->second); + break; + } + } + } + else + { + if (possibleMatch.getNumChildren() > confl.getNumChildren()) continue; + + unsigned k = 0; + bool matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) + { + // j is the index in possibleMatch + // k is the index in confl + while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) + { + ++k; + } + if (k == confl.getNumChildren()) + { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + + if (matching) + { + Debug("pf::bv") + << "Collecting info from a sub-conflict" << std::endl; + d_resolutionProof->collectClauses(it->second); + matchFound = true; + break; + } + } + } + + if (!matchFound) + { + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first + << std::endl; + } + + Unreachable(); + } + } + } +} + +void LFSCBitVectorProof::printTheoryLemmaProof(std::vector& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) +{ + Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" + << std::endl; + Expr conflict = utils::mkSortedExpr(kind::OR, lemma); + Debug("pf::bv") << "\tconflict = " << conflict << std::endl; + + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) + { + std::ostringstream lemma_paren; + for (unsigned i = 0; i < lemma.size(); ++i) + { + Expr lit = lemma[i]; + + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + Expr lem = utils::mkOr(lemma); + Assert(d_bbConflictMap.find(lem) != d_bbConflictMap.end()); + ClauseId lemma_id = d_bbConflictMap[lem]; + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof.get(), lemma_id, os, lemma_paren); + os << lemma_paren.str(); + } + else + { + Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching " + "sub-conflict..." + << std::endl; + + bool matching; + + ExprToClauseId::const_iterator it; + unsigned i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + // Our conflict is sorted, and the records are also sorted. + ++i; + Expr possibleMatch = it->first; + + if (possibleMatch.getKind() != kind::OR) + { + // This is a single-node conflict. If this node is in the conflict we're + // trying to prove, we have a match. + matching = false; + + for (unsigned k = 0; k < conflict.getNumChildren(); ++k) + { + if (conflict[k] == possibleMatch) + { + matching = true; + break; + } + } + } + else + { + if (possibleMatch.getNumChildren() > conflict.getNumChildren()) + continue; + + unsigned k = 0; + + matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) + { + // j is the index in possibleMatch + // k is the index in conflict + while (k < conflict.getNumChildren() + && conflict[k] != possibleMatch[j]) + { + ++k; + } + if (k == conflict.getNumChildren()) + { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + } + + if (matching) + { + Debug("pf::bv") << "Found a match with conflict #" << i << ": " + << std::endl + << possibleMatch << std::endl; + // The rest is just a copy of the usual handling, if a precise match is + // found. We only use the literals that appear in the matching conflict, + // though, and not in the original lemma - as these may not have even + // been bit blasted! + std::ostringstream lemma_paren; + + if (possibleMatch.getKind() == kind::OR) + { + for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) + { + Expr lit = possibleMatch[i]; + + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = + d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + } + else + { + // The conflict only consists of one node, either positive or + // negative. + Expr lit = possibleMatch; + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = + d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + + ClauseId lemma_id = it->second; + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof.get(), lemma_id, os, lemma_paren); + os << lemma_paren.str(); + + return; + } + } + + // We failed to find a matching sub conflict. The last hope is that the + // conflict has a FALSE assertion in it; this can happen in some corner + // cases, where the FALSE is the result of a rewrite. + + for (unsigned i = 0; i < lemma.size(); ++i) + { + if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) + { + Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; + os << "(clausify_false "; + os << ProofManager::getLitName(lemma[i]); + os << ")"; + return; + } + } + + Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; + } + + Unreachable(); + } +} + +void LFSCBitVectorProof::calculateAtomsInBitblastingProof() +{ + // Collect the input clauses used + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); + Assert(used_lemmas.empty()); +} + +void LFSCBitVectorProof::printResolutionProof(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; + + std::set::iterator atomIt; + Debug("pf::bv") << std::endl + << "BV Dumping atoms from inputs: " << std::endl + << std::endl; + for (atomIt = d_atomsInBitblastingProof.begin(); + atomIt != d_atomsInBitblastingProof.end(); + ++atomIt) + { + Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; + } + Debug("pf::bv") << std::endl; + + // first print bit-blasting + printBitblasting(os, paren); + + // print CNF conversion proof for bit-blasted facts + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + + d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); + os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; + for (IdToSatClause::iterator it = used_inputs.begin(); + it != used_inputs.end(); + ++it) + { + d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); + } + + os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; + proof::LFSCProofPrinter::printResolutions(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 new file mode 100644 index 000000000..a54d72d3f --- /dev/null +++ b/src/proof/resolution_bitvector_proof.h @@ -0,0 +1,132 @@ +/********************* */ +/*! \file resolution_bitvector_proof.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Mathias Preiner, Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 + ** + ** Bitvector proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H +#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H + +#include + +#include "context/context.h" +#include "expr/expr.h" +#include "proof/bitvector_proof.h" +#include "proof/theory_proof.h" +#include "prop/bvminisat/core/Solver.h" + +namespace CVC4 { + +namespace theory { +namespace bv { +class TheoryBV; +template +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 TSatProof; +typedef TSatProof BVSatProof; + +namespace proof { + +/** + * Represents a bitvector proof which is backed by + * (a) bitblasting and + * (b) a resolution unsat proof. + * + * Contains tools for constructing BV conflicts + */ +class ResolutionBitVectorProof : public BitVectorProof +{ + public: + ResolutionBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine); + + /** + * Create an (internal) SAT proof object + * Must be invoked before manipulating BV conflicts, + * or initializing a BNF proof + */ + void initSatProof(CVC4::BVMinisat::Solver* solver); + + 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& conflicts); + + void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); + void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); + void endBVConflict(const BVMinisat::Solver::TLitVec& confl); + + 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; + + protected: + // The CNF formula that results from bit-blasting will need a proof. + // This is that proof. + std::unique_ptr d_resolutionProof; + + bool d_isAssumptionConflict; + + theory::TheoryId getTheoryId() override; + context::Context d_fakeContext; +}; + +class LFSCBitVectorProof : public ResolutionBitVectorProof +{ + public: + LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : ResolutionBitVectorProof(bv, proofEngine) + { + } + void printTheoryLemmaProof(std::vector& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) override; + void printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void calculateAtomsInBitblastingProof() override; +}; + +} // namespace proof + +} // namespace CVC4 + +#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index cfad0a068..ee06fbfa0 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -22,12 +22,12 @@ #include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof.h" #include "proof/simplify_boolean_node.h" #include "proof/uf_proof.h" @@ -46,6 +46,9 @@ namespace CVC4 { +using proof::LFSCBitVectorProof; +using proof::ResolutionBitVectorProof; + unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; @@ -77,7 +80,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } if (id == theory::THEORY_BV) { - BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); + auto bv_theory = static_cast(th); + ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this); d_theoryProofTable[id] = bvp; return; } @@ -102,9 +106,9 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { theory::TheoryId id = th->getId(); if (id == theory::THEORY_BV) { Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); - - BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + ResolutionBitVectorProof* bvp = + (ResolutionBitVectorProof*)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp); return; } } @@ -529,7 +533,7 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std } } - BitVectorProof* bv = ProofManager::getBitVectorProof(); + ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); // bv->printResolutionProof(os, paren, letMap); } diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h new file mode 100644 index 000000000..686848829 --- /dev/null +++ b/src/prop/bv_sat_solver_notify.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file sat_solver_notify.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Dejan Jovanovic, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 The interface for things that want to recieve notification from the + ** SAT solver + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__BVSATSOLVERNOTIFY_H +#define __CVC4__PROP__BVSATSOLVERNOTIFY_H + +#include "prop/sat_solver_types.h" + +namespace CVC4 { +namespace prop { + +class BVSatSolverNotify { +public: + + virtual ~BVSatSolverNotify() {}; + + /** + * If the notify returns false, the solver will break out of whatever it's currently doing + * with an "unknown" answer. + */ + virtual bool notify(SatLiteral lit) = 0; + + /** + * Notify about a learnt clause. + */ + virtual void notify(SatClause& clause) = 0; + virtual void spendResource(unsigned amount) = 0; + virtual void safePoint(unsigned amount) = 0; + +};/* class BVSatSolverInterface::Notify */ + +} +} + +#endif diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 1eb4bce96..55710092b 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -51,7 +51,7 @@ void BVMinisatSatSolver::MinisatNotify::notify( d_notify->notify(satClause); } -void BVMinisatSatSolver::setNotify(Notify* notify) { +void BVMinisatSatSolver::setNotify(BVSatSolverNotify* notify) { d_minisatNotify.reset(new MinisatNotify(notify)); d_minisat->setNotify(d_minisatNotify.get()); } @@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } -void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) { +void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_minisat->setProofLog( bvp ); } diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 728d26bd4..16489b172 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -22,8 +22,10 @@ #include "context/cdo.h" #include "proof/clause_id.h" +#include "proof/resolution_bitvector_proof.h" #include "prop/bvminisat/simp/SimpSolver.h" #include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -35,10 +37,10 @@ class BVMinisatSatSolver : public BVSatSolverInterface, private: class MinisatNotify : public BVMinisat::Notify { - BVSatSolverInterface::Notify* d_notify; + BVSatSolverNotify* d_notify; public: - MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {} + MinisatNotify(BVSatSolverNotify* notify) : d_notify(notify) {} bool notify(BVMinisat::Lit lit) override { return d_notify->notify(toSatLiteral(lit)); @@ -66,7 +68,7 @@ public: BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); virtual ~BVMinisatSatSolver(); - void setNotify(Notify* notify) override; + void setNotify(BVSatSolverNotify* notify) override; ClauseId addClause(SatClause& clause, bool removable) override; @@ -117,7 +119,7 @@ public: void popAssumption() override; - void setProofLog(BitVectorProof* bvp) override; + void setProofLog(proof::ResolutionBitVectorProof* bvp) override; private: /* Disable the default constructor. */ diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index a4b0248e0..a877f20c3 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -29,9 +29,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "options/bv_options.h" #include "options/smt_options.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/mtl/Sort.h" @@ -1318,7 +1318,8 @@ void Solver::explain(Lit p, std::vector& explanation) { } } -void Solver::setProofLog( BitVectorProof * bvp ) { +void Solver::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bvp = bvp; d_bvp->initSatProof(this); d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false)); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index da4fb4c16..eef1c4e4c 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -39,7 +39,10 @@ namespace BVMinisat { class Solver; } -class BitVectorProof; +// TODO (aozdemir) replace this forward declaration with an include +namespace proof { +class ResolutionBitVectorProof; +} namespace BVMinisat { @@ -212,10 +215,10 @@ public: bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} void explain(Lit l, std::vector& explanation); - - void setProofLog( CVC4::BitVectorProof * bvp ); -protected: + void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp); + + protected: // has a clause been added bool clause_added; @@ -292,7 +295,7 @@ protected: bool asynch_interrupt; //proof log - CVC4::BitVectorProof * d_bvp; + CVC4::proof::ResolutionBitVectorProof* d_bvp; // Main internal methods: // diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 5222af200..49064c20f 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -26,13 +26,13 @@ #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" #include "util/statistics_registry.h" namespace CVC4 { - -class BitVectorProof; namespace prop { @@ -96,9 +96,9 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - - virtual void setProofLog( BitVectorProof * bvp ) {} - + + virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} + };/* class SatSolver */ @@ -107,27 +107,8 @@ public: virtual ~BVSatSolverInterface() {} /** Interface for notifications */ - class Notify { - public: - - virtual ~Notify() {}; - - /** - * If the notify returns false, the solver will break out of whatever it's currently doing - * with an "unknown" answer. - */ - virtual bool notify(SatLiteral lit) = 0; - - /** - * Notify about a learnt clause. - */ - virtual void notify(SatClause& clause) = 0; - virtual void spendResource(unsigned amount) = 0; - virtual void safePoint(unsigned amount) = 0; - - };/* class BVSatSolverInterface::Notify */ - virtual void setNotify(Notify* notify) = 0; + virtual void setNotify(BVSatSolverNotify* notify) = 0; virtual void markUnremovable(SatLiteral lit) = 0; diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index f041f6898..ed1c5397d 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -24,8 +24,9 @@ #include "cvc4_private.h" -#include #include +#include +#include namespace CVC4 { namespace prop { diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 6d21b69e6..62e70d73d 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H #include "theory/bv/bitblast/bitblaster.h" +#include "prop/sat_solver.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 9e2dac2f3..73b4d19c7 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -24,7 +24,8 @@ #include #include "expr/node.h" -#include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" +#include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" @@ -59,8 +60,6 @@ class TBitblaster TermDefMap d_termCache; ModelCache d_modelCache; - BitVectorProof* d_bvp; - void initAtomBBStrategies(); void initTermBBStrategies(); @@ -94,7 +93,7 @@ class TBitblaster void invalidateModelCache(); }; -class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify +class MinisatEmptyNotify : public prop::BVSatSolverNotify { public: MinisatEmptyNotify() {} @@ -172,7 +171,7 @@ void TBitblaster::initTermBBStrategies() } template -TBitblaster::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL) +TBitblaster::TBitblaster() : d_termCache(), d_modelCache() { initAtomBBStrategies(); initTermBBStrategies(); diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 01437cb64..33d5a1c80 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -19,7 +19,6 @@ #include "theory/bv/bitblast/eager_bitblaster.h" #include "options/bv_options.h" -#include "proof/bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" @@ -37,6 +36,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), d_cnfStream(), + d_bvp(nullptr), d_bv(theory_bv), d_bbAtoms(), d_variables(), @@ -268,10 +268,11 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void EagerBitblaster::setProofLog(BitVectorProof* bvp) { - d_bvp = bvp; - d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); +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) { diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 3e6190d76..3299ffc54 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -23,6 +23,8 @@ #include "theory/bv/bitblast/bitblaster.h" +#include "proof/bitvector_proof.h" +#include "proof/resolution_bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" @@ -53,7 +55,7 @@ class EagerBitblaster : public TBitblaster bool solve(); bool solve(const std::vector& assumptions); bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); private: context::Context* d_context; @@ -65,6 +67,8 @@ class EagerBitblaster : public TBitblaster std::unique_ptr d_bitblastingRegistrar; std::unique_ptr d_cnfStream; + BitVectorProof* d_bvp; + TheoryBV* d_bv; TNodeSet d_bbAtoms; TNodeSet d_variables; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index a50916413..529f0373b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -19,17 +19,16 @@ #include "theory/bv/bitblast/lazy_bitblaster.h" #include "options/bv_options.h" +#include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" -#include "proof/bitvector_proof.h" -#include "proof/proof_manager.h" -#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -65,6 +64,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bool emptyNotify) : TBitblaster(), d_bv(bv), + d_bvp(nullptr), d_ctx(c), d_nullRegistrar(new prop::NullRegistrar()), d_nullContext(new context::Context()), @@ -90,8 +90,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); @@ -566,7 +566,8 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ +void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bvp = bvp; d_satSolver->setProofLog( bvp ); bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); @@ -590,8 +591,8 @@ void TLazyBitblaster::clearSolver() { d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), d_bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 5e16b743a..1195d3590 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -19,13 +19,14 @@ #ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H #define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H +#include "proof/resolution_bitvector_proof.h" #include "theory/bv/bitblast/bitblaster.h" #include "context/cdhashmap.h" #include "context/cdlist.h" #include "prop/cnf_stream.h" #include "prop/registrar.h" -#include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" #include "theory/bv/abstraction.h" namespace CVC4 { @@ -76,7 +77,7 @@ class TLazyBitblaster : public TBitblaster * constants to equivalence classes that don't already have them */ bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setProofLog(proof::ResolutionBitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -106,7 +107,7 @@ class TLazyBitblaster : public TBitblaster prop::SatLiteralHashFunction> ExplanationMap; /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify + class MinisatNotify : public prop::BVSatSolverNotify { prop::CnfStream* d_cnf; TheoryBV* d_bv; @@ -125,13 +126,14 @@ class TLazyBitblaster : public TBitblaster }; TheoryBV* d_bv; + proof::ResolutionBitVectorProof* d_bvp; context::Context* d_ctx; std::unique_ptr d_nullRegistrar; std::unique_ptr d_nullContext; // sat solver used for bitblasting and associated CnfStream std::unique_ptr d_satSolver; - std::unique_ptr d_satSolverNotify; + std::unique_ptr d_satSolverNotify; std::unique_ptr d_cnfStream; AssertionList* diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 27a48875d..119195c4a 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -17,7 +17,6 @@ #include "theory/bv/bv_eager_solver.h" #include "options/bv_options.h" -#include "proof/bitvector_proof.h" #include "theory/bv/bitblast/aig_bitblaster.h" #include "theory/bv/bitblast/eager_bitblaster.h" @@ -57,7 +56,7 @@ void EagerBitblastSolver::initialize() { } else { d_bitblaster.reset(new EagerBitblaster(d_bv, d_context)); THEORY_PROOF(if (d_bvp) { - d_bitblaster->setProofLog(d_bvp); + d_bitblaster->setResolutionProofLog(d_bvp); d_bvp->setBitblaster(d_bitblaster.get()); }); } @@ -128,7 +127,11 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) return d_bitblaster->collectModelInfo(m, fullModel); } -void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; } +void EagerBitblastSolver::setResolutionProofLog( + proof::ResolutionBitVectorProof* bvp) +{ + d_bvp = bvp; +} } // namespace bv } // namespace theory diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index b17cd6ebc..7f688b3ae 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -23,6 +23,7 @@ #include #include "expr/node.h" +#include "proof/resolution_bitvector_proof.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -47,7 +48,7 @@ class EagerBitblastSolver { bool isInitialized(); void initialize(); bool collectModelInfo(theory::TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); private: context::CDHashSet d_assertionSet; @@ -60,7 +61,7 @@ class EagerBitblastSolver { bool d_useAig; TheoryBV* d_bv; - BitVectorProof* d_bvp; + proof::ResolutionBitVectorProof* d_bvp; }; // class EagerBitblastSolver } // namespace bv diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 3166401aa..31c542e0b 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -24,6 +24,11 @@ #include "theory/theory.h" namespace CVC4 { + +namespace proof { +class ResolutionBitVectorProof; +} + namespace theory { class TheoryModel; @@ -88,7 +93,7 @@ class SubtheorySolver { return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual void setProofLog(BitVectorProof* bvp) {} + virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } @@ -103,7 +108,7 @@ class SubtheorySolver { /** The bit-vector theory */ TheoryBV* d_bv; /** proof log */ - BitVectorProof* d_bvp; + proof::ResolutionBitVectorProof* d_bvp; AssertionQueue d_assertionQueue; context::CDO d_assertionIndex; }; /* class SubtheorySolver */ diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ea2f8e4bf..ff9dd52c2 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -18,7 +18,6 @@ #include "decision/decision_attributes.h" #include "options/bv_options.h" #include "options/decision_options.h" -#include "proof/bitvector_proof.h" #include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" @@ -277,7 +276,8 @@ void BitblastSolver::setConflict(TNode conflict) { d_bv->setConflict(final_conflict); } -void BitblastSolver::setProofLog( BitVectorProof * bvp ) { +void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* 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 ac0d38815..aa2c90c43 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -23,6 +23,11 @@ #include "theory/bv/bv_subtheory.h" namespace CVC4 { + +namespace proof { +class ResolutionBitVectorProof; +} + namespace theory { namespace bv { @@ -74,7 +79,7 @@ public: void bitblastQueue(); void setAbstraction(AbstractionModule* module); uint64_t computeAtomWeight(TNode atom); - void setProofLog(BitVectorProof* bvp) override; + void setProofLog(proof::ResolutionBitVectorProof* bvp) override; }; } /* namespace CVC4::theory::bv */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d08405ef3..e60d60456 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -986,9 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector& assertions, std::vector return changed; } -void TheoryBV::setProofLog( BitVectorProof * bvp ) { +void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) +{ if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ - d_eagerSolver->setProofLog( bvp ); + d_eagerSolver->setResolutionProofLog(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 d5e3ad02e..afa9f4b4f 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -104,9 +104,9 @@ public: bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); - void setProofLog( BitVectorProof * bvp ); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); -private: + private: class Statistics { public: