diff options
Diffstat (limited to 'src/proof/array_proof.cpp')
-rw-r--r-- | src/proof/array_proof.cpp | 173 |
1 files changed, 117 insertions, 56 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 8aba8dce9..aee236677 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -81,14 +81,29 @@ inline static bool match(TNode n1, TNode n2) { void ProofArray::setRowMergeTag(unsigned tag) { d_reasonRow = tag; + d_proofPrinter.d_row = tag; } void ProofArray::setRow1MergeTag(unsigned tag) { d_reasonRow1 = tag; + d_proofPrinter.d_row1 = tag; } void ProofArray::setExtMergeTag(unsigned tag) { d_reasonExt = tag; + d_proofPrinter.d_ext = tag; +} + +unsigned ProofArray::getRowMergeTag() const { + return d_reasonRow; +} + +unsigned ProofArray::getRow1MergeTag() const { + return d_reasonRow1; +} + +unsigned ProofArray::getExtMergeTag() const { + return d_reasonExt; } void ProofArray::toStream(std::ostream& out) { @@ -101,7 +116,7 @@ void ProofArray::toStream(std::ostream& out) { void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) { Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; @@ -114,7 +129,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, const LetMap& map) { Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; if(tb == 0) { @@ -150,7 +165,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf->d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::array"); + pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter); congruenceClosures.push_back(pf->d_children[i+count]); } @@ -220,48 +235,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ++i; } } - Assert(neg >= 0); + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) { + Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + Assert(pf->d_node.getNumChildren() == 2); + Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + } Node n1; std::stringstream ss, ss2; //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + if(!disequalityFound || pf->d_children.size() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - Debug("mgdx") << "\nhave proven: " << n1 << std::endl; - Debug("mgdx") << "n2 is " << n2 << std::endl; - Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; - Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; - - if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - - if (pf->d_children[neg]->d_id == d_reasonExt) { - // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. - - // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6 - - out << "(clausify_false (contra _ "; - out << ss.str(); - - toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + out << "(clausify_false (contra _ "; - out << " "; - out << ss2.str(); - out << "))"; + if (disequalityFound) { + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("mgdx") << "\nhave proven: " << n1 << std::endl; + Debug("mgdx") << "n2 is " << n2 << std::endl; + Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; + Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; - } else { - // The negative node is, e.g., a pure equality - out << "(clausify_false (contra _ "; + if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - if(n2[0].getKind() == kind::APPLY_UF) { + if ((pf->d_children[neg]->d_id == d_reasonExt) || + (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) { + // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. + out << ss.str(); + out << " "; + toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + out << ss2.str(); + } else if (n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; out << "(symm _ _ _ "; out << ss.str(); @@ -276,16 +291,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " << ProofManager::getLitName(n2[0]) << std::endl; - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << " " << ProofManager::getLitName(n2[0]); } + } else { + Node n2 = pf->d_node; + Assert(n2.getKind() == kind::EQUAL); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + + out << ss.str(); + out << " "; + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n1[0].toExpr(), + n1[1].toExpr()); } + out << "))" << std::endl; return Node(); } if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); std::stack<const theory::eq::EqProof*> stk; for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { Assert(!pf2->d_node.isNull()); @@ -315,7 +341,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd"); + pf2->debug_print("mgd", 0, &d_proofPrinter); // Temp Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl; Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl; @@ -332,7 +358,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "SIDE IS 1\n"; if(!match(pf2->d_node, n1[1])) { Debug("mgd") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("mgd"); + pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -546,6 +572,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf->d_node; } + else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::NOT); + Node n = pf->d_node[0]; + Assert(n.getKind() == kind::EQUAL); + Assert(n.getNumChildren() == 2); + Assert(n[0].isConst() && n[1].isConst()); + + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n[0].toExpr(), + n[1].toExpr()); + return pf->d_node; + } + else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; @@ -554,7 +594,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf->d_children.size() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); Debug("mgd") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; @@ -772,7 +812,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("mgdx",0); + pf->debug_print("mgdx", 0, &d_proofPrinter); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -931,6 +971,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, t4 = pf->d_children[0]->d_node[0][side][0][2]; ret = pf->d_node; + // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry. + bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; Assert(pf->d_children.size() == 1); @@ -939,28 +982,31 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + if (swap) { + out << "(symm _ _ _ "; + } + out << "(negativerow _ _ "; - tp->printTerm(t1.toExpr(), out, map); + tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); out << " "; - tp->printTerm(t2.toExpr(), out, map); + tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); out << " "; tp->printTerm(t3.toExpr(), out, map); out << " "; tp->printTerm(t4.toExpr(), out, map); out << " "; - - // if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); - // } else { - // Debug("pf::array") << "Need symmetry!" << std::endl; - // out << "(negsymm _ _ _ " << ss.str() << ")"; - // } + if (side != 0) { + out << "(negsymm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } out << ")"; - // Unreachable(); + if (swap) { + out << ") "; + } return ret; } @@ -1071,13 +1117,12 @@ void ArrayProof::registerTerm(Expr term) { } std::string ArrayProof::skolemToLiteral(Expr skolem) { + Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl; Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end()); return d_skolemToLiteral[skolem]; } void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { - Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl; - Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY); if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) { @@ -1154,7 +1199,21 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& m void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; Assert (type.isArray() || type.isSort()); - os << type <<" "; + if (type.isArray()){ + ArrayType array_type(type); + + Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: " + << array_type.getIndexType() + << ", element type: " << array_type.getConstituentType() << std::endl; + + os << "(Array "; + printSort(array_type.getIndexType(), os); + os << " "; + printSort(array_type.getConstituentType(), os); + os << ")"; + } else { + os << type <<" "; + } } void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { @@ -1169,8 +1228,6 @@ void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostrea void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { // declaring the sorts - Debug("pf::array") << "Arrays declaring sorts..." << std::endl; - for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { if (!ProofManager::currentPM()->wasPrinted(*it)) { os << "(% " << *it << " sort\n"; @@ -1229,6 +1286,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::array") << "Array: print deferred declarations called" << std::endl; + unsigned count = 1; for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) { Expr term = *it; Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it); @@ -1237,7 +1295,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p << "It is a witness for: " << equality << std::endl; std::ostringstream newSkolemLiteral; - newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); + newSkolemLiteral << ".sl" << count++; std::string skolemLiteral = newSkolemLiteral.str(); d_skolemToLiteral[*it] = skolemLiteral; @@ -1251,13 +1309,12 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p Node array_two = equality[0][1]; LetMap map; - os << "(ext _ _ "; printTerm(array_one.toExpr(), os, map); os << " "; printTerm(array_two.toExpr(), os, map); os << " (\\ "; - printTerm(*it, os, map); + os << ProofManager::sanitize(*it); os << " (\\ "; os << skolemLiteral.c_str(); os << "\n"; @@ -1266,4 +1323,8 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p } } +void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* CVC4 namespace */ |