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
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
** 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),
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<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();
+ d_bitblaster(nullptr),
+ d_useConstantLetification(false),
+ d_cnfProof()
+{
}
-void BitVectorProof::setBitblaster(bv::TBitblaster<Node>* bb) {
- Assert (d_bitblaster == NULL);
+void BitVectorProof::setBitblaster(theory::bv::TBitblaster<Node>* 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));
}
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()) {
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);
}
}
}
-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> 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" <<clause_id<< " => " << conflict << "\n";
- d_isAssumptionConflict = false;
-}
-
-void BitVectorProof::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 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) {
}
}
-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<BitVectorBitOf>().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) << " ";
}
}
-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 ? "_ _ " : "";
}
}
-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 << " ";
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 << " ";
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 <<" ";
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<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, 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, 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::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) {
}
}
-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<Expr,std::string>::const_iterator it;
}
}
-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();
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 << " _)";
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 :
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";
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<Expr>::const_iterator it = d_bbTerms.begin();
std::vector<Expr>::const_iterator end = d_bbTerms.end();
}
}
-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<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() {
+const std::set<Node>* 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<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, 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;
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));
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);
os << ")";
}
-} /* namespace CVC4 */
+} // namespace CVC4
** 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 <iostream>
#include <set>
-#include <sstream>
#include <unordered_map>
#include <unordered_set>
#include <vector>
-
#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 T> class TBitblaster;
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-
-class CnfProof;
-} /* namespace CVC4 */
-
-namespace CVC4 {
-
-template <class Solver> class TSatProof;
-typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
-
typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
typedef std::unordered_map<Expr, std::string, ExprHashFunction> 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<Expr> d_bbTerms; // order of bit-blasting
- ExprSet d_seenBBTerms; // terms that need to be bit-blasted
- std::vector<Expr> 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<Node>* 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<Expr,std::string> 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<Expr, std::string> 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<Node>* 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<Node> d_atomsInBitblastingProof;
- BVSatProof* getSatProof();
- CnfProof* getCnfProof() {return d_cnfProof; }
- void finalizeConflicts(std::vector<Expr>& 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<CnfProof> 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<Node>* 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<Node>* getAtomsInBitblastingProof() = 0;
- virtual void calculateAtomsInBitblastingProof() = 0;
-};
+ CnfProof* getCnfProof() { return d_cnfProof.get(); }
+
+ void setBitblaster(theory::bv::TBitblaster<Node>* bb);
-class LFSCBitVectorProof: public BitVectorProof {
+ private:
+ ExprToString d_exprToVariableName;
+
+ ExprToString d_assignedAliases;
+ std::map<std::string, std::string> 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);
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<std::string, std::string> 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<Node> 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<Expr>& 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,
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<Node>* getAtomsInBitblastingProof() override;
+
void printConstantDisequalityProof(std::ostream& os,
Expr c1,
Expr c2,
#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"
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<proof::ResolutionBitVectorProof*>(pf);
}
ArrayProof* ProofManager::getArrayProof() {
class UFProof;
class ArithProof;
class ArrayProof;
-class BitVectorProof;
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
template <class Solver> class LFSCSatProof;
typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
class LFSCCnfProof;
class LFSCTheoryProofEngine;
class LFSCUFProof;
-class LFSCBitVectorProof;
class LFSCRewriterProof;
namespace prop {
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();
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 <iosfwd>
+
+#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 T>
+class TBitblaster;
+} // namespace bv
+} // namespace theory
+
+// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
+// header cycle and remove this.
+namespace prop {
+class CnfStream;
+}
+
+} /* namespace CVC4 */
+
+
+namespace CVC4 {
+
+template <class Solver>
+class TSatProof;
+typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
+
+namespace proof {
+
+/**
+ * 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<Expr>& 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<BVSatProof> 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<Expr>& 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 */
#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"
namespace CVC4 {
+using proof::LFSCBitVectorProof;
+using proof::ResolutionBitVectorProof;
+
unsigned CVC4::ProofLetCount::counter = 0;
static unsigned LET_COUNT = 1;
}
if (id == theory::THEORY_BV) {
- BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this);
+ auto bv_theory = static_cast<theory::bv::TheoryBV*>(th);
+ ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this);
d_theoryProofTable[id] = bvp;
return;
}
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;
}
}
}
}
- BitVectorProof* bv = ProofManager::getBitVectorProof();
+ ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof();
bv->finalizeConflicts(bv_lemmas);
// bv->printResolutionProof(os, paren, letMap);
}
--- /dev/null
+/********************* */
+/*! \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
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());
}
d_minisat->popAssumption();
}
-void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) {
+void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+{
d_minisat->setProofLog( bvp );
}
#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 {
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));
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;
void popAssumption() override;
- void setProofLog(BitVectorProof* bvp) override;
+ void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
private:
/* Disable the default constructor. */
#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"
}
}
-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));
class Solver;
}
-class BitVectorProof;
+// TODO (aozdemir) replace this forward declaration with an include
+namespace proof {
+class ResolutionBitVectorProof;
+}
namespace BVMinisat {
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<Lit>& explanation);
-
- void setProofLog( CVC4::BitVectorProof * bvp );
-protected:
+ void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp);
+
+ protected:
// has a clause been added
bool clause_added;
bool asynch_interrupt;
//proof log
- CVC4::BitVectorProof * d_bvp;
+ CVC4::proof::ResolutionBitVectorProof* d_bvp;
// Main internal methods:
//
#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 {
/** 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 */
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;
#include "cvc4_private.h"
-#include <string>
#include <sstream>
+#include <string>
+#include <vector>
namespace CVC4 {
namespace prop {
#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;
#include <vector>
#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"
TermDefMap d_termCache;
ModelCache d_modelCache;
- BitVectorProof* d_bvp;
-
void initAtomBBStrategies();
void initTermBBStrategies();
void invalidateModelCache();
};
-class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify
+class MinisatEmptyNotify : public prop::BVSatSolverNotify
{
public:
MinisatEmptyNotify() {}
}
template <class T>
-TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL)
+TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache()
{
initAtomBBStrategies();
initTermBBStrategies();
#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"
d_satSolver(),
d_bitblastingRegistrar(new BitblastingRegistrar(this)),
d_cnfStream(),
+ d_bvp(nullptr),
d_bv(theory_bv),
d_bbAtoms(),
d_variables(),
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) {
#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"
bool solve();
bool solve(const std::vector<Node>& assumptions);
bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setProofLog(BitVectorProof* bvp);
+ void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
private:
context::Context* d_context;
std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
std::unique_ptr<prop::CnfStream> d_cnfStream;
+ BitVectorProof* d_bvp;
+
TheoryBV* d_bv;
TNodeSet d_bbAtoms;
TNodeSet d_variables;
#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 {
bool emptyNotify)
: TBitblaster<Node>(),
d_bv(bv),
+ d_bvp(nullptr),
d_ctx(c),
d_nullRegistrar(new prop::NullRegistrar()),
d_nullContext(new context::Context()),
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());
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());
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());
}
#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 {
* 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(); }
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;
};
TheoryBV* d_bv;
+ proof::ResolutionBitVectorProof* d_bvp;
context::Context* d_ctx;
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
std::unique_ptr<context::Context> d_nullContext;
// sat solver used for bitblasting and associated CnfStream
std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
- std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify;
+ std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
std::unique_ptr<prop::CnfStream> d_cnfStream;
AssertionList*
#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"
} 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());
});
}
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
#include <vector>
#include "expr/node.h"
+#include "proof/resolution_bitvector_proof.h"
#include "theory/bv/theory_bv.h"
#include "theory/theory_model.h"
bool isInitialized();
void initialize();
bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
- void setProofLog(BitVectorProof* bvp);
+ void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
private:
context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
bool d_useAig;
TheoryBV* d_bv;
- BitVectorProof* d_bvp;
+ proof::ResolutionBitVectorProof* d_bvp;
}; // class EagerBitblastSolver
} // namespace bv
#include "theory/theory.h"
namespace CVC4 {
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
+
namespace theory {
class TheoryModel;
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();
}
/** The bit-vector theory */
TheoryBV* d_bv;
/** proof log */
- BitVectorProof* d_bvp;
+ proof::ResolutionBitVectorProof* d_bvp;
AssertionQueue d_assertionQueue;
context::CDO<uint32_t> d_assertionIndex;
}; /* class SubtheorySolver */
#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"
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());
}
#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
+
namespace theory {
namespace bv {
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 */
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 );
bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- void setProofLog( BitVectorProof * bvp );
+ void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
-private:
+ private:
class Statistics {
public:
projects / cvc5.git / commitdiff