diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/array_proof.cpp | 119 | ||||
-rw-r--r-- | src/proof/array_proof.h | 11 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 82 |
3 files changed, 78 insertions, 134 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 764028c6b..aa615f90e 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -23,6 +23,10 @@ namespace CVC4 { +unsigned ProofArray::d_reasonRow; +unsigned ProofArray::d_reasonRow1; +unsigned ProofArray::d_reasonExt; + inline static Node eqNode(TNode n1, TNode n2) { return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); } @@ -79,6 +83,18 @@ inline static bool match(TNode n1, TNode n2) { return true; } +void ProofArray::setRowMergeTag(unsigned tag) { + d_reasonRow = tag; +} + +void ProofArray::setRow1MergeTag(unsigned tag) { + d_reasonRow1 = tag; +} + +void ProofArray::setExtMergeTag(unsigned tag) { + d_reasonExt = tag; +} + void ProofArray::toStream(std::ostream& out) { Trace("pf::array") << "; Print Array proof..." << std::endl; //AJR : carry this further? @@ -95,16 +111,16 @@ void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::Eq Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; } -void ProofArray::registerSkolem(Node equality, Node skolem) { - d_nodeToSkolem[equality] = skolem; -} - Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, unsigned tb, const LetMap& map) { + Debug("gk::temp") << "d_reasonExt = " << d_reasonExt << std::endl; + Debug("gk::temp") << "d_reasonRow = " << d_reasonRow << std::endl; + Debug("gk::temp") << "d_reasonRow1 = " << d_reasonRow1 << std::endl; + Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; pf->debug_print("pf::array"); Debug("pf::array") << std::endl; @@ -138,8 +154,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Collecting congruence sequence" << std::endl; for (count = 0; i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && - pf->d_children[i + count]->d_node.isNull(); + pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + 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"); @@ -235,7 +251,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, 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 == theory::eq::MERGED_ARRAYS_EXT) { + 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 @@ -275,8 +291,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return Node(); } - switch(pf->d_id) { - case theory::eq::MERGED_THROUGH_CONGRUENCE: { + if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; pf->debug_print("mgd"); std::stack<const theory::eq::EqProof*> stk; @@ -324,8 +339,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { 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"); + Debug("mgd") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("mgd"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -370,7 +385,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2 << kind::PARTIAL_APPLY_UF; b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); } - b2.append(n1[1-side].begin(), n1[1-side].end()); + b2.append(n1[1-side].begin(), n1[1-side].end()); } else if (n1[1-side].getKind() == kind::PARTIAL_SELECT_0) { b2 << kind::PARTIAL_SELECT_1; } else { @@ -464,13 +479,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b1.append(n1.begin(), n1.end()); n1 = b1; Debug("mgd") << "New n1: " << n1 << std::endl; - // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) { - // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; - // b1.clear(kind::PARTIAL_SELECT_1); - // b1.append(n1.begin(), n1.end()); - // n1 = b1; - // Debug("mgd") << "New n1: " << n1 << std::endl; - // } else + // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b1.clear(kind::PARTIAL_SELECT_1); + // b1.append(n1.begin(), n1.end()); + // n1 = b1; + // Debug("mgd") << "New n1: " << n1 << std::endl; + // } else } else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n1.getOperator())) { b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); @@ -498,13 +513,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2.append(n2.begin(), n2.end()); n2 = b2; Debug("mgd") << "New n2: " << n2 << std::endl; - // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) { - // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; - // b2.clear(kind::PARTIAL_SELECT_1); - // b2.append(n2.begin(), n2.end()); - // n2 = b2; - // Debug("mgd") << "New n2: " << n2 << std::endl; - // } else + // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b2.clear(kind::PARTIAL_SELECT_1); + // b2.append(n2.begin(), n2.end()); + // n2 = b2; + // Debug("mgd") << "New n2: " << n2 << std::endl; + // } else } else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n2.getOperator())) { b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); @@ -521,23 +536,25 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n; } - case theory::eq::MERGED_THROUGH_REFLEXIVITY: + else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); out << "(refl _ "; tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); out << ")"; return eqNode(pf->d_node, pf->d_node); + } - case theory::eq::MERGED_THROUGH_EQUALITY: + else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) { Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " << ProofManager::getLitName(pf->d_node.negate()) << std::endl; out << ProofManager::getLitName(pf->d_node.negate()); return pf->d_node; + } - case theory::eq::MERGED_THROUGH_TRANS: { + else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; @@ -734,27 +751,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { - if(tb == 1) { Debug("mgdx") << "case 1\n"; } - n1 = eqNode(n1[1], n2[1]); - ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str(); + if(tb == 1) { Debug("mgdx") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str(); } else if(n1[1] == n2[1]) { if(tb == 1) { Debug("mgdx") << "case 2\n"; } n1 = eqNode(n1[0], n2[0]); ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")"; } else if(n1[0] == n2[1]) { - if(tb == 1) { Debug("mgdx") << "case 3\n"; } - if(!firstNeg && !secondNeg) { - n1 = eqNode(n2[0], n1[1]); - ss << ss2.str() << " " << ss1.str(); - } else if (firstNeg) { - n1 = eqNode(n1[1], n2[0]); - ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; - } else { - Assert(secondNeg); - n1 = eqNode(n1[1], n2[0]); - ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")"; - } - if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } + if(tb == 1) { Debug("mgdx") << "case 3\n"; } + if(!firstNeg && !secondNeg) { + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + } else if (firstNeg) { + n1 = eqNode(n1[1], n2[0]); + ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; + } else { + Assert(secondNeg); + n1 = eqNode(n1[1], n2[0]); + ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")"; + } + if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } } else if(n1[1] == n2[0]) { if(tb == 1) { Debug("mgdx") << "case 4\n"; } n1 = eqNode(n1[0], n2[1]); @@ -811,7 +828,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n1; } - case theory::eq::MERGED_ARRAYS_ROW: { + else if (pf->d_id == d_reasonRow) { Debug("mgd") << "row lemma: " << pf->d_node << std::endl; Assert(pf->d_node.getKind() == kind::EQUAL); @@ -942,8 +959,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); + Debug("pf::array") << "Dont need symmetry!" << std::endl; + out << ss.str(); // } else { // Debug("pf::array") << "Need symmetry!" << std::endl; // out << "(negsymm _ _ _ " << ss.str() << ")"; @@ -957,7 +974,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } } - case theory::eq::MERGED_ARRAYS_ROW1: { + else if (pf->d_id == d_reasonRow1) { Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl; Assert(pf->d_node.getKind() == kind::EQUAL); TNode t1, t2, t3; @@ -992,7 +1009,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return ret; } - case theory::eq::MERGED_ARRAYS_EXT: { + else if (pf->d_id == d_reasonExt) { theory::eq::EqProof *child_proof; Assert(pf->d_node.getKind() == kind::NOT); @@ -1021,7 +1038,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf->d_node; } - default: + else { Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 9b308dcd8..b3fe89f0b 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -35,7 +35,12 @@ private: unsigned tb, const LetMap& map); - std::hash_map<Node, Node, NodeHashFunction> d_nodeToSkolem; + /** Merge tag for ROW applications */ + static unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + static unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + static unsigned d_reasonExt; public: ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} //it is simply an equality engine proof @@ -44,6 +49,10 @@ public: static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); void registerSkolem(Node equality, Node skolem); + + static void setRowMergeTag(unsigned tag); + static void setRow1MergeTag(unsigned tag); + static void setExtMergeTag(unsigned tag); }; namespace theory { diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 6a6f8d906..e728e9e49 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -615,88 +615,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E return n1; } - case theory::eq::MERGED_ARRAYS_ROW: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - TNode t1, t2, t3, t4; - Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0] == pf->d_node[1][0][0] && - pf->d_node[0][1] == pf->d_node[1][1]) { - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[1][1]; - t1 = pf->d_node[0][0]; - t4 = pf->d_node[1][0][2]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0] == pf->d_node[0][0][0] && - pf->d_node[1][1] == pf->d_node[0][1]); - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[0][1]; - t1 = pf->d_node[1][0]; - t4 = pf->d_node[0][0][2]; - ret = pf->d_node; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } - out << "(row _ _ "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << " "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t4.toExpr(), out, map); - out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")"; - return ret; - } - - case theory::eq::MERGED_ARRAYS_ROW1: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "row1 lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - TNode t1, t2, t3; - Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[1][0][1] == pf->d_node[1][1] && - pf->d_node[1][0][2] == pf->d_node[0]) { - t1 = pf->d_node[1][0][0]; - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[0]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; - } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[0][0][1] == pf->d_node[0][1] && - pf->d_node[0][0][2] == pf->d_node[1]); - t1 = pf->d_node[0][0][0]; - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[1]; - ret = pf->d_node; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; - } - out << "(row1 _ _ "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << ")"; - return ret; - } - default: Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); |