diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/array_proof.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/array_proof.cpp')
-rw-r--r-- | src/proof/array_proof.cpp | 173 |
1 files changed, 56 insertions, 117 deletions
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 */ |