diff options
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 495 |
1 files changed, 442 insertions, 53 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index b63782226..479266db4 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,9 +15,11 @@ **/ -#include "proof/bitvector_proof.h" #include "options/bv_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" #include "proof/clause_id.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" @@ -80,20 +82,40 @@ BVSatProof* BitVectorProof::getSatProof() { } void BitVectorProof::registerTermBB(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl; + 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 (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; + Expr def = atom.iffExpr(atom_bb); - d_bbAtoms.insert(std::make_pair(atom, def)); + d_bbAtoms.insert(std::make_pair(atom, def)); registerTerm(atom); + + // Register the atom's terms for bitblasting + registerTermBB(atom[0]); + registerTermBB(atom[1]); } void BitVectorProof::registerTerm(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; + d_usedBB.insert(term); if (Theory::isLeafOf(term, theory::THEORY_BV) && @@ -101,6 +123,11 @@ void BitVectorProof::registerTerm(Expr term) { d_declarations.insert(term); } + Debug("pf::bv") << "Going to register children: " << std::endl; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + Debug("pf::bv") << "\t" << term[i] << std::endl; + } + // don't care about parametric operators for bv? for (unsigned i = 0; i < term.getNumChildren(); ++i) { d_proofEngine->registerTerm(term[i]); @@ -108,6 +135,7 @@ void BitVectorProof::registerTerm(Expr term) { } std::string BitVectorProof::getBBTermName(Expr expr) { + Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl; std::ostringstream os; os << "bt"<< expr.getId(); return os.str(); @@ -122,6 +150,8 @@ void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit 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]); @@ -129,6 +159,7 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl 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; @@ -144,25 +175,99 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl 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"; + 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) { + + for (unsigned i = 0; i < conflicts.size(); ++i) { Expr confl = conflicts[i]; - Debug("pf::bv") << "Finalize conflict " << confl << std::endl; - //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); - if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ + 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{ - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; + } 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(); + } } } } @@ -238,11 +343,25 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa printBitOf(term, os, map); return; } - case kind::VARIABLE: + + case kind::VARIABLE: { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + return; + } + case kind::SKOLEM: { - os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; + + // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems, + // like ITE terms. Is there a more elegant way? + + if (ProofManager::getSkolemizationManager()->isSkolem(term)) { + os << ProofManager::sanitize(term); + } else { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + } return; } + default: Unreachable(); } @@ -258,14 +377,7 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m << ", var = " << var << std::endl; os << "(bitof "; - if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) { - // If var is "simple", we can just sanitize and print - os << ProofManager::sanitize(var); - } else { - // If var is "complex", it can belong to another theory. Therefore, dispatch again. - d_proofEngine->printBoundTerm(var, os, map); - } - + os << d_exprToVariableName[var]; os << " " << bit << ")"; } @@ -349,14 +461,16 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::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) { + 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) { @@ -377,7 +491,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::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"; + os <<"(\\ unit"<<bb_var<<"\n"; lemma_paren <<")"; } Expr lem = utils::mkOr(lemma); @@ -386,11 +500,120 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); os <<lemma_paren.str(); } else { - Unreachable(); // If we were to reach here, we would crash because BV replay is currently not supported - // in TheoryProof::printTheoryLemmaProof() - Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; - BitVectorProof::printTheoryLemmaProof( lemma, os, paren ); + 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; + d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + os <<lemma_paren.str(); + + 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(); } } @@ -402,7 +625,13 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { - os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n"; + if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) { + d_exprToVariableName[*it] = ProofManager::sanitize(*it); + } else { + d_exprToVariableName[*it] = assignAlias(*it); + } + + os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; paren <<")"; } } @@ -411,15 +640,43 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea // Nothing to do here at this point. } +void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Print "trust" statements to bind complex bv variables to their associated terms + + ExprToString::const_iterator it = d_assignedAliases.begin(); + ExprToString::const_iterator end = d_assignedAliases.end(); + + for (; it != end; ++it) { + Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl; + std::stringstream declaration; + declaration << ".fbvd" << d_aliasToBindDeclaration.size(); + d_aliasToBindDeclaration[it->second] = declaration.str(); + + os << "(th_let_pf _ "; + + os << "(trust_f "; + os << "(= (BitVec " << utils::getSize(it->first) << ") "; + os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") "; + LetMap emptyMap; + d_proofEngine->printBoundTerm(it->first, os, emptyMap); + os << ")) "; + os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n"; + paren << "))"; + } + + os << "\n"; +} + void LFSCBitVectorProof::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()) { - os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )"; + if (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; } @@ -448,37 +705,60 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_PLUS : case kind::BITVECTOR_SUB : case kind::BITVECTOR_CONCAT : { - for (unsigned i =0; i < term.getNumChildren() - 1; ++i) { + Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; + + for (int i = term.getNumChildren() - 1; i > 0; --i) { os <<"(bv_bbl_"<< utils::toLFSCKind(kind); + + if (i > 1) { + // This is not the inner-most operation; only child i+1 can be aliased + if (hasAlias(term[i])) {os << "_alias_2";} + } else { + // This is the inner-most operation; both children can be aliased + if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";} + if (hasAlias(term[i-1])) {os << "_1";} + if (hasAlias(term[i])) {os << "_2";} + } + if (kind == kind::BITVECTOR_CONCAT) { - os << " " << utils::getSize(term) <<" _ "; + os << " " << utils::getSize(term) << " _"; } - os <<" _ _ _ _ _ _ "; + os << " _ _ _ _ _ _ "; } - os << getBBTermName(term[0]) <<" "; + + if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} + os << getBBTermName(term[0]) << " "; for (unsigned i = 1; i < term.getNumChildren(); ++i) { + if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";} os << getBBTermName(term[i]); os << ") "; } return; } + case kind::BITVECTOR_NEG : case kind::BITVECTOR_NOT : case kind::BITVECTOR_ROTATE_LEFT : case kind::BITVECTOR_ROTATE_RIGHT : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind); - os <<" _ _ _ _ "; + os << "(bv_bbl_"<<utils::toLFSCKind(kind); + os << " _ _ _ _ "; os << getBBTermName(term[0]); - os <<")"; + os << ")"; return; } case kind::BITVECTOR_EXTRACT : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; - os << utils::getSize(term) << " "; + os <<"(bv_bbl_"<<utils::toLFSCKind(kind); + + if (hasAlias(term[0])) {os << "_alias";}; + + os << " " << utils::getSize(term) << " "; os << utils::getExtractHigh(term) << " "; os << utils::getExtractLow(term) << " "; os << " _ _ _ _ "; + + if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} + os << getBBTermName(term[0]); os <<")"; return; @@ -486,7 +766,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_REPEAT : case kind::BITVECTOR_ZERO_EXTEND : case kind::BITVECTOR_SIGN_EXTEND : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; + os <<"(bv_bbl_" <<utils::toLFSCKind(kind) << (hasAlias(term[0]) ? "_alias " : " "); os << utils::getSize(term) <<" "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; @@ -501,7 +781,9 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; os << amount; } + os <<" _ _ _ _ "; + if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} os << getBBTermName(term[0]); os <<")"; return; @@ -539,7 +821,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -550,11 +832,28 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { case kind::BITVECTOR_SLE : case kind::BITVECTOR_SGT : case kind::BITVECTOR_SGE : - case kind::EQUAL: - { - os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + case kind::EQUAL: { + Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; + + os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + + if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";} + if (hasAlias(atom[0])) {os << "_1";} + if (hasAlias(atom[1])) {os << "_2";} + + if (swap) {os << "_swap";} + os << " _ _ _ _ _ _ "; - os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; + + if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} + os << getBBTermName(atom[0]); + + os << " "; + + if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} + os << getBBTermName(atom[1]); + + os << ")"; return; } default: @@ -562,19 +861,53 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { } } +void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { + Assert(atom.getKind() == kind::EQUAL); + + os << "(bv_bbl_=_false"; + os << " _ _ _ _ _ _ "; + if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} + os << getBBTermName(atom[0]); + + os << " "; + + if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} + os << getBBTermName(atom[1]); + + os << ")"; +} void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { // bit-blast terms + { + Debug("pf::bv") << "LFSCBitVectorProof::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(); + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + + for (; it != end; ++it) { + if (d_usedBB.find(*it) == d_usedBB.end()) { + Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; + } else { + Debug("pf::bv") << "\t" << *it << std::endl; + } + } + + Debug("pf::bv") << std::endl; + } + std::vector<Expr>::const_iterator it = d_bbTerms.begin(); std::vector<Expr>::const_iterator end = d_bbTerms.end(); for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end() && options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) continue; - os <<"(decl_bblast _ _ _ "; + + os << "(decl_bblast _ _ _ "; printTermBitblasting(*it, os); - os << "(\\ "<< getBBTermName(*it); - paren <<"\n))"; + os << "(\\ "<< getBBTermName(*it) << "\n"; + paren << "))"; } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -589,7 +922,35 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) bool val = ait->first.getConst<bool>(); os << "(iff_symm " << (val ? "true" : "false" ) << ")"; } else { - printAtomBitblasting(ait->first, os); + Assert(ait->first == ait->second[0]); + + bool swap = false; + if (ait->first.getKind() == kind::EQUAL) { + Expr bitwiseEquivalence = ait->second[1]; + if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst<bool>()) { + printAtomBitblastingToFalse(ait->first, os); + } else { + if (bitwiseEquivalence.getKind() != kind::AND) { + // Just one bit + if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0]); + } + } else { + // Multiple bits + if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0][0]); + } else if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[0] == bitwiseEquivalence[0][1][0]); + } + } + + printAtomBitblasting(ait->first, os, swap); + } + } else { + printAtomBitblasting(ait->first, os, swap); + } } os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; @@ -606,25 +967,53 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, used_lemmas); Assert (used_lemmas.empty()); + IdToSatClause::iterator it2; + Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl; + for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) { + Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl; + } + Debug("pf::bv") << std::endl; + // print mapping between theory atoms and internal SAT variables - os << ";; BB atom mapping\n"; + os << std::endl << ";; BB atom mapping\n" << std::endl; + + std::set<Node> atoms; + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); - NodeSet atoms; - d_cnfProof->collectAtomsForClauses(used_inputs,atoms); + std::set<Node>::iterator atomIt; + Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; + for (atomIt = atoms.begin(); atomIt != atoms.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 d_cnfProof->printAtomMapping(atoms, os, paren); - os << ";; Bit-blasting definitional clauses \n"; + 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 << ";; Bit-blasting learned clauses \n"; + os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; d_resolutionProof->printResolutions(os, paren); } +std::string LFSCBitVectorProof::assignAlias(Expr expr) { + static unsigned counter = 0; + Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); + std::stringstream ss; + ss << "fbv" << counter++; + Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl; + d_assignedAliases[expr] = ss.str(); + return ss.str(); +} + +bool LFSCBitVectorProof::hasAlias(Expr expr) { + return d_assignedAliases.find(expr) != d_assignedAliases.end(); +} + } /* namespace CVC4 */ |