diff options
Diffstat (limited to 'src/proof/resolution_bitvector_proof.cpp')
| -rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 522 |
1 files changed, 522 insertions, 0 deletions
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 <iostream> +#include <sstream> + +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<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(); +} + +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> 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<Expr>& 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<bool>()) + || (confl.getKind() == kind::NOT && confl[0].isConst() + && !confl[0].getConst<bool>())) + { + ignoreConflict = true; + } + else if (confl.getKind() == kind::OR) + { + for (unsigned k = 0; k < confl.getNumChildren(); ++k) + { + if ((confl[k].isConst() && confl[k].getConst<bool>()) + || (confl[k].getKind() == kind::NOT && confl[k][0].isConst() + && !confl[k][0].getConst<bool>())) + { + 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<Expr>& 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<Node>::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 */ |