diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 4 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 1 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 173 | ||||
-rw-r--r-- | src/proof/array_proof.h | 33 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 513 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 15 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 115 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 34 | ||||
-rw-r--r-- | src/proof/lemma_proof.cpp | 193 | ||||
-rw-r--r-- | src/proof/lemma_proof.h | 79 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 91 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 7 | ||||
-rw-r--r-- | src/proof/proof_output_channel.cpp | 82 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 50 | ||||
-rw-r--r-- | src/proof/proof_utils.cpp | 52 | ||||
-rw-r--r-- | src/proof/proof_utils.h | 53 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 27 | ||||
-rw-r--r-- | src/proof/skolemization_manager.h | 1 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 630 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 61 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 103 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 1 |
22 files changed, 1882 insertions, 436 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..b2d6fdecf 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,14 @@ 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 { + std::string newAlias = assignAlias(*it); + d_exprToVariableName[*it] = newAlias; + } + + os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; paren <<")"; } } @@ -411,15 +641,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,14 +706,18 @@ 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 (kind == kind::BITVECTOR_CONCAT) { - os << " " << utils::getSize(term) <<" _ "; + os << " " << utils::getSize(term) << " _"; } - os <<" _ _ _ _ _ _ "; + os << " _ _ _ _ _ _ "; } - os << getBBTermName(term[0]) <<" "; + + os << getBBTermName(term[0]) << " "; for (unsigned i = 1; i < term.getNumChildren(); ++i) { os << getBBTermName(term[i]); @@ -463,22 +725,25 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& 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); + + os << " " << utils::getSize(term) << " "; os << utils::getExtractHigh(term) << " "; os << utils::getExtractLow(term) << " "; os << " _ _ _ _ "; + os << getBBTermName(term[0]); os <<")"; return; @@ -486,8 +751,8 @@ 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 << utils::getSize(term) <<" "; + os << "(bv_bbl_" << utils::toLFSCKind(kind) << " "; + os << utils::getSize(term) << " "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; os << amount; @@ -501,6 +766,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; os << amount; } + os <<" _ _ _ _ "; os << getBBTermName(term[0]); os <<")"; @@ -539,7 +805,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 +816,19 @@ 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 (swap) {os << "_swap";} + os << " _ _ _ _ _ _ "; - os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; + os << getBBTermName(atom[0]); + os << " "; + os << getBBTermName(atom[1]); + os << ")"; + return; } default: @@ -562,19 +836,62 @@ 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 << " _ _ _ _ _ _ "; + os << getBBTermName(atom[0]); + + os << " "; + + 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 _ _ _ "; - printTermBitblasting(*it, os); - os << "(\\ "<< getBBTermName(*it); - paren <<"\n))"; + + // Is this term has an alias, we inject it through the decl_bblast statement + if (hasAlias(*it)) { + os << "(decl_bblast_with_alias _ _ _ _ "; + printTermBitblasting(*it, os); + os << " " << d_aliasToBindDeclaration[d_assignedAliases[*it]] << " "; + os << "(\\ "<< getBBTermName(*it); + os << "\n"; + paren <<"))"; + } else { + os << "(decl_bblast _ _ _ "; + printTermBitblasting(*it, os); + os << "(\\ "<< getBBTermName(*it); + os << "\n"; + paren <<"))"; + } } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -589,7 +906,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 +951,83 @@ 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; - NodeSet atoms; - d_cnfProof->collectAtomsForClauses(used_inputs,atoms); + std::set<Node> 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) { + Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); + + std::stringstream ss; + ss << "fbv" << d_assignedAliases.size(); + 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(); +} + +void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + Assert (c1.isConst()); + Assert (c2.isConst()); + Assert (utils::getSize(c1) == utils::getSize(c2)); + + os << "(bv_disequal_constants " << utils::getSize(c1) << " "; + + std::ostringstream paren; + + for (int i = utils::getSize(c1) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c1, i) ? "b1" : "b0") << " "; + paren << ")"; + } + os << "bvn"; + os << paren.str(); + + os << " "; + + for (int i = utils::getSize(c2) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c2, i) ? "b1" : "b0") << " "; + + } + os << "bvn"; + os << paren.str(); + + os << ")"; +} + } /* namespace CVC4 */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4a1f4015d..5ea754e08 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,13 +138,16 @@ 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); + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); }; }/* CVC4 namespace */ 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..fe67ec94d 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,40 @@ 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) { + Assert(c1.isConst()); + Assert(c2.isConst()); + + Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2)); + getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2); +} + 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 +146,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 +231,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 +272,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 +302,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } + + performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -333,17 +315,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 +386,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); + } - theory::TheoryId theory_id = getTheoryForLemma(id); - if (theory_id != theory::THEORY_BV) continue; + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); + recipe.dump("pf::dumpLemmas"); + } + + 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 +535,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 +891,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 +1010,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 +1052,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,10 +1088,26 @@ 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) { Unreachable("No boolean lemmas yet!"); } +void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + // By default, we just print a trust statement. Specific theories can implement + // better proofs. + LetMap emptyMap; + + os << "(trust_f (not (= _ "; + d_proofEngine->printBoundTerm(c1, os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(c2, os, emptyMap); + os << ")))"; +} + } /* namespace CVC4 */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 54c86f3f3..352cc1b53 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,26 @@ 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; + /** + * Print a proof for the disequality of two constants that belong to this theory. + * + * @param term + */ + virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + + virtual void treatBoolsAsFormulas(bool value) {} }; class BooleanProof : public TheoryProof { @@ -292,12 +340,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 +354,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); }; |