summaryrefslogtreecommitdiff
path: root/src/proof/bitvector_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r--src/proof/bitvector_proof.cpp495
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback