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 | 495 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 14 | ||||
-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 | 620 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 55 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 103 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 1 |
22 files changed, 434 insertions, 1849 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index b9907aac9..a1287b667 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -830,8 +830,4 @@ 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 810d41155..788e4bd86 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -74,7 +74,6 @@ 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 aee236677..8aba8dce9 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -81,29 +81,14 @@ 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) { @@ -116,7 +101,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", 0, &d_proofPrinter); + pf->debug_print("pf::array"); Debug("pf::array") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; @@ -129,7 +114,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", 0, &d_proofPrinter); + pf->debug_print("pf::array"); Debug("pf::array") << std::endl; if(tb == 0) { @@ -165,7 +150,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", 0, &d_proofPrinter); + pf->d_children[i+count]->debug_print("pf::array"); congruenceClosures.push_back(pf->d_children[i+count]); } @@ -235,48 +220,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ++i; } } - - 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()); - } + Assert(neg >= 0); 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(!disequalityFound || pf->d_children.size() > 2) { + if(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; } - out << "(clausify_false (contra _ "; + 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 (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; + 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].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. - 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) { + // (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 << " "; + out << ss2.str(); + out << "))"; + + } else { + // The negative node is, e.g., a pure equality + out << "(clausify_false (contra _ "; + + if(n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; out << "(symm _ _ _ "; out << ss.str(); @@ -291,27 +276,16 @@ 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]); + 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(); } if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd", 0, &d_proofPrinter); + pf->debug_print("mgd"); 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()); @@ -341,7 +315,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd", 0, &d_proofPrinter); + pf2->debug_print("mgd"); // 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; @@ -358,7 +332,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", 0, &d_proofPrinter); + pf2->d_children[0]->debug_print("mgd"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -572,20 +546,6 @@ 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; @@ -594,7 +554,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", 0, &d_proofPrinter); + pf->debug_print("mgd"); Debug("mgd") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; @@ -812,7 +772,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, &d_proofPrinter); + pf->debug_print("mgdx",0); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -971,9 +931,6 @@ 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); @@ -982,31 +939,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; - if (swap) { - out << "(symm _ _ _ "; - } - out << "(negativerow _ _ "; - tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); + tp->printTerm(t1.toExpr(), out, map); out << " "; - tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); + tp->printTerm(t2.toExpr(), out, map); out << " "; tp->printTerm(t3.toExpr(), out, map); out << " "; tp->printTerm(t4.toExpr(), out, map); out << " "; - if (side != 0) { - out << "(negsymm _ _ _ " << ss.str() << ")"; - } else { - out << ss.str(); - } + + // 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() << ")"; + // } out << ")"; - if (swap) { - out << ") "; - } + // Unreachable(); return ret; } @@ -1117,12 +1071,13 @@ 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) { @@ -1199,21 +1154,7 @@ 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()); - 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 <<" "; - } + os << type <<" "; } void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { @@ -1228,6 +1169,8 @@ 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"; @@ -1286,7 +1229,6 @@ 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); @@ -1295,7 +1237,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p << "It is a witness for: " << equality << std::endl; std::ostringstream newSkolemLiteral; - newSkolemLiteral << ".sl" << count++; + newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); std::string skolemLiteral = newSkolemLiteral.str(); d_skolemToLiteral[*it] = skolemLiteral; @@ -1309,12 +1251,13 @@ 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 << " (\\ "; - os << ProofManager::sanitize(*it); + printTerm(*it, os, map); os << " (\\ "; os << skolemLiteral.c_str(); os << "\n"; @@ -1323,8 +1266,4 @@ 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 076ba7381..fb25c9433 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -30,32 +30,6 @@ 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, @@ -67,8 +41,6 @@ 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 @@ -81,10 +53,6 @@ public: void setRowMergeTag(unsigned tag); void setRow1MergeTag(unsigned tag); void setExtMergeTag(unsigned tag); - - unsigned getRowMergeTag() const; - unsigned getRow1MergeTag() const; - unsigned getExtMergeTag() const; }; namespace theory { @@ -123,7 +91,6 @@ 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 479266db4..b63782226 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,11 +15,9 @@ **/ -#include "options/bv_options.h" -#include "proof/array_proof.h" #include "proof/bitvector_proof.h" +#include "options/bv_options.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" @@ -82,40 +80,20 @@ 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) && @@ -123,11 +101,6 @@ 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]); @@ -135,7 +108,6 @@ 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(); @@ -150,8 +122,6 @@ 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]); @@ -159,7 +129,6 @@ 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; @@ -175,99 +144,25 @@ 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 #" << 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()) { + Debug("pf::bv") << "Finalize conflict " << confl << std::endl; + //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); + if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ ClauseId id = d_bbConflictMap[confl]; d_resolutionProof->collectClauses(id); - } else { - // There is no exact match for our conflict, but maybe it is a subset of another conflict - ExprToClauseId::const_iterator it; - bool matchFound = false; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - Expr possibleMatch = it->first; - if (possibleMatch.getKind() != kind::OR) { - // This is a single-node conflict. If this node is in the conflict we're trying to prove, - // we have a match. - for (unsigned k = 0; k < confl.getNumChildren(); ++k) { - if (confl[k] == possibleMatch) { - matchFound = true; - d_resolutionProof->collectClauses(it->second); - break; - } - } - } else { - if (possibleMatch.getNumChildren() > confl.getNumChildren()) - continue; - - unsigned k = 0; - bool matching = true; - for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { - // j is the index in possibleMatch - // k is the index in confl - while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) { - ++k; - } - if (k == confl.getNumChildren()) { - // We couldn't find a match for possibleMatch[j], so not a match - matching = false; - break; - } - } - - if (matching) { - Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl; - d_resolutionProof->collectClauses(it->second); - matchFound = true; - break; - } - } - } - - if (!matchFound) { - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl - << "Dumping existing conflicts:" << std::endl; - - i = 0; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - ++i; - Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; - } - - Unreachable(); - } + }else{ + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; } } } @@ -343,25 +238,11 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa printBitOf(term, os, map); return; } - - case kind::VARIABLE: { - os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; - return; - } - + case kind::VARIABLE: case kind::SKOLEM: { - - // 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) << ")"; - } + os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; return; } - default: Unreachable(); } @@ -377,7 +258,14 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m << ", var = " << var << std::endl; os << "(bitof "; - os << d_exprToVariableName[var]; + 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 << " " << bit << ")"; } @@ -461,16 +349,14 @@ 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) { @@ -491,7 +377,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); @@ -500,120 +386,11 @@ 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") << "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(); + Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; + BitVectorProof::printTheoryLemmaProof( lemma, os, paren ); } } @@ -625,13 +402,7 @@ 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) { - if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) { - d_exprToVariableName[*it] = ProofManager::sanitize(*it); - } else { - d_exprToVariableName[*it] = assignAlias(*it); - } - - os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; + os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n"; paren <<")"; } } @@ -640,43 +411,15 @@ 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()) { - // 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 << " _ )"; + if (Theory::isLeafOf(term, theory::THEORY_BV) && + !term.isConst()) { + os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )"; return; } @@ -705,60 +448,37 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_PLUS : case kind::BITVECTOR_SUB : case kind::BITVECTOR_CONCAT : { - Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; - - for (int i = term.getNumChildren() - 1; i > 0; --i) { + for (unsigned i =0; i < term.getNumChildren() - 1; ++i) { os <<"(bv_bbl_"<< utils::toLFSCKind(kind); - - if (i > 1) { - // This is not the inner-most operation; only child i+1 can be aliased - if (hasAlias(term[i])) {os << "_alias_2";} - } else { - // This is the inner-most operation; both children can be aliased - if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";} - if (hasAlias(term[i-1])) {os << "_1";} - if (hasAlias(term[i])) {os << "_2";} - } - if (kind == kind::BITVECTOR_CONCAT) { - os << " " << utils::getSize(term) << " _"; + os << " " << utils::getSize(term) <<" _ "; } - os << " _ _ _ _ _ _ "; + os <<" _ _ _ _ _ _ "; } - - if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} - os << getBBTermName(term[0]) << " "; + os << getBBTermName(term[0]) <<" "; for (unsigned i = 1; i < term.getNumChildren(); ++i) { - if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";} os << getBBTermName(term[i]); os << ") "; } return; } - case kind::BITVECTOR_NEG : case kind::BITVECTOR_NOT : case kind::BITVECTOR_ROTATE_LEFT : case kind::BITVECTOR_ROTATE_RIGHT : { - os << "(bv_bbl_"<<utils::toLFSCKind(kind); - os << " _ _ _ _ "; + os <<"(bv_bbl_"<<utils::toLFSCKind(kind); + os <<" _ _ _ _ "; os << getBBTermName(term[0]); - os << ")"; + os <<")"; return; } case kind::BITVECTOR_EXTRACT : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind); - - if (hasAlias(term[0])) {os << "_alias";}; - - os << " " << utils::getSize(term) << " "; + os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; + os << utils::getSize(term) << " "; os << utils::getExtractHigh(term) << " "; os << utils::getExtractLow(term) << " "; os << " _ _ _ _ "; - - if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} - os << getBBTermName(term[0]); os <<")"; return; @@ -766,7 +486,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_REPEAT : case kind::BITVECTOR_ZERO_EXTEND : case kind::BITVECTOR_SIGN_EXTEND : { - os <<"(bv_bbl_" <<utils::toLFSCKind(kind) << (hasAlias(term[0]) ? "_alias " : " "); + os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; os << utils::getSize(term) <<" "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; @@ -781,9 +501,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; os << amount; } - os <<" _ _ _ _ "; - if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} os << getBBTermName(term[0]); os <<")"; return; @@ -821,7 +539,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -832,28 +550,11 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool case kind::BITVECTOR_SLE : case kind::BITVECTOR_SGT : case kind::BITVECTOR_SGE : - case kind::EQUAL: { - Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; - - os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); - - if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";} - if (hasAlias(atom[0])) {os << "_1";} - if (hasAlias(atom[1])) {os << "_2";} - - if (swap) {os << "_swap";} - + case kind::EQUAL: + { + os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); os << " _ _ _ _ _ _ "; - - if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} - os << getBBTermName(atom[0]); - - os << " "; - - if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} - os << getBBTermName(atom[1]); - - os << ")"; + os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; return; } default: @@ -861,53 +562,19 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool } } -void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { - Assert(atom.getKind() == kind::EQUAL); - - os << "(bv_bbl_=_false"; - os << " _ _ _ _ _ _ "; - if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} - os << getBBTermName(atom[0]); - - os << " "; - - if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} - os << getBBTermName(atom[1]); - - os << ")"; -} void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { // bit-blast terms - { - Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl; - std::vector<Expr>::const_iterator it = d_bbTerms.begin(); - std::vector<Expr>::const_iterator end = d_bbTerms.end(); - - Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); - - for (; it != end; ++it) { - if (d_usedBB.find(*it) == d_usedBB.end()) { - Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; - } else { - Debug("pf::bv") << "\t" << *it << std::endl; - } - } - - Debug("pf::bv") << std::endl; - } - std::vector<Expr>::const_iterator it = d_bbTerms.begin(); std::vector<Expr>::const_iterator end = d_bbTerms.end(); for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end() && options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) continue; - - os << "(decl_bblast _ _ _ "; + os <<"(decl_bblast _ _ _ "; printTermBitblasting(*it, os); - os << "(\\ "<< getBBTermName(*it) << "\n"; - paren << "))"; + os << "(\\ "<< getBBTermName(*it); + paren <<"\n))"; } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -922,35 +589,7 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) bool val = ait->first.getConst<bool>(); os << "(iff_symm " << (val ? "true" : "false" ) << ")"; } else { - 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); - } + printAtomBitblasting(ait->first, os); } os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; @@ -967,53 +606,25 @@ 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 << std::endl << ";; BB atom mapping\n" << std::endl; - - std::set<Node> atoms; - d_cnfProof->collectAtomsForClauses(used_inputs, atoms); + os << ";; BB atom mapping\n"; - 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; + NodeSet atoms; + d_cnfProof->collectAtomsForClauses(used_inputs,atoms); // first print bit-blasting printBitblasting(os, paren); // print CNF conversion proof for bit-blasted facts d_cnfProof->printAtomMapping(atoms, os, paren); - os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; + os << ";; Bit-blasting definitional clauses \n"; for (IdToSatClause::iterator it = used_inputs.begin(); it != used_inputs.end(); ++it) { d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); } - os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; + os << ";; Bit-blasting learned clauses \n"; d_resolutionProof->printResolutions(os, paren); } -std::string LFSCBitVectorProof::assignAlias(Expr expr) { - static unsigned counter = 0; - Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); - std::stringstream ss; - ss << "fbv" << counter++; - Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl; - d_assignedAliases[expr] = ss.str(); - return ss.str(); -} - -bool LFSCBitVectorProof::hasAlias(Expr expr) { - return d_assignedAliases.find(expr) != d_assignedAliases.end(); -} - } /* namespace CVC4 */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4e5e98541..4a1f4015d 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,7 +60,6 @@ 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: @@ -109,8 +108,7 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; + virtual void printAtomBitblasting(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; @@ -125,12 +123,6 @@ 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) @@ -138,13 +130,11 @@ 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, bool swap); - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); + virtual void printAtomBitblasting(Expr term, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); - virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printBitblasting(std::ostream& os, std::ostream& paren); virtual void printResolutionProof(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index abe48e3cd..19e9cbac9 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,7 +19,6 @@ #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" @@ -33,6 +32,7 @@ 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,6 +103,7 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); + registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -142,15 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) { - Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); - return d_lemmaToProofRecipe[lemma]; +void CnfProof::registerExplanationLemma(ClauseId clauseId) { + d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); } -bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) { - return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); +theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { + Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); + return d_clauseIdToOwnerTheory[clause]; } + void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -181,10 +183,12 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { - Assert(proofRecipe); - Assert(proofRecipe->getNumSteps() > 0); - d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; +void CnfProof::setExplainerTheory(theory::TheoryId theory) { + d_explainerTheory = theory; +} + +theory::TheoryId CnfProof::getExplainerTheory() { + return d_explainerTheory; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -208,19 +212,22 @@ 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, - std::set<Node>& atoms) { + NodeSet& 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); } } @@ -230,75 +237,14 @@ 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, - std::set<Node>& atoms) { + NodeSet& atom_map) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atoms); + collectAtoms(clause, atom_map); } -} - -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, @@ -317,13 +263,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, +void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) { - std::set<Node>::const_iterator it = atoms.begin(); - std::set<Node>::const_iterator end = atoms.end(); + NodeSet::const_iterator it = atoms.begin(); + NodeSet::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(); @@ -331,8 +277,8 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name); - os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name) + << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -358,9 +304,6 @@ 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); @@ -393,10 +336,6 @@ 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; @@ -625,7 +564,6 @@ 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 ); @@ -724,7 +662,6 @@ 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 62036ced0..a21cb1c0e 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,7 +27,6 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" -#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -44,9 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; -typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe; -typedef std::pair<Node, Node> NodePair; -typedef std::set<NodePair> NodePairSet; +typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; class CnfProof { protected: @@ -58,8 +55,11 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; - /** Map from lemma to the recipe for proving it **/ - LemmaToRecipe d_lemmaToProofRecipe; + /** Map from assertion to the theory that added this assertion **/ + ClauseIdToTheory d_clauseIdToOwnerTheory; + + /** The last theory to explain a lemma **/ + theory::TheoryId d_explainerTheory; /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; @@ -91,16 +91,10 @@ 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, - std::set<Node>& atoms); + NodeSet& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - std::set<Node>& atoms); - void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, - std::set<Node>& atoms, - NodePairSet& rewrites); + NodeSet& atoms); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -127,9 +121,11 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setProofRecipe(LemmaProofRecipe* proofRecipe); - LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); - bool haveProofRecipe(const std::set<Node> &lemma); + void setExplainerTheory(theory::TheoryId theory); + theory::TheoryId getExplainerTheory(); + theory::TheoryId getOwnerTheory(ClauseId clause); + + void registerExplanationLemma(ClauseId clauseId); // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); @@ -138,7 +134,7 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const std::set<Node>& atoms, + virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) = 0; @@ -165,7 +161,7 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const std::set<Node>& atoms, + void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp deleted file mode 100644 index a12a516cf..000000000 --- a/src/proof/lemma_proof.cpp +++ /dev/null @@ -1,193 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index e96ff5337..000000000 --- a/src/proof/lemma_proof.h +++ /dev/null @@ -1,79 +0,0 @@ -/********************* */ -/*! \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 5ce8b523f..a3689d746 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -200,6 +200,7 @@ 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; @@ -216,15 +217,9 @@ std::string ProofManager::getAtomName(TNode atom, Assert(!lit.isNegated()); return getAtomName(lit.getSatVariable(), prefix); } - std::string ProofManager::getLitName(TNode lit, const std::string& 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; + return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); } std::string ProofManager::sanitize(TNode node) { @@ -336,9 +331,6 @@ 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 @@ -392,37 +384,8 @@ void LFSCProof::toStream(std::ostream& out) { for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; - std::set<Node> atoms; - NodePairSet rewrites; + NodeSet atoms; // 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); @@ -430,23 +393,38 @@ 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); } - std::set<Node>::iterator atomIt; - Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " - << std::endl << std::endl; + NodeSet::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 = atoms.begin(); it != atoms.end(); ++it) { + for(; it != end; ++it) { Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } @@ -466,15 +444,9 @@ 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\n"; + out << " ;; Printing deferred declarations \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); @@ -492,6 +464,10 @@ 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; @@ -520,8 +496,6 @@ 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 _ "; @@ -532,6 +506,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; + } os << "\n"; @@ -593,14 +568,6 @@ 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 c6454b652..c74aac237 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -34,8 +34,6 @@ namespace CVC4 { -class SmtGlobals; - // forward declarations namespace Minisat { class Solver; @@ -138,8 +136,6 @@ class ProofManager { std::set<Type> d_printedTypes; - std::map<std::string, std::string> d_rewriteFilters; - protected: LogicInfo d_logic; @@ -228,9 +224,6 @@ 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 deleted file mode 100644 index 6d729db1f..000000000 --- a/src/proof/proof_output_channel.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index b85af5fb5..000000000 --- a/src/proof/proof_output_channel.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \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 fe0d42242..5b04c281d 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, std::set<Node>& seen) { +void collectAtoms(TNode node, CVC4::NodeSet& 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 8c734c892..da10c33a0 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,9 +29,6 @@ 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); @@ -45,7 +42,7 @@ inline unsigned getExtractLow(Expr node) { } inline unsigned getSize(Type type) { - BitVectorType bv(type); + BitVectorType bv(type); return bv.getSize(); } @@ -63,8 +60,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) { @@ -76,16 +73,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) { @@ -95,14 +92,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(); @@ -112,23 +109,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(); @@ -138,7 +135,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) { ++ it; } - Node res = conjunction; + Node res = conjunction; return res.toExpr(); }/* mkAnd() */ @@ -147,14 +144,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(); @@ -168,13 +165,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, std::set<Node>& seen); +void collectAtoms(TNode node, NodeSet& seen); } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 1e01e4dce..4f3330ef7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -543,9 +543,12 @@ 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) - << std::endl; + Debug("pf::sat") + << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; + d_cnfProof->registerExplanationLemma(newId); } } @@ -576,10 +579,12 @@ 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 - << std::endl; + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "lemma (UNIT CLAUSE): " + << lit << ". Explainer theory: " + << d_cnfProof->getExplainerTheory() << std::endl; d_lemmaClauses.insert(newId); + d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; @@ -837,7 +842,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 (size_t i = 0; i < current_reason_size; i++) { + for (int 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]; @@ -899,7 +904,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 (size_t i = 0; i < conflict_size; ++i) { + for (int 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); @@ -1101,12 +1106,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 b026e21c2..de510e514 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -37,6 +37,7 @@ 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 eaf21846b..088275b3f 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -25,7 +25,6 @@ #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" @@ -49,6 +48,74 @@ 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() @@ -64,12 +131,13 @@ 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("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; + Trace("theory-proof-debug") << "; register theory " << id << std::endl; if (id == theory::THEORY_UF) { d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); @@ -99,42 +167,19 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { - // The UF theory handles queries for the Builtin theory. - if (id == theory::THEORY_BUILTIN) { - Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl; - id = theory::THEORY_UF; - } - Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end()); return d_theoryProofTable[id]; } -void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) { - d_exprToTheoryIds[term].insert(id); -} - -void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { - LetMap emptyMap; - - os << "(trust_f (not (= _ "; - printBoundTerm(c1, os, emptyMap); - os << " "; - printBoundTerm(c2, os, emptyMap); - os << ")))"; -} - void TheoryProofEngine::registerTerm(Expr term) { - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; - if (d_registrationCache.count(term)) { return; } - - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl; + Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -148,38 +193,32 @@ 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(const prop::SatClause* clause) { +theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { ProofManager* pm = ProofManager::currentPM(); - 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; - } + Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" + << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; - nodes.insert(lit.isNegated() ? node.notNode() : node); + 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; } - // Ensure that the lemma is in the database. - Assert (pm->getCnfProof()->haveProofRecipe(nodes)); - return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); + 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(); } void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { @@ -233,6 +272,8 @@ 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 @@ -274,29 +315,6 @@ 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(); @@ -304,8 +322,6 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } - - performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -317,43 +333,17 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - std::ostringstream name; - name << "A" << counter++; - os << "(% " << name.str() << " (th_holds "; + // FIXME: merge this with counter + os << "(% A" << counter++ << " (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; @@ -388,148 +378,55 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost } } -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) { - it->second->printAliasingDeclarations(os, paren); - } -} +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(); -void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { - Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; - ProofManager* pm = ProofManager::currentPM(); - for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + for (; it != end; ++it) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; ClauseId id = it->first; - Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl; - const prop::SatClause* clause = it->second; - std::set<Node> nodes; - for(unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = (*clause)[i]; - Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); - if (node.isConst()) { - Assert (node.toExpr() == utils::mkTrue()); - continue; - } - nodes.insert(lit.isNegated() ? node.notNode() : node); - } - - LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); - recipe.dump("pf::dumpLemmas"); + Debug("pf::tp") << "\tLemma = " << id + << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; } + it = lemmas.begin(); - 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 + // 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) { + for (; it != end; ++it) { + ClauseId id = it->first; const prop::SatClause* clause = it->second; + theory::TheoryId theory_id = getTheoryForLemma(id); + if (theory_id != theory::THEORY_BV) continue; + std::vector<Expr> conflict; - std::set<Node> conflictNodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable()); - Expr atom = node.toExpr(); - - // The literals (true) and (not false) are omitted from conflicts + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); 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); + bv->printResolutionProof(os, paren); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -537,247 +434,54 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, return; } - ProofManager* pm = ProofManager::currentPM(); + it = lemmas.begin(); + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; - for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + 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; 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") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = " - << id << std::endl; + Debug("pf::tp") << "CnfProof printing clause..." << std::endl; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + Debug("pf::tp") << "CnfProof printing clause - Done!" << 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]; - Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); - Expr atom = node.toExpr(); + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).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); } - 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 << "))"; - } + 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 << "))"; } } 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()) { @@ -893,21 +597,19 @@ 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("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; - - if (d_theory->getId()==theory::THEORY_UF) { + Trace("theory-proof-debug") << ";; 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::"); @@ -1012,10 +714,7 @@ void BooleanProof::registerTerm(Expr term) { void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - if (d_treatBoolsAsFormulas) - os << "(p_app " << ProofManager::sanitize(term) <<")"; - else - os << ProofManager::sanitize(term); + os << "(p_app " << ProofManager::sanitize(term) <<")"; return; } @@ -1054,10 +753,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& return; case kind::CONST_BOOLEAN: - if (d_treatBoolsAsFormulas) - os << (term.getConst<bool>() ? "true" : "false"); - else - os << (term.getConst<bool>() ? "t_true" : "t_false"); + os << (term.getConst<bool>() ? "true" : "false"); return; default: @@ -1090,10 +786,6 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream& // Nothing to do here at this point. } -void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { - // Nothing to do here at this point. -} - void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index c8c776ec9..54c86f3f3 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -27,7 +27,6 @@ #include "proof/clause_id.h" #include "prop/sat_solver_types.h" #include "util/proof.h" -#include "proof/proof_utils.h" namespace CVC4 { @@ -91,14 +90,10 @@ 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 @@ -153,14 +148,6 @@ 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). * @@ -184,14 +171,8 @@ public: */ void registerTheory(theory::Theory* theory); - theory::TheoryId getTheoryForLemma(const prop::SatClause* clause); + theory::TheoryId getTheoryForLemma(ClauseId id); 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 { @@ -209,25 +190,11 @@ 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 { @@ -303,20 +270,11 @@ public: */ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; /** - * Print any aliasing declarations. - * - * @param os - * @param paren - */ - virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; - /** * Register a term of this theory that appears in the proof. * * @param term */ virtual void registerTerm(Expr term) = 0; - - virtual void treatBoolsAsFormulas(bool value) {} }; class BooleanProof : public TheoryProof { @@ -334,13 +292,12 @@ 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), d_treatBoolsAsFormulas(true) + : BooleanProof(proofEngine) {} virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); @@ -348,14 +305,6 @@ 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 bc409901c..32ca122b0 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -86,16 +86,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E pf->debug_print("pf::uf"); Debug("pf::uf") << std::endl; - 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(); - } - + if(tb == 0) { Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); Assert(pf->d_children.size() >= 2); @@ -199,71 +190,42 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ++i; } } - - 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()); - } + Assert(neg >= 0); 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(!disequalityFound || subTrans.d_children.size() >= 2) { + if(pf->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; } - Debug("pf::uf") << "\nhave proven: " << 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 (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].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 (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 (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; + 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() << ")"; } 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() << ")"; - } else { - out << ss.str(); - } - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << ss.str(); } - } 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; + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } - return Node(); } @@ -622,10 +584,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].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[1]; ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[0]; ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); @@ -633,16 +595,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].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[1]; ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[0]; ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); } } else { - // Both n1 and n2 are predicates. Don't know what to do... + // Both n1 and n2 are prediacates. Don't know what to do... Unreachable(); } @@ -705,7 +667,6 @@ 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 "; @@ -722,7 +683,6 @@ 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) { @@ -754,8 +714,6 @@ 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; @@ -771,8 +729,7 @@ 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 << " "; - d_proofEngine->printSort(arg_type, os); + os << " " << arg_type; if (i < args.size() - 2) { os << " (arrow"; fparen << ")"; @@ -785,16 +742,10 @@ 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 0a23267d8..e359eaebd 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -69,7 +69,6 @@ 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); }; |