summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/arith_proof.cpp4
-rw-r--r--src/proof/arith_proof.h1
-rw-r--r--src/proof/array_proof.cpp173
-rw-r--r--src/proof/array_proof.h33
-rw-r--r--src/proof/bitvector_proof.cpp495
-rw-r--r--src/proof/bitvector_proof.h14
-rw-r--r--src/proof/cnf_proof.cpp115
-rw-r--r--src/proof/cnf_proof.h34
-rw-r--r--src/proof/lemma_proof.cpp193
-rw-r--r--src/proof/lemma_proof.h79
-rw-r--r--src/proof/proof_manager.cpp91
-rw-r--r--src/proof/proof_manager.h7
-rw-r--r--src/proof/proof_output_channel.cpp82
-rw-r--r--src/proof/proof_output_channel.h50
-rw-r--r--src/proof/proof_utils.cpp52
-rw-r--r--src/proof/proof_utils.h53
-rw-r--r--src/proof/sat_proof_implementation.h27
-rw-r--r--src/proof/skolemization_manager.h1
-rw-r--r--src/proof/theory_proof.cpp620
-rw-r--r--src/proof/theory_proof.h55
-rw-r--r--src/proof/uf_proof.cpp103
-rw-r--r--src/proof/uf_proof.h1
22 files changed, 1849 insertions, 434 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index a1287b667..b9907aac9 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -830,4 +830,8 @@ void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
// Nothing to do here at this point.
}
+void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* CVC4 namespace */
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 788e4bd86..810d41155 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -74,6 +74,7 @@ public:
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 8aba8dce9..aee236677 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -81,14 +81,29 @@ inline static bool match(TNode n1, TNode n2) {
void ProofArray::setRowMergeTag(unsigned tag) {
d_reasonRow = tag;
+ d_proofPrinter.d_row = tag;
}
void ProofArray::setRow1MergeTag(unsigned tag) {
d_reasonRow1 = tag;
+ d_proofPrinter.d_row1 = tag;
}
void ProofArray::setExtMergeTag(unsigned tag) {
d_reasonExt = tag;
+ d_proofPrinter.d_ext = tag;
+}
+
+unsigned ProofArray::getRowMergeTag() const {
+ return d_reasonRow;
+}
+
+unsigned ProofArray::getRow1MergeTag() const {
+ return d_reasonRow1;
+}
+
+unsigned ProofArray::getExtMergeTag() const {
+ return d_reasonExt;
}
void ProofArray::toStream(std::ostream& out) {
@@ -101,7 +116,7 @@ void ProofArray::toStream(std::ostream& out) {
void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) {
Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
- pf->debug_print("pf::array");
+ pf->debug_print("pf::array", 0, &d_proofPrinter);
Debug("pf::array") << std::endl;
toStreamRecLFSC( out, tp, pf, 0, map );
Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
@@ -114,7 +129,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
const LetMap& map) {
Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
- pf->debug_print("pf::array");
+ pf->debug_print("pf::array", 0, &d_proofPrinter);
Debug("pf::array") << std::endl;
if(tb == 0) {
@@ -150,7 +165,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
pf->d_children[i + count]->d_node.isNull();
++count) {
Debug("pf::array") << "Found a congruence: " << std::endl;
- pf->d_children[i+count]->debug_print("pf::array");
+ pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter);
congruenceClosures.push_back(pf->d_children[i+count]);
}
@@ -220,48 +235,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
++i;
}
}
- Assert(neg >= 0);
+
+ bool disequalityFound = (neg >= 0);
+ if (!disequalityFound) {
+ Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+ Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::EQUAL);
+ Assert(pf->d_node.getNumChildren() == 2);
+ Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ }
Node n1;
std::stringstream ss, ss2;
//Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(pf->d_children.size() > 2) {
+ if(!disequalityFound || pf->d_children.size() > 2) {
n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
} else {
n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
- Node n2 = pf->d_children[neg]->d_node;
- Assert(n2.getKind() == kind::NOT);
- Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
- Debug("mgdx") << "n2 is " << n2 << std::endl;
- Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
- Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
-
- if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
- if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
-
- if (pf->d_children[neg]->d_id == d_reasonExt) {
- // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
-
- // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
-
- out << "(clausify_false (contra _ ";
- out << ss.str();
-
- toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+ out << "(clausify_false (contra _ ";
- out << " ";
- out << ss2.str();
- out << "))";
+ if (disequalityFound) {
+ Node n2 = pf->d_children[neg]->d_node;
+ Assert(n2.getKind() == kind::NOT);
+ Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
+ Debug("mgdx") << "n2 is " << n2 << std::endl;
+ Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
+ Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
- } else {
- // The negative node is, e.g., a pure equality
- out << "(clausify_false (contra _ ";
+ if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
+ if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
- if(n2[0].getKind() == kind::APPLY_UF) {
+ if ((pf->d_children[neg]->d_id == d_reasonExt) ||
+ (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
+ // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
+ out << ss.str();
+ out << " ";
+ toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+ out << ss2.str();
+ } else if (n2[0].getKind() == kind::APPLY_UF) {
out << "(trans _ _ _ _ ";
out << "(symm _ _ _ ";
out << ss.str();
@@ -276,16 +291,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " <<
ProofManager::getLitName(n2[0]) << std::endl;
- out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+ out << " " << ProofManager::getLitName(n2[0]);
}
+ } else {
+ Node n2 = pf->d_node;
+ Assert(n2.getKind() == kind::EQUAL);
+ Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+ out << ss.str();
+ out << " ";
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+ n1[0].toExpr(),
+ n1[1].toExpr());
}
+ out << "))" << std::endl;
return Node();
}
if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
Debug("mgd") << "\nok, looking at congruence:\n";
- pf->debug_print("mgd");
+ pf->debug_print("mgd", 0, &d_proofPrinter);
std::stack<const theory::eq::EqProof*> stk;
for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
Assert(!pf2->d_node.isNull());
@@ -315,7 +341,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
- pf2->debug_print("mgd");
+ pf2->debug_print("mgd", 0, &d_proofPrinter);
// Temp
Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
@@ -332,7 +358,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Debug("mgd") << "SIDE IS 1\n";
if(!match(pf2->d_node, n1[1])) {
Debug("mgd") << "IN BAD CASE, our first subproof is\n";
- pf2->d_children[0]->debug_print("mgd");
+ pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter);
}
Assert(match(pf2->d_node, n1[1]));
side = 1;
@@ -546,6 +572,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
return pf->d_node;
}
+ else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+ Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::NOT);
+ Node n = pf->d_node[0];
+ Assert(n.getKind() == kind::EQUAL);
+ Assert(n.getNumChildren() == 2);
+ Assert(n[0].isConst() && n[1].isConst());
+
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+ n[0].toExpr(),
+ n[1].toExpr());
+ return pf->d_node;
+ }
+
else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
bool firstNeg = false;
bool secondNeg = false;
@@ -554,7 +594,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Assert(pf->d_children.size() >= 2);
std::stringstream ss;
Debug("mgd") << "\ndoing trans proof[[\n";
- pf->debug_print("mgd");
+ pf->debug_print("mgd", 0, &d_proofPrinter);
Debug("mgd") << "\n";
Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
@@ -772,7 +812,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
Warning() << "0 proves " << n1 << "\n";
Warning() << "1 proves " << n2 << "\n\n";
- pf->debug_print("mgdx",0);
+ pf->debug_print("mgdx", 0, &d_proofPrinter);
//toStreamRec(Warning.getStream(), pf, 0);
Warning() << "\n\n";
Unreachable();
@@ -931,6 +971,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
t4 = pf->d_children[0]->d_node[0][side][0][2];
ret = pf->d_node;
+ // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
+ bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]);
+
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
Assert(pf->d_children.size() == 1);
@@ -939,28 +982,31 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
+ if (swap) {
+ out << "(symm _ _ _ ";
+ }
+
out << "(negativerow _ _ ";
- tp->printTerm(t1.toExpr(), out, map);
+ tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
out << " ";
- tp->printTerm(t2.toExpr(), out, map);
+ tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
out << " ";
tp->printTerm(t3.toExpr(), out, map);
out << " ";
tp->printTerm(t4.toExpr(), out, map);
out << " ";
-
- // if (subproof[0][1] == t3) {
- Debug("pf::array") << "Dont need symmetry!" << std::endl;
- out << ss.str();
- // } else {
- // Debug("pf::array") << "Need symmetry!" << std::endl;
- // out << "(negsymm _ _ _ " << ss.str() << ")";
- // }
+ if (side != 0) {
+ out << "(negsymm _ _ _ " << ss.str() << ")";
+ } else {
+ out << ss.str();
+ }
out << ")";
- // Unreachable();
+ if (swap) {
+ out << ") ";
+ }
return ret;
}
@@ -1071,13 +1117,12 @@ void ArrayProof::registerTerm(Expr term) {
}
std::string ArrayProof::skolemToLiteral(Expr skolem) {
+ Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl;
Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end());
return d_skolemToLiteral[skolem];
}
void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
- Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl;
-
Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
@@ -1154,7 +1199,21 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& m
void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
Assert (type.isArray() || type.isSort());
- os << type <<" ";
+ if (type.isArray()){
+ ArrayType array_type(type);
+
+ Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: "
+ << array_type.getIndexType()
+ << ", element type: " << array_type.getConstituentType() << std::endl;
+
+ os << "(Array ";
+ printSort(array_type.getIndexType(), os);
+ os << " ";
+ printSort(array_type.getConstituentType(), os);
+ os << ")";
+ } else {
+ os << type <<" ";
+ }
}
void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
@@ -1169,8 +1228,6 @@ void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostrea
void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
// declaring the sorts
- Debug("pf::array") << "Arrays declaring sorts..." << std::endl;
-
for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) {
if (!ProofManager::currentPM()->wasPrinted(*it)) {
os << "(% " << *it << " sort\n";
@@ -1229,6 +1286,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren
void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
Debug("pf::array") << "Array: print deferred declarations called" << std::endl;
+ unsigned count = 1;
for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) {
Expr term = *it;
Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it);
@@ -1237,7 +1295,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
<< "It is a witness for: " << equality << std::endl;
std::ostringstream newSkolemLiteral;
- newSkolemLiteral << ".sl" << d_skolemToLiteral.size();
+ newSkolemLiteral << ".sl" << count++;
std::string skolemLiteral = newSkolemLiteral.str();
d_skolemToLiteral[*it] = skolemLiteral;
@@ -1251,13 +1309,12 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
Node array_two = equality[0][1];
LetMap map;
-
os << "(ext _ _ ";
printTerm(array_one.toExpr(), os, map);
os << " ";
printTerm(array_two.toExpr(), os, map);
os << " (\\ ";
- printTerm(*it, os, map);
+ os << ProofManager::sanitize(*it);
os << " (\\ ";
os << skolemLiteral.c_str();
os << "\n";
@@ -1266,4 +1323,8 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
}
}
+void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* CVC4 namespace */
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index fb25c9433..076ba7381 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,6 +30,32 @@ namespace CVC4 {
//proof object outputted by TheoryARRAY
class ProofArray : public Proof {
private:
+ class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter {
+ public:
+ ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) {
+ }
+
+ std::string printTag(unsigned tag) {
+ if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence";
+ if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality";
+ if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity";
+ if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants";
+ if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity";
+
+ if (tag == d_row) return "Read Over Write";
+ if (tag == d_row1) return "Read Over Write (1)";
+ if (tag == d_ext) return "Extensionality";
+
+ std::ostringstream result;
+ result << tag;
+ return result.str();
+ }
+
+ unsigned d_row;
+ unsigned d_row1;
+ unsigned d_ext;
+ };
+
Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
theory::eq::EqProof* pf,
unsigned tb,
@@ -41,6 +67,8 @@ private:
unsigned d_reasonRow1;
/** Merge tag for EXT applications */
unsigned d_reasonExt;
+
+ ArrayProofPrinter d_proofPrinter;
public:
ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
//it is simply an equality engine proof
@@ -53,6 +81,10 @@ public:
void setRowMergeTag(unsigned tag);
void setRow1MergeTag(unsigned tag);
void setExtMergeTag(unsigned tag);
+
+ unsigned getRowMergeTag() const;
+ unsigned getRow1MergeTag() const;
+ unsigned getExtMergeTag() const;
};
namespace theory {
@@ -91,6 +123,7 @@ public:
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
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 */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4a1f4015d..4e5e98541 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -60,6 +60,7 @@ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
class BitVectorProof : public TheoryProof {
protected:
@@ -108,7 +109,8 @@ public:
virtual void registerTerm(Expr term);
virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
- virtual void printAtomBitblasting(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;
virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
@@ -123,6 +125,12 @@ class LFSCBitVectorProof: public BitVectorProof {
void printPredicate(Expr term, std::ostream& os, const LetMap& map);
void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
void printBitOf(Expr term, std::ostream& os, const LetMap& map);
+
+ ExprToString d_exprToVariableName;
+ ExprToString d_assignedAliases;
+ std::map<std::string, std::string> d_aliasToBindDeclaration;
+ std::string assignAlias(Expr expr);
+ bool hasAlias(Expr expr);
public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
@@ -130,11 +138,13 @@ public:
virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTermBitblasting(Expr term, std::ostream& os);
- virtual void printAtomBitblasting(Expr term, std::ostream& os);
+ virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
+ virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printBitblasting(std::ostream& os, std::ostream& paren);
virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
};
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 19e9cbac9..abe48e3cd 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -19,6 +19,7 @@
#include "proof/clause_id.h"
#include "proof/proof_manager.h"
+#include "proof/proof_utils.h"
#include "proof/theory_proof.h"
#include "prop/cnf_stream.h"
#include "prop/minisat/minisat.h"
@@ -32,7 +33,6 @@ CnfProof::CnfProof(prop::CnfStream* stream,
: d_cnfStream(stream)
, d_clauseToAssertion(ctx)
, d_assertionToProofRule(ctx)
- , d_clauseIdToOwnerTheory(ctx)
, d_currentAssertionStack()
, d_currentDefinitionStack()
, d_clauseToDefinition(ctx)
@@ -103,7 +103,6 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
setClauseAssertion(clause, current_assertion);
setClauseDefinition(clause, current_expr);
- registerExplanationLemma(clause);
}
void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
@@ -143,16 +142,15 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) {
d_assertionToProofRule.insert(assertion, reason);
}
-void CnfProof::registerExplanationLemma(ClauseId clauseId) {
- d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory());
+LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
+ Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
+ return d_lemmaToProofRecipe[lemma];
}
-theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) {
- Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end());
- return d_clauseIdToOwnerTheory[clause];
+bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
+ return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
}
-
void CnfProof::setCnfDependence(Node from, Node to) {
Debug("proof:cnf") << "CnfProof::setCnfDependence "
<< "from " << from << std::endl
@@ -183,12 +181,10 @@ Node CnfProof::getCurrentAssertion() {
return d_currentAssertionStack.back();
}
-void CnfProof::setExplainerTheory(theory::TheoryId theory) {
- d_explainerTheory = theory;
-}
-
-theory::TheoryId CnfProof::getExplainerTheory() {
- return d_explainerTheory;
+void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
+ Assert(proofRecipe);
+ Assert(proofRecipe->getNumSteps() > 0);
+ d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
}
void CnfProof::pushCurrentDefinition(Node definition) {
@@ -212,22 +208,19 @@ Node CnfProof::getCurrentDefinition() {
return d_currentDefinitionStack.back();
}
-
Node CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
Node node = d_cnfStream->getNode(lit);
return node;
}
-
void CnfProof::collectAtoms(const prop::SatClause* clause,
- NodeSet& atoms) {
+ std::set<Node>& atoms) {
for (unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = clause->operator[](i);
prop::SatVariable var = lit.getSatVariable();
TNode atom = getAtom(var);
if (atoms.find(atom) == atoms.end()) {
- Assert (atoms.find(atom) == atoms.end());
atoms.insert(atom);
}
}
@@ -237,14 +230,75 @@ prop::SatLiteral CnfProof::getLiteral(TNode atom) {
return d_cnfStream->getLiteral(atom);
}
+bool CnfProof::hasLiteral(TNode atom) {
+ return d_cnfStream->hasLiteral(atom);
+}
+
+void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) {
+ d_cnfStream->ensureLiteral(atom, noPreregistration);
+}
+
void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses,
- NodeSet& atom_map) {
+ std::set<Node>& atoms) {
IdToSatClause::const_iterator it = clauses.begin();
for (; it != clauses.end(); ++it) {
const prop::SatClause* clause = it->second;
- collectAtoms(clause, atom_map);
+ collectAtoms(clause, atoms);
}
+}
+
+void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+ std::set<Node>& atoms,
+ NodePairSet& rewrites) {
+ IdToSatClause::const_iterator it = lemmaClauses.begin();
+ for (; it != lemmaClauses.end(); ++it) {
+ const prop::SatClause* clause = it->second;
+
+ // TODO: just calculate the map from ID to recipe once,
+ // instead of redoing this over and over again
+ std::vector<Expr> clause_expr;
+ std::set<Node> clause_expr_nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+ if (atom.isConst()) {
+ Assert (atom == utils::mkTrue());
+ continue;
+ }
+ clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes);
+ for (unsigned i = 0; i < recipe.getNumSteps(); ++i) {
+ const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i);
+ Node atom = proofStep->getLiteral();
+
+ if (atom == Node()) {
+ // The last proof step always has the empty node as its target...
+ continue;
+ }
+
+ if (atom.getKind() == kind::NOT) {
+ atom = atom[0];
+ }
+
+ atoms.insert(atom);
+ }
+
+ LemmaProofRecipe::RewriteIterator rewriteIt;
+ for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) {
+ rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second));
+
+ // The unrewritten terms also need to have literals, so insert them into atoms
+ Node rewritten = rewriteIt->first;
+ if (rewritten.getKind() == kind::NOT) {
+ rewritten = rewritten[0];
+ }
+ atoms.insert(rewritten);
+ }
+ }
}
void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
@@ -263,13 +317,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
}
}
-void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) {
- NodeSet::const_iterator it = atoms.begin();
- NodeSet::const_iterator end = atoms.end();
+ std::set<Node>::const_iterator it = atoms.begin();
+ std::set<Node>::const_iterator end = atoms.end();
- for (;it != end; ++it) {
+ for (;it != end; ++it) {
os << "(decl_atom ";
Node atom = *it;
prop::SatVariable var = getLiteral(atom).getSatVariable();
@@ -277,8 +331,8 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
pe->printLetTerm(atom.toExpr(), os);
- os << " (\\ " << ProofManager::getVarName(var, d_name)
- << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+ os << " (\\ " << ProofManager::getVarName(var, d_name);
+ os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
paren << ")))";
}
}
@@ -304,6 +358,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
const prop::SatClause* clause,
std::ostream& os,
std::ostream& paren) {
+ Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting "
+ << std::endl;
+
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
@@ -336,6 +393,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
// and prints the proof of the top-level formula
bool is_input = printProofTopLevel(base_assertion, os_base);
+ if (is_input) {
+ Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
+ }
+
//get base assertion with polarity
bool base_pol = base_assertion.getKind()!=kind::NOT;
base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
@@ -564,6 +625,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
if( !pols[0] || num_nots_1==1 ){
os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
}else{
+ Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
}
Assert( elimNum!=0 );
@@ -662,6 +724,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
os << ")" << clause_paren.str()
<< " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
+
paren << "))";
}
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index a21cb1c0e..62036ced0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -27,6 +27,7 @@
#include "context/cdhashmap.h"
#include "proof/clause_id.h"
+#include "proof/lemma_proof.h"
#include "proof/sat_proof.h"
#include "util/proof.h"
@@ -43,7 +44,9 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
-typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory;
+typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
class CnfProof {
protected:
@@ -55,11 +58,8 @@ protected:
/** Map from assertion to reason for adding assertion **/
NodeToProofRule d_assertionToProofRule;
- /** Map from assertion to the theory that added this assertion **/
- ClauseIdToTheory d_clauseIdToOwnerTheory;
-
- /** The last theory to explain a lemma **/
- theory::TheoryId d_explainerTheory;
+ /** Map from lemma to the recipe for proving it **/
+ LemmaToRecipe d_lemmaToProofRecipe;
/** Top of stack is assertion currently being converted to CNF **/
std::vector<Node> d_currentAssertionStack;
@@ -91,10 +91,16 @@ public:
Node getAtom(prop::SatVariable var);
prop::SatLiteral getLiteral(TNode node);
+ bool hasLiteral(TNode node);
+ void ensureLiteral(TNode node, bool noPreregistration = false);
+
void collectAtoms(const prop::SatClause* clause,
- NodeSet& atoms);
+ std::set<Node>& atoms);
void collectAtomsForClauses(const IdToSatClause& clauses,
- NodeSet& atoms);
+ std::set<Node>& atoms);
+ void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+ std::set<Node>& atoms,
+ NodePairSet& rewrites);
void collectAssertionsForClauses(const IdToSatClause& clauses,
NodeSet& assertions);
@@ -121,11 +127,9 @@ public:
void popCurrentDefinition();
Node getCurrentDefinition();
- void setExplainerTheory(theory::TheoryId theory);
- theory::TheoryId getExplainerTheory();
- theory::TheoryId getOwnerTheory(ClauseId clause);
-
- void registerExplanationLemma(ClauseId clauseId);
+ void setProofRecipe(LemmaProofRecipe* proofRecipe);
+ LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
+ bool haveProofRecipe(const std::set<Node> &lemma);
// accessors for the leaf assertions that are being converted to CNF
bool isAssertion(Node node);
@@ -134,7 +138,7 @@ public:
Node getAssertionForClause(ClauseId clause);
/** Virtual methods for printing things **/
- virtual void printAtomMapping(const NodeSet& atoms,
+ virtual void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) = 0;
@@ -161,7 +165,7 @@ public:
{}
~LFSCCnfProof() {}
- void printAtomMapping(const NodeSet& atoms,
+ void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren);
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
new file mode 100644
index 000000000..a12a516cf
--- /dev/null
+++ b/src/proof/lemma_proof.cpp
@@ -0,0 +1,193 @@
+/********************* */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "proof/lemma_proof.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) :
+ d_theory(theory), d_literalToProve(literalToProve) {
+}
+
+theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const {
+ return d_theory;
+}
+
+Node LemmaProofRecipe::ProofStep::getLiteral() const {
+ return d_literalToProve;
+}
+
+void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) {
+ d_assertions.insert(assertion);
+}
+
+std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const {
+ return d_assertions;
+}
+
+void LemmaProofRecipe::addStep(ProofStep& proofStep) {
+ std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin();
+ d_proofSteps.push_front(proofStep);
+}
+
+std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const {
+ Assert(index < d_proofSteps.size());
+
+ std::set<Node> existingAssertions = getBaseAssertions();
+
+ std::list<ProofStep>::const_iterator step = d_proofSteps.begin();
+ while (index != 0) {
+ existingAssertions.insert(step->getLiteral().negate());
+ ++step;
+ --index;
+ }
+
+ std::set<Node> neededAssertions = step->getAssertions();
+
+ std::set<Node> result;
+ std::set_difference(neededAssertions.begin(), neededAssertions.end(),
+ existingAssertions.begin(), existingAssertions.end(),
+ std::inserter(result, result.begin()));
+ return result;
+}
+
+void LemmaProofRecipe::dump(const char *tag) const {
+
+ if (d_proofSteps.size() == 1) {
+ Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl;
+ }
+
+ unsigned count = 1;
+ Debug(tag) << "Base assertions:" << std::endl;
+ for (std::set<Node>::iterator baseIt = d_baseAssertions.begin();
+ baseIt != d_baseAssertions.end();
+ ++baseIt) {
+ Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl;
+ ++count;
+ }
+
+ Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl;
+
+ count = 1;
+ for (std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) {
+ Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] ";
+ if (step->getLiteral() == Node()) {
+ Debug(tag) << "Contradiction";
+ } else {
+ Debug(tag) << step->getLiteral();
+ }
+
+ Debug(tag) << std::endl;
+
+ std::set<Node> missingAssertions = getMissingAssertionsForStep(count - 1);
+ for (std::set<Node>::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) {
+ Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl;
+ }
+
+ Debug(tag) << std::endl;
+ ++count;
+ }
+
+ if (!d_assertionToExplanation.empty()) {
+ Debug(tag) << std::endl << "Rewrites used:" << std::endl;
+ count = 1;
+ for (std::map<Node, Node>::const_iterator rewrite = d_assertionToExplanation.begin();
+ rewrite != d_assertionToExplanation.end();
+ ++rewrite) {
+ Debug(tag) << "\tRewrite #" << count << ":" << std::endl
+ << "\t\t" << rewrite->first
+ << std::endl << "\t\trewritten into" << std::endl
+ << "\t\t" << rewrite->second
+ << std::endl << std::endl;
+ ++count;
+ }
+ }
+}
+
+void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) {
+ d_baseAssertions.insert(baseAssertion);
+}
+
+std::set<Node> LemmaProofRecipe::getBaseAssertions() const {
+ return d_baseAssertions;
+}
+
+theory::TheoryId LemmaProofRecipe::getTheory() const {
+ Assert(d_proofSteps.size() > 0);
+ return d_proofSteps.back().getTheory();
+}
+
+void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) {
+ if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) {
+ Assert(d_assertionToExplanation[assertion] == explanation);
+ }
+
+ d_assertionToExplanation[assertion] = explanation;
+}
+
+bool LemmaProofRecipe::wasRewritten(Node assertion) const {
+ return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end();
+}
+
+Node LemmaProofRecipe::getExplanation(Node assertion) const {
+ Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end());
+ return d_assertionToExplanation.find(assertion)->second;
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const {
+ return d_assertionToExplanation.begin();
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const {
+ return d_assertionToExplanation.end();
+}
+
+bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const {
+ return d_baseAssertions < other.d_baseAssertions;
+ }
+
+bool LemmaProofRecipe::simpleLemma() const {
+ return d_proofSteps.size() == 1;
+}
+
+bool LemmaProofRecipe::compositeLemma() const {
+ return !simpleLemma();
+}
+
+const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const {
+ Assert(index < d_proofSteps.size());
+
+ std::list<ProofStep>::const_iterator it = d_proofSteps.begin();
+ while (index != 0) {
+ ++it;
+ --index;
+ }
+
+ return &(*it);
+}
+
+LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) {
+ Assert(index < d_proofSteps.size());
+
+ std::list<ProofStep>::iterator it = d_proofSteps.begin();
+ while (index != 0) {
+ ++it;
+ --index;
+ }
+
+ return &(*it);
+}
+
+unsigned LemmaProofRecipe::getNumSteps() const {
+ return d_proofSteps.size();
+}
+
+} /* namespace CVC4 */
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h
new file mode 100644
index 000000000..e96ff5337
--- /dev/null
+++ b/src/proof/lemma_proof.h
@@ -0,0 +1,79 @@
+/********************* */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__LEMMA_PROOF_H
+#define __CVC4__LEMMA_PROOF_H
+
+#include "expr/expr.h"
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+#include "util/proof.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class LemmaProofRecipe {
+public:
+ class ProofStep {
+ public:
+ ProofStep(theory::TheoryId theory, Node literalToProve);
+ theory::TheoryId getTheory() const;
+ Node getLiteral() const;
+ void addAssertion(const Node& assertion);
+ std::set<Node> getAssertions() const;
+
+ private:
+ theory::TheoryId d_theory;
+ Node d_literalToProve;
+ std::set<Node> d_assertions;
+ };
+
+ //* The lemma assertions and owner */
+ void addBaseAssertion(Node baseAssertion);
+ std::set<Node> getBaseAssertions() const;
+ theory::TheoryId getTheory() const;
+
+ //* Rewrite rules */
+ typedef std::map<Node, Node>::const_iterator RewriteIterator;
+ RewriteIterator rewriteBegin() const;
+ RewriteIterator rewriteEnd() const;
+
+ void addRewriteRule(Node assertion, Node explanation);
+ bool wasRewritten(Node assertion) const;
+ Node getExplanation(Node assertion) const;
+
+ //* Proof Steps */
+ void addStep(ProofStep& proofStep);
+ const ProofStep* getStep(unsigned index) const;
+ ProofStep* getStep(unsigned index);
+ unsigned getNumSteps() const;
+ std::set<Node> getMissingAssertionsForStep(unsigned index) const;
+ bool simpleLemma() const;
+ bool compositeLemma() const;
+
+ void dump(const char *tag) const;
+ bool operator<(const LemmaProofRecipe& other) const;
+
+private:
+ //* The list of assertions for this lemma */
+ std::set<Node> d_baseAssertions;
+
+ //* The various steps needed to derive the empty clause */
+ std::list<ProofStep> d_proofSteps;
+
+ //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
+ std::map<Node, Node> d_assertionToExplanation;
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index a3689d746..5ce8b523f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -200,7 +200,6 @@ std::string ProofManager::getLitName(prop::SatLiteral lit,
return append(prefix+".l", lit.toInt());
}
-
std::string ProofManager::getPreprocessedAssertionName(Node node,
const std::string& prefix) {
node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
@@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom,
Assert(!lit.isNegated());
return getAtomName(lit.getSatVariable(), prefix);
}
+
std::string ProofManager::getLitName(TNode lit,
const std::string& prefix) {
- return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+ std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+ if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) {
+ return currentPM()->d_rewriteFilters[litName];
+ }
+
+ return litName;
}
std::string ProofManager::sanitize(TNode node) {
@@ -331,6 +336,9 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine,
{}
void LFSCProof::toStream(std::ostream& out) {
+
+ Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
+
d_satProof->constructProof();
// collecting leaf clauses in resolution proof
@@ -384,8 +392,37 @@ void LFSCProof::toStream(std::ostream& out) {
for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
- NodeSet atoms;
+ std::set<Node> atoms;
+ NodePairSet rewrites;
// collects the atoms in the clauses
+ d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
+
+ if (!rewrites.empty()) {
+ Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
+ NodePairSet::const_iterator rewriteIt;
+ for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
+ Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
+ }
+ Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
+ } else {
+ Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
+ }
+
+ // The derived/unrewritten atoms may not have CNF literals required later on.
+ // If they don't, add them.
+ std::set<Node>::const_iterator it;
+ for (it = atoms.begin(); it != atoms.end(); ++it) {
+ Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
+ if (!d_cnfProof->hasLiteral(*it)) {
+ // For arithmetic: these literals are not normalized, causing an error in Arith.
+ if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
+ d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
+ } else {
+ d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
+ }
+ }
+ }
+
d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
@@ -393,38 +430,23 @@ void LFSCProof::toStream(std::ostream& out) {
for (NodeSet::const_iterator it = used_assertions.begin();
it != used_assertions.end(); ++it) {
utils::collectAtoms(*it, atoms);
+ // utils::collectAtoms(*it, newAtoms);
}
- NodeSet::iterator atomIt;
- Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl;
+ std::set<Node>::iterator atomIt;
+ Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
+ << std::endl << std::endl;
for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
-
- if (Debug.isOn("proof:pm")) {
- // std::cout << NodeManager::currentNM();
- Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl;
- for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) {
- Debug("proof:pm") << " " << *it << std::endl;
- }
-
- Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl;
- for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) {
- Debug("proof:pm") << " " << *it << std::endl;
- }
- }
}
-
smt::SmtScope scope(d_smtEngine);
std::ostringstream paren;
out << "(check\n";
out << " ;; Declarations\n";
// declare the theory atoms
- NodeSet::const_iterator it = atoms.begin();
- NodeSet::const_iterator end = atoms.end();
-
Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
- for(; it != end; ++it) {
+ for(it = atoms.begin(); it != atoms.end(); ++it) {
Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
d_theoryProof->registerTerm((*it).toExpr());
}
@@ -444,9 +466,15 @@ void LFSCProof::toStream(std::ostream& out) {
out << "(: (holds cln)\n\n";
// Have the theory proofs print deferred declarations, e.g. for skolem variables.
- out << " ;; Printing deferred declarations \n";
+ out << " ;; Printing deferred declarations \n\n";
d_theoryProof->printDeferredDeclarations(out, paren);
+ out << " ;; Printing aliasing declarations \n\n";
+ d_theoryProof->printAliasingDeclarations(out, paren);
+
+ out << " ;; Rewrites for Lemmas \n";
+ d_theoryProof->printLemmaRewrites(rewrites, out, paren);
+
// print trust that input assertions are their preprocessed form
printPreprocessedAssertions(used_assertions, out, paren);
@@ -464,10 +492,6 @@ void LFSCProof::toStream(std::ostream& out) {
Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
- // FIXME: for now assume all theory lemmas are in CNF form so
- // distinguish between them and inputs
- // print theory lemmas for resolution proof
-
Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
@@ -496,6 +520,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
NodeSet::const_iterator it = assertions.begin();
NodeSet::const_iterator end = assertions.end();
+ Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
+
for (; it != end; ++it) {
os << "(th_let_pf _ ";
@@ -506,7 +532,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
paren << "))";
-
}
os << "\n";
@@ -568,6 +593,14 @@ void ProofManager::markPrinted(const Type& type) {
d_printedTypes.insert(type);
}
+void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
+ d_rewriteFilters[original] = substitute;
+}
+
+void ProofManager::clearRewriteFilters() {
+ d_rewriteFilters.clear();
+}
+
std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
switch(k) {
case RULE_GIVEN:
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c74aac237..c6454b652 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -34,6 +34,8 @@
namespace CVC4 {
+class SmtGlobals;
+
// forward declarations
namespace Minisat {
class Solver;
@@ -136,6 +138,8 @@ class ProofManager {
std::set<Type> d_printedTypes;
+ std::map<std::string, std::string> d_rewriteFilters;
+
protected:
LogicInfo d_logic;
@@ -224,6 +228,9 @@ public:
void markPrinted(const Type& type);
bool wasPrinted(const Type& type) const;
+ void addRewriteFilter(const std::string &original, const std::string &substitute);
+ void clearRewriteFilters();
+
};/* class ProofManager */
class LFSCProof : public Proof {
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
new file mode 100644
index 000000000..6d729db1f
--- /dev/null
+++ b/src/proof/proof_output_channel.cpp
@@ -0,0 +1,82 @@
+/********************* */
+/*! \file proof_output_channel.cpp
+** \verbatim
+** \brief [[ Add one-line brief description here ]]
+**
+** [[ Add lengthier description here ]]
+** \todo document this file
+**/
+
+#include "base/cvc4_assert.h"
+#include "proof_output_channel.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+
+ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
+
+void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
+ Assert(d_conflict.isNull());
+ Assert(!n.isNull());
+ d_conflict = n;
+ Assert(pf != NULL);
+ d_proof = pf;
+}
+
+bool ProofOutputChannel::propagate(TNode x) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl;
+ d_propagations.insert(x);
+ return true;
+}
+
+theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
+ d_lemma = n;
+ return theory::LemmaStatus(TNode::null(), 0);
+}
+
+theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() {
+ AlwaysAssert(false);
+ return theory::LemmaStatus(TNode::null(), 0);
+}
+
+void ProofOutputChannel::requirePhase(TNode n, bool b) throw() {
+ Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
+ Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
+}
+
+bool ProofOutputChannel::flipDecision() throw() {
+ Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
+ AlwaysAssert(false);
+ return false;
+}
+
+void ProofOutputChannel::setIncomplete() throw() {
+ Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
+ AlwaysAssert(false);
+}
+
+
+MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory)
+ : d_theory(theory)
+ , d_visited() {
+}
+
+bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
+ return d_visited.find(current) != d_visited.end();
+}
+
+void MyPreRegisterVisitor::visit(TNode current, TNode parent) {
+ d_theory->preRegisterTerm(current);
+ d_visited.insert(current);
+}
+
+void MyPreRegisterVisitor::start(TNode node) {
+}
+
+void MyPreRegisterVisitor::done(TNode node) {
+}
+
+} /* namespace CVC4 */
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
new file mode 100644
index 000000000..b85af5fb5
--- /dev/null
+++ b/src/proof/proof_output_channel.h
@@ -0,0 +1,50 @@
+/********************* */
+/*! \file proof_output_channel.h
+ ** \verbatim
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
+#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+
+class ProofOutputChannel : public theory::OutputChannel {
+public:
+ Node d_conflict;
+ Proof* d_proof;
+ Node d_lemma;
+ std::set<Node> d_propagations;
+
+ ProofOutputChannel();
+
+ virtual ~ProofOutputChannel() throw() {}
+
+ void conflict(TNode n, Proof* pf) throw();
+ bool propagate(TNode x) throw();
+ theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw();
+ theory::LemmaStatus splitLemma(TNode, bool) throw();
+ void requirePhase(TNode n, bool b) throw();
+ bool flipDecision() throw();
+ void setIncomplete() throw();
+};/* class ProofOutputChannel */
+
+class MyPreRegisterVisitor {
+ theory::Theory* d_theory;
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+public:
+ typedef void return_type;
+ MyPreRegisterVisitor(theory::Theory* theory);
+ bool alreadyVisited(TNode current, TNode parent);
+ void visit(TNode current, TNode parent);
+ void start(TNode node);
+ void done(TNode node);
+}; /* class MyPreRegisterVisitor */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp
index 5b04c281d..fe0d42242 100644
--- a/src/proof/proof_utils.cpp
+++ b/src/proof/proof_utils.cpp
@@ -21,14 +21,14 @@
namespace CVC4 {
namespace utils {
-void collectAtoms(TNode node, CVC4::NodeSet& seen) {
+void collectAtoms(TNode node, std::set<Node>& seen) {
if (seen.find(node) != seen.end())
return;
if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) {
seen.insert(node);
return;
}
-
+
for (unsigned i = 0; i < node.getNumChildren(); ++i) {
collectAtoms(node[i], seen);
}
@@ -47,23 +47,23 @@ std::string toLFSCKind(Kind kind) {
// bit-vector kinds
case kind::BITVECTOR_AND :
- return "bvand";
+ return "bvand";
case kind::BITVECTOR_OR :
- return "bvor";
+ return "bvor";
case kind::BITVECTOR_XOR :
- return "bvxor";
+ return "bvxor";
case kind::BITVECTOR_NAND :
- return "bvnand";
+ return "bvnand";
case kind::BITVECTOR_NOR :
- return "bvnor";
+ return "bvnor";
case kind::BITVECTOR_XNOR :
- return "bvxnor";
+ return "bvxnor";
case kind::BITVECTOR_COMP :
- return "bvcomp";
+ return "bvcomp";
case kind::BITVECTOR_MULT :
return "bvmul";
case kind::BITVECTOR_PLUS :
- return "bvadd";
+ return "bvadd";
case kind::BITVECTOR_SUB :
return "bvsub";
case kind::BITVECTOR_UDIV :
@@ -71,49 +71,49 @@ std::string toLFSCKind(Kind kind) {
return "bvudiv";
case kind::BITVECTOR_UREM :
case kind::BITVECTOR_UREM_TOTAL :
- return "bvurem";
+ return "bvurem";
case kind::BITVECTOR_SDIV :
- return "bvsdiv";
+ return "bvsdiv";
case kind::BITVECTOR_SREM :
return "bvsrem";
case kind::BITVECTOR_SMOD :
- return "bvsmod";
+ return "bvsmod";
case kind::BITVECTOR_SHL :
- return "bvshl";
+ return "bvshl";
case kind::BITVECTOR_LSHR :
return "bvlshr";
case kind::BITVECTOR_ASHR :
return "bvashr";
case kind::BITVECTOR_CONCAT :
- return "concat";
+ return "concat";
case kind::BITVECTOR_NEG :
- return "bvneg";
+ return "bvneg";
case kind::BITVECTOR_NOT :
- return "bvnot";
+ return "bvnot";
case kind::BITVECTOR_ROTATE_LEFT :
- return "rotate_left";
+ return "rotate_left";
case kind::BITVECTOR_ROTATE_RIGHT :
return "rotate_right";
case kind::BITVECTOR_ULT :
- return "bvult";
+ return "bvult";
case kind::BITVECTOR_ULE :
- return "bvule";
+ return "bvule";
case kind::BITVECTOR_UGT :
return "bvugt";
case kind::BITVECTOR_UGE :
return "bvuge";
case kind::BITVECTOR_SLT :
- return "bvslt";
+ return "bvslt";
case kind::BITVECTOR_SLE :
- return "bvsle";
+ return "bvsle";
case kind::BITVECTOR_SGT :
- return "bvsgt";
+ return "bvsgt";
case kind::BITVECTOR_SGE :
- return "bvsge";
+ return "bvsge";
case kind::BITVECTOR_EXTRACT :
- return "extract";
+ return "extract";
case kind::BITVECTOR_REPEAT :
- return "repeat";
+ return "repeat";
case kind::BITVECTOR_ZERO_EXTEND :
return "zero_extend";
case kind::BITVECTOR_SIGN_EXTEND :
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index da10c33a0..8c734c892 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -17,7 +17,7 @@
#include "cvc4_private.h"
-#pragma once
+#pragma once
#include <set>
#include <vector>
@@ -29,6 +29,9 @@ namespace CVC4 {
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
+
namespace utils {
std::string toLFSCKind(Kind kind);
@@ -42,7 +45,7 @@ inline unsigned getExtractLow(Expr node) {
}
inline unsigned getSize(Type type) {
- BitVectorType bv(type);
+ BitVectorType bv(type);
return bv.getSize();
}
@@ -60,8 +63,8 @@ inline Expr mkFalse() {
return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
}
inline BitVector mkBitVectorOnes(unsigned size) {
- Assert(size > 0);
- return BitVector(1, Integer(1)).signExtend(size - 1);
+ Assert(size > 0);
+ return BitVector(1, Integer(1)).signExtend(size - 1);
}
inline Expr mkExpr(Kind k , Expr expr) {
@@ -73,16 +76,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) {
inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
}
-
-
+
+
inline Expr mkOnes(unsigned size) {
- BitVector val = mkBitVectorOnes(size);
- return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+ BitVector val = mkBitVectorOnes(size);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
}
inline Expr mkConst(unsigned size, unsigned int value) {
BitVector val(size, value);
- return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
}
inline Expr mkConst(const BitVector& value) {
@@ -92,14 +95,14 @@ inline Expr mkConst(const BitVector& value) {
inline Expr mkOr(const std::vector<Expr>& nodes) {
std::set<Expr> all;
all.insert(nodes.begin(), nodes.end());
- Assert(all.size() != 0 );
+ Assert(all.size() != 0 );
if (all.size() == 1) {
// All the same, or just one
return nodes[0];
}
-
-
+
+
NodeBuilder<> disjunction(kind::OR);
std::set<Expr>::const_iterator it = all.begin();
std::set<Expr>::const_iterator it_end = all.end();
@@ -109,23 +112,23 @@ inline Expr mkOr(const std::vector<Expr>& nodes) {
}
Node res = disjunction;
- return res.toExpr();
+ return res.toExpr();
}/* mkOr() */
-
+
inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
std::set<Expr> all;
all.insert(conjunctions.begin(), conjunctions.end());
if (all.size() == 0) {
- return mkTrue();
+ return mkTrue();
}
-
+
if (all.size() == 1) {
// All the same, or just one
return conjunctions[0];
}
-
+
NodeBuilder<> conjunction(kind::AND);
std::set<Expr>::const_iterator it = all.begin();
@@ -135,7 +138,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
++ it;
}
- Node res = conjunction;
+ Node res = conjunction;
return res.toExpr();
}/* mkAnd() */
@@ -144,14 +147,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
all.insert(children.begin(), children.end());
if (all.size() == 0) {
- return mkTrue();
+ return mkTrue();
}
-
+
if (all.size() == 1) {
// All the same, or just one
return children[0];
}
-
+
NodeBuilder<> res(kind);
std::set<Expr>::const_iterator it = all.begin();
@@ -165,13 +168,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
}/* mkSortedNode() */
inline const bool getBit(Expr expr, unsigned i) {
- Assert (i < utils::getSize(expr) &&
- expr.isConst());
+ Assert (i < utils::getSize(expr) &&
+ expr.isConst());
Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
- return (bit == 1u);
+ return (bit == 1u);
}
-void collectAtoms(TNode node, NodeSet& seen);
+void collectAtoms(TNode node, std::set<Node>& seen);
}
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 4f3330ef7..1e01e4dce 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -543,12 +543,9 @@ ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause,
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
d_lemmaClauses.insert(newId);
- Debug("pf::sat")
- << "TSatProof::registerClause registering a new lemma clause: "
- << newId << " = " << *buildClause(newId)
- << ". Explainer theory: " << d_cnfProof->getExplainerTheory()
- << std::endl;
- d_cnfProof->registerExplanationLemma(newId);
+ Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: "
+ << newId << " = " << *buildClause(newId)
+ << std::endl;
}
}
@@ -579,12 +576,10 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
}
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
- "lemma (UNIT CLAUSE): "
- << lit << ". Explainer theory: "
- << d_cnfProof->getExplainerTheory() << std::endl;
+ Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): "
+ << lit
+ << std::endl;
d_lemmaClauses.insert(newId);
- d_cnfProof->registerExplanationLemma(newId);
}
}
ClauseId id = d_unitId[toInt(lit)];
@@ -842,7 +837,7 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
// clause allocator. So reload reason ptr each time.
const typename Solver::TClause& initial_reason = getClause(reason_ref);
size_t current_reason_size = initial_reason.size();
- for (int i = 0; i < current_reason_size; i++) {
+ for (size_t i = 0; i < current_reason_size; i++) {
const typename Solver::TClause& current_reason = getClause(reason_ref);
current_reason_size = current_reason.size();
typename Solver::TLit l = current_reason[i];
@@ -904,7 +899,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
// Here, the call to resolveUnit() can reallocate memory in the
// clause allocator. So reload conflict ptr each time.
size_t conflict_size = getClause(conflict_ref).size();
- for (int i = 0; i < conflict_size; ++i) {
+ for (size_t i = 0; i < conflict_size; ++i) {
const typename Solver::TClause& conflict = getClause(conflict_ref);
typename Solver::TLit lit = conflict[i];
ClauseId res_id = resolveUnit(~lit);
@@ -1106,12 +1101,12 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
}
if (id == this->d_emptyClauseId) {
- out << "(\\empty empty)";
+ out <<"(\\ empty empty)";
return;
}
- out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name
- paren << "))"; // closing parethesis for lemma binding and satlem
+ out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name
+ paren << "))"; // closing parethesis for lemma binding and satlem
}
/// LFSCSatProof class
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index de510e514..b026e21c2 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -37,7 +37,6 @@ public:
Node getSkolem(Node disequality);
Node getDisequality(Node skolem);
bool isSkolem(Node skolem);
-
void clear();
std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 088275b3f..eaf21846b 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -25,6 +25,7 @@
#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/sat_proof.h"
#include "proof/uf_proof.h"
@@ -48,74 +49,6 @@ namespace CVC4 {
unsigned CVC4::LetCount::counter = 0;
static unsigned LET_COUNT = 1;
-//for proof replay
-class ProofOutputChannel : public theory::OutputChannel {
-public:
- Node d_conflict;
- Proof* d_proof;
- Node d_lemma;
-
- ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
- virtual ~ProofOutputChannel() throw() {}
-
- void conflict(TNode n, Proof* pf) throw() {
- Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl;
- Assert(d_conflict.isNull());
- Assert(!n.isNull());
- d_conflict = n;
- Assert(pf != NULL);
- d_proof = pf;
- }
- bool propagate(TNode x) throw() {
- Trace("theory-proof-debug") << "got a propagation: " << x << std::endl;
- return true;
- }
- theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
- Trace("theory-proof-debug") << "new lemma: " << n << std::endl;
- d_lemma = n;
- return theory::LemmaStatus(TNode::null(), 0);
- }
- theory::LemmaStatus splitLemma(TNode, bool) throw() {
- AlwaysAssert(false);
- return theory::LemmaStatus(TNode::null(), 0);
- }
- void requirePhase(TNode n, bool b) throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl;
- Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl;
- }
- bool flipDecision() throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl;
- AlwaysAssert(false);
- return false;
- }
- void setIncomplete() throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl;
- AlwaysAssert(false);
- }
-};/* class ProofOutputChannel */
-
-//for proof replay
-class MyPreRegisterVisitor {
- theory::Theory* d_theory;
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
-public:
- typedef void return_type;
- MyPreRegisterVisitor(theory::Theory* theory)
- : d_theory(theory)
- , d_visited()
- {}
- bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); }
- void visit(TNode current, TNode parent) {
- if(theory::Theory::theoryOf(current) == d_theory->getId()) {
- //Trace("theory-proof-debug") << "preregister " << current << std::endl;
- d_theory->preRegisterTerm(current);
- d_visited.insert(current);
- }
- }
- void start(TNode node) { }
- void done(TNode node) { }
-}; /* class MyPreRegisterVisitor */
-
TheoryProofEngine::TheoryProofEngine()
: d_registrationCache()
, d_theoryProofTable()
@@ -131,13 +64,12 @@ TheoryProofEngine::~TheoryProofEngine() {
}
}
-
void TheoryProofEngine::registerTheory(theory::Theory* th) {
- if( th ){
+ if (th) {
theory::TheoryId id = th->getId();
if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
- Trace("theory-proof-debug") << "; register theory " << id << std::endl;
+ Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
if (id == theory::THEORY_UF) {
d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
@@ -167,19 +99,42 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
}
TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
+ // The UF theory handles queries for the Builtin theory.
+ if (id == theory::THEORY_BUILTIN) {
+ Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl;
+ id = theory::THEORY_UF;
+ }
+
Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end());
return d_theoryProofTable[id];
}
+void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) {
+ d_exprToTheoryIds[term].insert(id);
+}
+
+void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+ LetMap emptyMap;
+
+ os << "(trust_f (not (= _ ";
+ printBoundTerm(c1, os, emptyMap);
+ os << " ";
+ printBoundTerm(c2, os, emptyMap);
+ os << ")))";
+}
+
void TheoryProofEngine::registerTerm(Expr term) {
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
+
if (d_registrationCache.count(term)) {
return;
}
- Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl;
+
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
theory::TheoryId theory_id = theory::Theory::theoryOf(term);
- Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
+ Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
// don't need to register boolean terms
if (theory_id == theory::THEORY_BUILTIN ||
@@ -193,32 +148,38 @@ void TheoryProofEngine::registerTerm(Expr term) {
if (!supportedTheory(theory_id)) return;
+ // Register the term with its owner theory
getTheoryProof(theory_id)->registerTerm(term);
+
+ // A special case: the array theory needs to know of every skolem, even if
+ // it belongs to another theory (e.g., a BV skolem)
+ if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl;
+ getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+ }
+
d_registrationCache.insert(term);
}
-theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) {
ProofManager* pm = ProofManager::currentPM();
- Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
- << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+ std::set<Node> nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+ if (atom.isConst()) {
+ Assert (atom == utils::mkTrue());
+ continue;
+ }
- if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) {
- Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. "
- << "Returning THEORY_ARITH" << std::endl;
- return theory::THEORY_ARITH;
+ nodes.insert(lit.isNegated() ? node.notNode() : node);
}
- return pm->getCnfProof()->getOwnerTheory(id);
-
- // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF;
- // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV;
- // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY;
- // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV;
-
- // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl;
-
- // Unreachable();
+ // Ensure that the lemma is in the database.
+ Assert (pm->getCnfProof()->haveProofRecipe(nodes));
+ return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
}
void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
@@ -272,8 +233,6 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
theory::TheoryId theory_id = theory::Theory::theoryOf(term);
- Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term
- << ", theory_id = " << theory_id << std::endl;
// boolean terms and ITEs are special because they
// are common to all theories
@@ -315,6 +274,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
Unreachable();
}
+void LFSCTheoryProofEngine::performExtraRegistrations() {
+ ExprToTheoryIds::const_iterator it;
+ for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) {
+ if (d_registrationCache.count(it->first)) { // Only register if the term appeared
+ TheoryIdSet::const_iterator theoryIt;
+ for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) {
+ Debug("pf::tp") << "\tExtra registration of term " << it->first
+ << " with theory: " << *theoryIt << std::endl;
+ Assert(supportedTheory(*theoryIt));
+ getTheoryProof(*theoryIt)->registerTerm(it->first);
+ }
+ }
+ }
+}
+
+void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
+ TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+ TheoryProofTable::const_iterator end = d_theoryProofTable.end();
+ for (; it != end; ++it) {
+ it->second->treatBoolsAsFormulas(value);
+ }
+}
+
void LFSCTheoryProofEngine::registerTermsFromAssertions() {
ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
@@ -322,6 +304,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
for(; it != end; ++it) {
registerTerm(*it);
}
+
+ performExtraRegistrations();
}
void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -333,17 +317,43 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
for (; it != end; ++it) {
Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
- // FIXME: merge this with counter
- os << "(% A" << counter++ << " (th_holds ";
+ std::ostringstream name;
+ name << "A" << counter++;
+ os << "(% " << name.str() << " (th_holds ";
printLetTerm(*it, os);
os << ")\n";
paren << ")";
}
- //store map between assertion and counter
- // ProofManager::currentPM()->setAssertion( *it );
+
Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
}
+void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) {
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl;
+
+ NodePairSet::const_iterator it;
+
+ for (it = rewrites.begin(); it != rewrites.end(); ++it) {
+ Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
+
+ std::ostringstream rewriteRule;
+ rewriteRule << ".lrr" << d_assertionToRewrite.size();
+
+ LetMap emptyMap;
+ os << "(th_let_pf _ (trust_f (iff ";
+ printBoundTerm(it->second.toExpr(), os, emptyMap);
+ os << " ";
+ printBoundTerm(it->first.toExpr(), os, emptyMap);
+ os << ")) (\\ " << rewriteRule.str() << "\n";
+
+ d_assertionToRewrite[it->first] = rewriteRule.str();
+ Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
+ paren << "))";
+ }
+
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl;
+}
+
void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) {
Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl;
@@ -378,55 +388,148 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
}
}
-void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
- std::ostream& os,
- std::ostream& paren) {
- os << " ;; Theory Lemmas \n";
- ProofManager* pm = ProofManager::currentPM();
- IdToSatClause::const_iterator it = lemmas.begin();
- IdToSatClause::const_iterator end = lemmas.end();
-
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
+ TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+ TheoryProofTable::const_iterator end = d_theoryProofTable.end();
for (; it != end; ++it) {
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
- ClauseId id = it->first;
- Debug("pf::tp") << "\tLemma = " << id
- << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+ it->second->printAliasingDeclarations(os, paren);
}
- it = lemmas.begin();
+}
- // BitVector theory is special case: must know all
- // conflicts needed ahead of time for resolution
- // proof lemmas
- std::vector<Expr> bv_lemmas;
- for (; it != end; ++it) {
+void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
+ Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+
+ ProofManager* pm = ProofManager::currentPM();
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
ClauseId id = it->first;
+ Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl;
const prop::SatClause* clause = it->second;
+ std::set<Node> nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ if (node.isConst()) {
+ Assert (node.toExpr() == utils::mkTrue());
+ continue;
+ }
+ nodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes);
+ recipe.dump("pf::dumpLemmas");
+ }
- theory::TheoryId theory_id = getTheoryForLemma(id);
- if (theory_id != theory::THEORY_BV) continue;
+ Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl;
+}
+
+// TODO: this function should be moved into the BV prover.
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+ // BitVector theory is special case: must know all conflicts needed
+ // ahead of time for resolution proof lemmas
+ std::vector<Expr> bv_lemmas;
+
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+ const prop::SatClause* clause = it->second;
std::vector<Expr> conflict;
+ std::set<Node> conflictNodes;
for(unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = (*clause)[i];
- Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+ Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+
+ // The literals (true) and (not false) are omitted from conflicts
if (atom.isConst()) {
Assert (atom == utils::mkTrue() ||
(atom == utils::mkFalse() && lit.isNegated()));
continue;
}
+
Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
conflict.push_back(expr_lit);
+ conflictNodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes);
+
+ unsigned numberOfSteps = recipe.getNumSteps();
+
+ prop::SatClause currentClause = *clause;
+ std::vector<Expr> currentClauseExpr = conflict;
+
+ for (unsigned i = 0; i < numberOfSteps; ++i) {
+ const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+ if (currentStep->getTheory() != theory::THEORY_BV) {
+ continue;
+ }
+
+ // If any rewrites took place, we need to update the conflict clause accordingly
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+ std::map<Node, Node> explanationToMissingAssertion;
+ std::set<Node>::iterator assertionIt;
+ for (assertionIt = missingAssertions.begin();
+ assertionIt != missingAssertions.end();
+ ++assertionIt) {
+ Node negated = (*assertionIt).negate();
+ explanationToMissingAssertion[recipe.getExplanation(negated)] = negated;
+ }
+
+ currentClause = *clause;
+ currentClauseExpr = conflict;
+
+ for (unsigned j = 0; j < i; ++j) {
+ // Literals already used in previous steps need to be negated
+ Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+
+ // If this literal is the result of a rewrite, we need to translate it
+ if (explanationToMissingAssertion.find(previousLiteralNode) !=
+ explanationToMissingAssertion.end()) {
+ previousLiteralNode = explanationToMissingAssertion[previousLiteralNode];
+ }
+
+ Node previousLiteralNodeNegated = previousLiteralNode.negate();
+ prop::SatLiteral previousLiteralNegated =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+
+ currentClause.push_back(previousLiteralNegated);
+ currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+ }
+
+ // If we're in the final step, the last literal is Null and should not be added.
+ // Otherwise, the current literal does NOT need to be negated
+ Node currentLiteralNode = currentStep->getLiteral();
+
+ if (currentLiteralNode != Node()) {
+ prop::SatLiteral currentLiteral =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+ currentClause.push_back(currentLiteral);
+ currentClauseExpr.push_back(currentLiteralNode.toExpr());
+ }
+
+ bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr));
}
- bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict));
}
- // FIXME: ugly, move into bit-vector proof by adding lemma
- // queue inside each theory_proof
+
BitVectorProof* bv = ProofManager::getBitVectorProof();
bv->finalizeConflicts(bv_lemmas);
-
bv->printResolutionProof(os, paren);
+}
+
+void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
+ std::ostream& os,
+ std::ostream& paren) {
+ os << " ;; Theory Lemmas \n";
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
+
+ if (Debug.isOn("pf::dumpLemmas")) {
+ dumpTheoryLemmas(lemmas);
+ }
+
+ finalizeBvConflicts(lemmas, os, paren);
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
Assert (lemmas.size() == 1);
@@ -434,54 +537,247 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
return;
}
- it = lemmas.begin();
-
+ ProofManager* pm = ProofManager::currentPM();
Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
- for (; it != end; ++it) {
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl;
-
- // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl;
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
ClauseId id = it->first;
- Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
const prop::SatClause* clause = it->second;
- // printing clause as it appears in resolution proof
- os << "(satlem _ _ ";
- std::ostringstream clause_paren;
- Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
- pm->getCnfProof()->printClause(*clause, os, clause_paren);
- Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl;
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
+ << id << std::endl;
std::vector<Expr> clause_expr;
+ std::set<Node> clause_expr_nodes;
for(unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = (*clause)[i];
- Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
if (atom.isConst()) {
Assert (atom == utils::mkTrue());
continue;
}
Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
clause_expr.push_back(expr_lit);
+ clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
}
- Debug("pf::tp") << "Expression printing done!" << std::endl;
-
- // query appropriate theory for proof of clause
- theory::TheoryId theory_id = getTheoryForLemma(id);
- Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
- Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl;
- getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
- Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
- // os << " (clausify_false trust)";
- os << clause_paren.str();
- os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
- paren << "))";
+ LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes);
+
+ if (recipe.simpleLemma()) {
+ // In a simple lemma, there will be no propositional resolution in the end
+
+ Debug("pf::tp") << "Simple lemma" << std::endl;
+ // Printing the clause as it appears in resolution proof
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+ pm->getCnfProof()->printClause(*clause, os, clause_paren);
+
+ // Find and handle missing assertions, due to rewrites
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0);
+ if (!missingAssertions.empty()) {
+ Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl;
+ }
+
+ std::set<Node>::const_iterator missingAssertion;
+ for (missingAssertion = missingAssertions.begin();
+ missingAssertion != missingAssertions.end();
+ ++missingAssertion) {
+
+ Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+ Assert(recipe.wasRewritten(missingAssertion->negate()));
+ Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+ Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+ // We have a missing assertion.
+ // rewriteIt->first is the assertion after the rewrite (the explanation),
+ // rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+ bool found = false;
+ unsigned k;
+ for (k = 0; k < clause_expr.size(); ++k) {
+ if (clause_expr[k] == explanation.toExpr()) {
+ found = true;
+ break;
+ }
+ }
+
+ Assert(found);
+ Debug("pf::tp") << "Replacing theory assertion "
+ << clause_expr[k]
+ << " with "
+ << *missingAssertion
+ << std::endl;
+
+ clause_expr[k] = missingAssertion->toExpr();
+
+ std::ostringstream rewritten;
+ rewritten << "(or_elim_1 _ _ ";
+ rewritten << "(not_not_intro _ ";
+ rewritten << pm->getLitName(explanation);
+ rewritten << ") (iff_elim_1 _ _ ";
+ rewritten << d_assertionToRewrite[missingAssertion->negate()];
+ rewritten << "))";
+
+ Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+ << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+ << std::endl << std::endl;
+
+ pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+ }
+
+ // Query the appropriate theory for a proof of this clause
+ theory::TheoryId theory_id = getTheoryForLemma(clause);
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+ getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
+
+ // Turn rewrite filter OFF
+ pm->clearRewriteFilters();
+
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+ os << clause_paren.str();
+ os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
+ paren << "))";
+ } else { // This is a composite lemma
+
+ unsigned numberOfSteps = recipe.getNumSteps();
+ prop::SatClause currentClause = *clause;
+ std::vector<Expr> currentClauseExpr = clause_expr;
+
+ for (unsigned i = 0; i < numberOfSteps; ++i) {
+ const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+ currentClause = *clause;
+ currentClauseExpr = clause_expr;
+
+ for (unsigned j = 0; j < i; ++j) {
+ // Literals already used in previous steps need to be negated
+ Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+ Node previousLiteralNodeNegated = previousLiteralNode.negate();
+ prop::SatLiteral previousLiteralNegated =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+ currentClause.push_back(previousLiteralNegated);
+ currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+ }
+
+ // If the current literal is NULL, can ignore (final step)
+ // Otherwise, the current literal does NOT need to be negated
+ Node currentLiteralNode = currentStep->getLiteral();
+ if (currentLiteralNode != Node()) {
+ prop::SatLiteral currentLiteral =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+ currentClause.push_back(currentLiteral);
+ currentClauseExpr.push_back(currentLiteralNode.toExpr());
+ }
+
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+
+ pm->getCnfProof()->printClause(currentClause, os, clause_paren);
+
+ // query appropriate theory for proof of clause
+ theory::TheoryId theory_id = currentStep->getTheory();
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+ if (!missingAssertions.empty()) {
+ Debug("pf::tp") << "Have missing assertions for this step!" << std::endl;
+ }
+
+ // Turn rewrite filter ON
+ std::set<Node>::const_iterator missingAssertion;
+ for (missingAssertion = missingAssertions.begin();
+ missingAssertion != missingAssertions.end();
+ ++missingAssertion) {
+
+ Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+
+ Assert(recipe.wasRewritten(missingAssertion->negate()));
+ Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+
+ Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+ // We have a missing assertion.
+ // rewriteIt->first is the assertion after the rewrite (the explanation),
+ // rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+ bool found = false;
+ unsigned k;
+ for (k = 0; k < currentClauseExpr.size(); ++k) {
+ if (currentClauseExpr[k] == explanation.toExpr()) {
+ found = true;
+ break;
+ }
+ }
+
+ Assert(found);
+
+ Debug("pf::tp") << "Replacing theory assertion "
+ << currentClauseExpr[k]
+ << " with "
+ << *missingAssertion
+ << std::endl;
+
+ currentClauseExpr[k] = missingAssertion->toExpr();
+
+ std::ostringstream rewritten;
+ rewritten << "(or_elim_1 _ _ ";
+ rewritten << "(not_not_intro _ ";
+ rewritten << pm->getLitName(explanation);
+ rewritten << ") (iff_elim_1 _ _ ";
+ rewritten << d_assertionToRewrite[missingAssertion->negate()];
+ rewritten << "))";
+
+ Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+ << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+ << std::endl << std::endl;
+
+ pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+ }
+
+ getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+
+ // Turn rewrite filter OFF
+ pm->clearRewriteFilters();
+
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+ os << clause_paren.str();
+ os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n";
+ paren << "))";
+ }
+
+ Assert(numberOfSteps >= 2);
+
+ os << "(satlem_simplify _ _ _ ";
+ for (unsigned i = 0; i < numberOfSteps - 1; ++i) {
+ // Resolve step i with step i + 1
+ if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) {
+ os << "(Q _ _ ";
+ } else {
+ os << "(R _ _ ";
+ }
+
+ os << pm->getLemmaClauseName(id) << "s" << i;
+ os << " ";
+ }
+
+ os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " ";
+
+ prop::SatLiteral v;
+ for (int i = numberOfSteps - 2; i >= 0; --i) {
+ v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral());
+ os << ProofManager::getVarName(v.getSatVariable(), "") << ") ";
+ }
+
+ os << "( \\ " << pm->getLemmaClauseName(id) << "\n";
+ paren << "))";
+ }
}
}
void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
- // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
LetMap::const_iterator it = map.find(term);
if (it != map.end()) {
@@ -597,19 +893,21 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let
}
void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
- //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
- Assert( d_theory!=NULL );
+ // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
+ Assert(d_theory!=NULL);
+
context::UserContext fakeContext;
ProofOutputChannel oc;
theory::Valuation v(NULL);
//make new copy of theory
theory::Theory* th;
- Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
- if(d_theory->getId()==theory::THEORY_UF) {
+ Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
+
+ if (d_theory->getId()==theory::THEORY_UF) {
th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
ProofManager::currentPM()->getLogicInfo(),
"replay::");
- } else if(d_theory->getId()==theory::THEORY_ARRAY) {
+ } else if (d_theory->getId()==theory::THEORY_ARRAY) {
th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
ProofManager::currentPM()->getLogicInfo(),
"replay::");
@@ -714,7 +1012,10 @@ void BooleanProof::registerTerm(Expr term) {
void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
Assert (term.getType().isBoolean());
if (term.isVariable()) {
- os << "(p_app " << ProofManager::sanitize(term) <<")";
+ if (d_treatBoolsAsFormulas)
+ os << "(p_app " << ProofManager::sanitize(term) <<")";
+ else
+ os << ProofManager::sanitize(term);
return;
}
@@ -753,7 +1054,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap&
return;
case kind::CONST_BOOLEAN:
- os << (term.getConst<bool>() ? "true" : "false");
+ if (d_treatBoolsAsFormulas)
+ os << (term.getConst<bool>() ? "true" : "false");
+ else
+ os << (term.getConst<bool>() ? "t_true" : "t_false");
return;
default:
@@ -786,6 +1090,10 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream&
// Nothing to do here at this point.
}
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& os,
std::ostream& paren) {
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 54c86f3f3..c8c776ec9 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -27,6 +27,7 @@
#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
#include "util/proof.h"
+#include "proof/proof_utils.h"
namespace CVC4 {
@@ -90,10 +91,14 @@ class TheoryProof;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
+typedef std::set<theory::TheoryId> TheoryIdSet;
+typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds;
+
class TheoryProofEngine {
protected:
ExprSet d_registrationCache;
TheoryProofTable d_theoryProofTable;
+ ExprToTheoryIds d_exprToTheoryIds;
/**
* Returns whether the theory is currently supported in proof
@@ -148,6 +153,14 @@ public:
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
/**
+ * Print aliasing declarations.
+ *
+ * @param os
+ * @param paren closing parenthesis
+ */
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+
+ /**
* Print proofs of all the theory lemmas (must prove
* actual clause used in resolution proof).
*
@@ -171,8 +184,14 @@ public:
*/
void registerTheory(theory::Theory* theory);
- theory::TheoryId getTheoryForLemma(ClauseId id);
+ theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
TheoryProof* getTheoryProof(theory::TheoryId id);
+
+ void markTermForFutureRegistration(Expr term, theory::TheoryId id);
+
+ void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+
+ virtual void treatBoolsAsFormulas(bool value) {};
};
class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -190,11 +209,25 @@ public:
virtual void printLetTerm(Expr term, std::ostream& os);
virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printAssertions(std::ostream& os, std::ostream& paren);
+ virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTheoryLemmas(const IdToSatClause& lemmas,
std::ostream& os,
std::ostream& paren);
virtual void printSort(Type type, std::ostream& os);
+
+ void performExtraRegistrations();
+
+ void treatBoolsAsFormulas(bool value);
+
+private:
+ static void dumpTheoryLemmas(const IdToSatClause& lemmas);
+
+ // TODO: this function should be moved into the BV prover.
+ void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
+
+ std::map<Node, std::string> d_assertionToRewrite;
};
class TheoryProof {
@@ -270,11 +303,20 @@ public:
*/
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
/**
+ * Print any aliasing declarations.
+ *
+ * @param os
+ * @param paren
+ */
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
* Register a term of this theory that appears in the proof.
*
* @param term
*/
virtual void registerTerm(Expr term) = 0;
+
+ virtual void treatBoolsAsFormulas(bool value) {}
};
class BooleanProof : public TheoryProof {
@@ -292,12 +334,13 @@ public:
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
};
class LFSCBooleanProof : public BooleanProof {
public:
LFSCBooleanProof(TheoryProofEngine* proofEngine)
- : BooleanProof(proofEngine)
+ : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
{}
virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
@@ -305,6 +348,14 @@ public:
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+
+ void treatBoolsAsFormulas(bool value) {
+ d_treatBoolsAsFormulas = value;
+ }
+
+private:
+ bool d_treatBoolsAsFormulas;
};
} /* CVC4 namespace */
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 32ca122b0..bc409901c 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -86,7 +86,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
pf->debug_print("pf::uf");
Debug("pf::uf") << std::endl;
- if(tb == 0) {
+ if (tb == 0) {
+ // Special case: false was an input, so the proof is just "false".
+ if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
+ pf->d_node == NodeManager::currentNM()->mkConst(false)) {
+ out << "(clausify_false ";
+ out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
+ out << ")" << std::endl;
+ return Node();
+ }
+
Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
Assert(!pf->d_node.isNull());
Assert(pf->d_children.size() >= 2);
@@ -190,42 +199,71 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
++i;
}
}
- Assert(neg >= 0);
+
+ bool disequalityFound = (neg >= 0);
+ if (!disequalityFound) {
+ Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+ Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::EQUAL);
+ Assert(pf->d_node.getNumChildren() == 2);
+ Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ }
Node n1;
std::stringstream ss;
- //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(pf->d_children.size() > 2) {
+
+ if(!disequalityFound || subTrans.d_children.size() >= 2) {
n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
} else {
n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
- Node n2 = pf->d_children[neg]->d_node;
- Assert(n2.getKind() == kind::NOT);
- out << "(clausify_false (contra _ ";
Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
- Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
- if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
- if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+ out << "(clausify_false (contra _ ";
+
+ if (disequalityFound) {
+ Node n2 = pf->d_children[neg]->d_node;
+ Assert(n2.getKind() == kind::NOT);
+ Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
- if(n2[0].getKind() == kind::APPLY_UF) {
- out << "(trans _ _ _ _ ";
- out << "(symm _ _ _ ";
- out << ss.str();
- out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
- } else {
- Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
- if(n1[1] == n2[0][0]) {
- out << "(symm _ _ _ " << ss.str() << ")";
+ if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
+ if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+
+ if(n2[0].getKind() == kind::APPLY_UF) {
+ out << "(trans _ _ _ _ ";
+
+ if (n1[0] == n2[0]) {
+ out << "(symm _ _ _ ";
+ out << ss.str();
+ out << ") ";
+ } else {
+ Assert(n1[1] == n2[0]);
+ out << ss.str();
+ }
+ out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
} else {
- out << ss.str();
+ Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+ if(n1[1] == n2[0][0]) {
+ out << "(symm _ _ _ " << ss.str() << ")";
+ } else {
+ out << ss.str();
+ }
+ out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
}
- out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+ } else {
+ Node n2 = pf->d_node;
+ Assert(n2.getKind() == kind::EQUAL);
+ Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+ out << ss.str();
+ out << " ";
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr());
+ out << "))" << std::endl;
}
+
return Node();
}
@@ -584,10 +622,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
} else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
// n1 is an equality/iff, but n2 is a predicate
if(n1[0] == n2) {
- n1 = n1[1];
+ n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
} else if(n1[1] == n2) {
- n1 = n1[0];
+ n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
} else {
Unreachable();
@@ -595,16 +633,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
} else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
// n2 is an equality/iff, but n1 is a predicate
if(n2[0] == n1) {
- n1 = n2[1];
+ n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
} else if(n2[1] == n1) {
- n1 = n2[0];
+ n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
} else {
Unreachable();
}
} else {
- // Both n1 and n2 are prediacates. Don't know what to do...
+ // Both n1 and n2 are predicates. Don't know what to do...
Unreachable();
}
@@ -667,6 +705,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map)
}
Assert (term.getKind() == kind::APPLY_UF);
+ d_proofEngine->treatBoolsAsFormulas(false);
if(term.getType().isBoolean()) {
os << "(p_app ";
@@ -683,6 +722,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map)
if(term.getType().isBoolean()) {
os << ")";
}
+ d_proofEngine->treatBoolsAsFormulas(true);
}
void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
@@ -714,6 +754,8 @@ void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
// declaring the terms
+ Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl;
+
for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
Expr term = *it;
@@ -729,7 +771,8 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
os << "(arrow";
for (unsigned i = 0; i < args.size(); i++) {
Type arg_type = args[i];
- os << " " << arg_type;
+ os << " ";
+ d_proofEngine->printSort(arg_type, os);
if (i < args.size() - 2) {
os << " (arrow";
fparen << ")";
@@ -742,10 +785,16 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
}
paren << ")";
}
+
+ Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl;
}
void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
// Nothing to do here at this point.
}
+void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* namespace CVC4 */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index e359eaebd..0a23267d8 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -69,6 +69,7 @@ public:
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback