From 1ae10032fb99ca1d8f73c5f51dce3cfc976b3dfb Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 25 Apr 2018 15:12:51 -0700 Subject: [PATCH] Refactor array-proofs and uf-proofs (#1655) This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp. --- src/proof/arith_proof.cpp | 1 + src/proof/arith_proof.h | 3 +- src/proof/array_proof.cpp | 1045 +++++++++++++++------------------ src/proof/array_proof.h | 3 +- src/proof/bitvector_proof.cpp | 1 + src/proof/bitvector_proof.h | 2 +- src/proof/theory_proof.cpp | 373 +++++++++++- src/proof/theory_proof.h | 60 +- src/proof/uf_proof.cpp | 364 ++++-------- src/proof/uf_proof.h | 3 +- 10 files changed, 1005 insertions(+), 850 deletions(-) diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 89221dc69..3da7efd2e 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -643,6 +643,7 @@ ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe) : TheoryProof(arith, pe), d_realMode(false) {} +theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; } void ArithProof::registerTerm(Expr term) { Debug("pf::arith") << "Arith register term: " << term << ". Kind: " << term.getKind() << ". Type: " << term.getType() << std::endl; diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 677952bf7..2052adeac 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -63,8 +63,9 @@ protected: ExprSet d_declarations; // all the variable/function declarations bool d_realMode; + theory::TheoryId getTheoryId(); -public: + public: ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index b0290fb3e..96197bb00 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -59,61 +59,7 @@ std::string ArrayProofPrinter::printTag(unsigned tag) { } // namespace -inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); -} - -// congrence matching term helper -inline static bool match(TNode n1, TNode n2) { - Debug("mgd") << "match " << n1 << " " << n2 << std::endl; - if(ProofManager::currentPM()->hasOp(n1)) { - n1 = ProofManager::currentPM()->lookupOp(n1); - } - if(ProofManager::currentPM()->hasOp(n2)) { - n2 = ProofManager::currentPM()->lookupOp(n2); - } - Debug("mgd") << "+ match " << n1 << " " << n2 << std::endl; - Debug("pf::array") << "+ match: step 1" << std::endl; - if(n1 == n2) { - return true; - } - - if(n1.getType().isFunction() && n2.hasOperator()) { - if(ProofManager::currentPM()->hasOp(n2.getOperator())) { - return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator()); - } else { - return n1 == n2.getOperator(); - } - } - - if(n2.getType().isFunction() && n1.hasOperator()) { - if(ProofManager::currentPM()->hasOp(n1.getOperator())) { - return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator()); - } else { - return n2 == n1.getOperator(); - } - } - - if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) { - if (!((n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_0) || - (n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_1) || - (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::SELECT) || - (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::PARTIAL_SELECT_0) || - (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::SELECT) || - (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::PARTIAL_SELECT_1) - )) { - return false; - } - } - - for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) { - if(n1[i] != n2[i]) { - return false; - } - } - return true; -} ProofArray::ProofArray(std::shared_ptr pf, unsigned row, @@ -160,131 +106,19 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); - pf.debug_print("pf::array", 0, &proofPrinter); - Debug("pf::array") << std::endl; - if(tb == 0) { - Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); - Assert(!pf.d_node.isNull()); - Assert(pf.d_children.size() >= 2); - - int neg = -1; std::shared_ptr subTrans = std::make_shared(); - subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; - subTrans->d_node = pf.d_node; - size_t i = 0; - while (i < pf.d_children.size()) { - if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) - pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node); - - // Look for the negative clause, with which we will form a contradiction. - if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) { - Assert(neg < 0); - neg = i; - ++i; - } - - // Handle congruence closures over equalities. - else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) { - Debug("pf::array") << "Handling congruence over equalities" << std::endl; - - // Gather the sequence of consecutive congruence closures. - std::vector> congruenceClosures; - unsigned count; - 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(); - ++count) { - Debug("pf::array") << "Found a congruence: " << std::endl; - pf.d_children[i + count]->debug_print("pf::array", 0, &proofPrinter); - congruenceClosures.push_back(pf.d_children[i + count]); - } - - Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; - - // Determine if the "target" of the congruence sequence appears right before or right after the sequence. - bool targetAppearsBefore = true; - bool targetAppearsAfter = true; - - if ((i == 0) || (i == 1 && neg == 0)) { - Debug("pf::array") << "Target does not appear before" << std::endl; - targetAppearsBefore = false; - } - - if ((i + count >= pf.d_children.size()) || - (!pf.d_children[i + count]->d_node.isNull() && - pf.d_children[i + count]->d_node.getKind() == kind::NOT)) { - Debug("pf::array") << "Target does not appear after" << std::endl; - targetAppearsAfter = false; - } - - // Assert that we have precisely one target clause. - Assert(targetAppearsBefore != targetAppearsAfter); - - // Begin breaking up the congruences and ordering the equalities correctly. - std::vector> orderedEqualities; - - // Insert target clause first. - if (targetAppearsBefore) { - orderedEqualities.push_back(pf.d_children[i - 1]); - // The target has already been added to subTrans; remove it. - subTrans->d_children.pop_back(); - } else { - orderedEqualities.push_back(pf.d_children[i + count]); - } - - // Start with the congruence closure closest to the target clause, and work our way back/forward. - if (targetAppearsBefore) { - for (unsigned j = 0; j < count; ++j) { - if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]); - if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]); - } - } else { - for (unsigned j = 0; j < count; ++j) { - if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]); - if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]); - } - } - - // Copy the result into the main transitivity proof. - subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); - - // Increase i to skip over the children that have been processed. - i += count; - if (targetAppearsAfter) { - ++i; - } - } - - // Else, just copy the child proof as is - else { - subTrans->d_children.push_back(pf.d_children[i]); - ++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()); - } + int neg = tp->assertAndPrint(pf, map, subTrans, &proofPrinter); 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) { + bool disequalityFound = (neg >= 0); + + 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); @@ -294,7 +128,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } out << "(clausify_false (contra _ "; - if (disequalityFound) { Node n2 = pf.d_children[neg]->d_node; Assert(n2.getKind() == kind::NOT); @@ -347,77 +180,95 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return Node(); } - if (pf.d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { - Debug("mgd") << "\nok, looking at congruence:\n"; - pf.debug_print("mgd", 0, &proofPrinter); - std::stack stk; - for (const theory::eq::EqProof* pf2 = &pf; - pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; - pf2 = pf2->d_children[0].get()) { - Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node - << std::endl; - Assert(!pf2->d_node.isNull()); - Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || - pf2->d_node.getKind() == kind::BUILTIN || - pf2->d_node.getKind() == kind::APPLY_UF || - pf2->d_node.getKind() == kind::SELECT || - pf2->d_node.getKind() == kind::PARTIAL_SELECT_0 || - pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 || - pf2->d_node.getKind() == kind::STORE); - - Assert(pf2->d_children.size() == 2); - out << "(cong _ _ _ _ _ _ "; - stk.push(pf2); - } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); - // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); - NodeBuilder<> b1, b2; - - const theory::eq::EqProof* pf2 = stk.top(); - stk.pop(); - Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); - Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map); - out << " "; - std::stringstream ss; - Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map); - - - Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd", 0, &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; - // - Debug("mgd") << "looking at " << pf2->d_node << "\n"; - Debug("mgd") << " " << n1 << "\n"; - Debug("mgd") << " " << n2 << "\n"; - - int side = 0; - if(match(pf2->d_node, n1[0])) { - Debug("mgd") << "SIDE IS 0\n"; - side = 0; - } 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", 0, &proofPrinter); + switch (pf.d_id) + { + case theory::eq::MERGED_THROUGH_CONGRUENCE: + { + Debug("mgd") << "\nok, looking at congruence:\n"; + pf.debug_print("mgd", 0, &proofPrinter); + std::stack stk; + for (const theory::eq::EqProof* pf2 = &pf; + pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; + pf2 = pf2->d_children[0].get()) + { + Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node + << std::endl; + Assert(!pf2->d_node.isNull()); + Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF + || pf2->d_node.getKind() == kind::BUILTIN + || pf2->d_node.getKind() == kind::APPLY_UF + || pf2->d_node.getKind() == kind::SELECT + || pf2->d_node.getKind() == kind::PARTIAL_SELECT_0 + || pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 + || pf2->d_node.getKind() == kind::STORE); + + Assert(pf2->d_children.size() == 2); + out << "(cong _ _ _ _ _ _ "; + stk.push(pf2); } - Assert(match(pf2->d_node, n1[1])); - side = 1; - } + Assert(stk.top()->d_children[0]->d_id + != theory::eq::MERGED_THROUGH_CONGRUENCE); + // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), + // b2(kind::PARTIAL_APPLY_UF); + NodeBuilder<> b1, b2; - if(n1[side].getKind() == kind::APPLY_UF || - n1[side].getKind() == kind::PARTIAL_APPLY_UF || - n1[side].getKind() == kind::SELECT || - n1[side].getKind() == kind::PARTIAL_SELECT_1 || - n1[side].getKind() == kind::STORE) { - if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) { - b1 << kind::PARTIAL_APPLY_UF; - b1 << n1[side].getOperator(); - } else if (n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::PARTIAL_SELECT_1) { - // b1 << n1[side].getKind(); - b1 << kind::SELECT; - } else { + const theory::eq::EqProof* pf2 = stk.top(); + stk.pop(); + Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); + Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map); + out << " "; + std::stringstream ss; + Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map); + + Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" + << "\n"; + pf2->debug_print("mgd", 0, &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; + // + Debug("mgd") << "looking at " << pf2->d_node << "\n"; + Debug("mgd") << " " << n1 << "\n"; + Debug("mgd") << " " << n2 << "\n"; + + int side = 0; + if (tp->match(pf2->d_node, n1[0])) + { + Debug("mgd") << "SIDE IS 0\n"; + side = 0; + } + else + { + Debug("mgd") << "SIDE IS 1\n"; + if (!tp->match(pf2->d_node, n1[1])) + { + Debug("mgd") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("mgd", 0, &proofPrinter); + } + Assert(tp->match(pf2->d_node, n1[1])); + side = 1; + } + + if (n1[side].getKind() == kind::APPLY_UF + || n1[side].getKind() == kind::PARTIAL_APPLY_UF + || n1[side].getKind() == kind::SELECT + || n1[side].getKind() == kind::PARTIAL_SELECT_1 + || n1[side].getKind() == kind::STORE) + { + if (n1[side].getKind() == kind::APPLY_UF + || n1[side].getKind() == kind::PARTIAL_APPLY_UF) + { + b1 << kind::PARTIAL_APPLY_UF; + b1 << n1[side].getOperator(); + } + else if (n1[side].getKind() == kind::SELECT + || n1[side].getKind() == kind::PARTIAL_SELECT_1) + { + // b1 << n1[side].getKind(); + b1 << kind::SELECT; + } else { b1 << kind::PARTIAL_APPLY_UF; b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); } @@ -539,13 +390,6 @@ 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.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n1.getOperator())) { b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); @@ -573,13 +417,6 @@ 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.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n2.getOperator())) { b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); @@ -590,22 +427,22 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2.append(n2.begin(), n2.end()); n2 = b2; } - Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); + Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1)); Debug("mgdx") << "\ncong proved: " << n << "\n"; return n; } - - else if (pf.d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + case 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); + return pf.d_node.eqNode(pf.d_node); } - - else if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY) { + case 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() << " ) = " << @@ -614,22 +451,8 @@ 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(), - map); - return pf.d_node; - } - - else if (pf.d_id == theory::eq::MERGED_THROUGH_TRANS) { + case theory::eq::MERGED_THROUGH_TRANS: + { bool firstNeg = false; bool secondNeg = false; @@ -643,6 +466,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node); Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); + Node n2; Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -650,134 +474,117 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, bool identicalEqualities = false; bool evenLengthSequence; - Node nodeAfterEqualitySequence; + std::stringstream dontCare; + Node nodeAfterEqualitySequence = + toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map); std::map childToStream; - for(size_t i = 1; i < pf.d_children.size(); ++i) { + std::stringstream ss1(ss.str()), ss2; + std::pair nodePair; + for (size_t i = 1; i < pf.d_children.size(); ++i) + { std::stringstream ss1(ss.str()), ss2; ss.str(""); - // In congruences, we can have something like a[x] - it's important to keep these, - // and not turn them into (a[x]=true), because that will mess up the congruence application + // In congruences, we can have something like a[x] - it's important to + // keep these, + // and not turn them into (a[x]=true), because that will mess up the + // congruence application // later. if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) - pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node); + pf.d_children[i]->d_node = + simplifyBooleanNode(pf.d_children[i]->d_node); - // It is possible that we've already converted the i'th child to stream. If so, + // It is possible that we've already converted the i'th child to stream. + // If so, // use previously stored result. Otherwise, convert and store. Node n2; if (childToStream.find(i) != childToStream.end()) n2 = childToStream[i]; - else { + else + { n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map); childToStream[i] = n2; } Debug("mgd") << "\ndoing trans proof, got (first) n2 " << n2 << "\n"; - // The following branch is dedicated to handling sequences of identical equalities, + // The following branch is dedicated to handling sequences of identical + // equalities, // i.e. trans[ a=b, a=b, a=b ]. // // There are two cases: - // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality, + // 1. The number of equalities is odd. Then, the sequence can be + // collapsed to just one equality, // i.e. a=b. - // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this, - // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs - // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, + // 2. The number of equalities is even. Now, we have two options: a=a + // or b=b. To determine this, + // we look at the node after the equality sequence. If it needs a, + // we go for a=a; and if it needs + // b, we go for b=b. If there is no following node, we look at the + // goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL) { - if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { + if (n2.getKind() == kind::EQUAL) + { + if (((n1[0] == n2[0]) && (n1[1] == n2[1])) + || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) + { // We are in a sequence of identical equalities - Debug("pf::array") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + Debug("pf::array") << "Detected identical equalities: " << std::endl + << "\t" << n1 << std::endl; - if (!identicalEqualities) { + if (!identicalEqualities) + { // The sequence of identical equalities has started just now identicalEqualities = true; - Debug("pf::array") << "The sequence is just beginning. Determining length..." << std::endl; + Debug("pf::array") + << "The sequence is just beginning. Determining length..." + << std::endl; // Determine whether the length of this sequence is odd or even. evenLengthSequence = true; bool sequenceOver = false; size_t j = i + 1; - while (j < pf.d_children.size() && !sequenceOver) { + while (j < pf.d_children.size() && !sequenceOver) + { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map ); - - if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || - ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { + nodeAfterEqualitySequence = toStreamRecLFSC( + dontCare, tp, *(pf.d_children[j]), tb + 1, map); + if (((nodeAfterEqualitySequence[0] == n1[0]) + && (nodeAfterEqualitySequence[1] == n1[1])) + || ((nodeAfterEqualitySequence[0] == n1[1]) + && (nodeAfterEqualitySequence[1] == n1[0]))) + { evenLengthSequence = !evenLengthSequence; - } else { + } + else + { sequenceOver = true; } ++j; } - if (evenLengthSequence) { - // If the length is even, we need to apply transitivity for the "correct" hand of the equality. - - Debug("pf::array") << "Equality sequence of even length" << std::endl; - Debug("pf::array") << "n1 is: " << n1 << std::endl; - Debug("pf::array") << "n2 is: " << n2 << std::endl; - Debug("pf::array") << "pf-d_node is: " << pf.d_node << std::endl; - Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence << std::endl; - - ss << "(trans _ _ _ _ "; - - // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us. - if (!sequenceOver) { - if (match(n1[0], pf.d_node[0])) { - n1 = eqNode(n1[0], n1[0]); - ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - } else if (match(n1[1], pf.d_node[1])) { - n1 = eqNode(n1[1], n1[1]); - ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); - } else { - Debug("pf::array") << "Error: identical equalities over, but hands don't match what we're proving." - << std::endl; - Assert(false); - } - } else { - // We have a "next node". Use it to guide us. - if (nodeAfterEqualitySequence.getKind() == kind::NOT) { - nodeAfterEqualitySequence = nodeAfterEqualitySequence[0]; - } - - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); - - if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { - - // Eliminate n1[1] - ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - n1 = eqNode(n1[0], n1[0]); - - } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) { - - // Eliminate n1[0] - ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); - n1 = eqNode(n1[1], n1[1]); - - } else { - Debug("pf::array") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; - Assert(false); - } - } - - ss << ")"; - - } else { - Debug("pf::array") << "Equality sequence length is odd!" << std::endl; - ss.str(ss1.str()); - } - - Debug("pf::array") << "Have proven: " << n1 << std::endl; - } else { + nodePair = + tp->identicalEqualitiesPrinterHelper(evenLengthSequence, + sequenceOver, + pf, + map, + ss1.str(), + &ss, + n1, + nodeAfterEqualitySequence); + n1 = nodePair.first; + nodeAfterEqualitySequence = nodePair.second; + } + else + { ss.str(ss1.str()); } @@ -786,18 +593,23 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } } - if (identicalEqualities) { - // We were in a sequence of identical equalities, but it has now ended. Resume normal operation. + if (identicalEqualities) + { + // We were in a sequence of identical equalities, but it has now ended. + // Resume normal operation. identicalEqualities = false; } Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; - if(tb == 1) { + if (tb == 1) + { Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n"; - if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { - Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; + if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) + { + Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " + << n2[0].getId() << " " << n2[1].getId() << "\n"; Debug("mgdx") << n1[0].getId() << " " << n1[0] << "\n"; Debug("mgdx") << n1[1].getId() << " " << n1[1] << "\n"; Debug("mgdx") << n2[0].getId() << " " << n2[0] << "\n"; @@ -836,29 +648,29 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, { if(n1[0] == n2[0]) { if(tb == 1) { Debug("mgdx") << "case 1\n"; } - n1 = eqNode(n1[1], n2[1]); + n1 = n1[1].eqNode(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]); + n1 = n1[0].eqNode(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]); + n1 = n2[0].eqNode(n1[1]); ss << ss2.str() << " " << ss1.str(); } else if (firstNeg) { - n1 = eqNode(n1[1], n2[0]); + n1 = n1[1].eqNode(n2[0]); ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; } else { Assert(secondNeg); - n1 = eqNode(n1[1], n2[0]); + n1 = n1[1].eqNode(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]); + n1 = n1[0].eqNode(n2[1]); ss << ss1.str() << " " << ss2.str(); } else { Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; @@ -912,246 +724,312 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n1; } - else if (pf.d_id == d_reasonRow) { - Debug("mgd") << "row lemma: " << pf.d_node << std::endl; - Assert(pf.d_node.getKind() == kind::EQUAL); - - - if (pf.d_node[1].getKind() == kind::SELECT) { - // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k). - 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("mgd") << "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("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } + case 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()); - // inner index != outer index - // t3 is the outer index + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( + out, n[0].toExpr(), n[1].toExpr(), map); + return pf.d_node; + } - Assert(pf.d_children.size() == 1); - std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); + default: + { + if (pf.d_id == d_reasonRow) + { + Debug("mgd") << "row lemma: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::EQUAL); - 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 << " "; + if (pf.d_node[1].getKind() == kind::SELECT) + { + // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof + // explains why (i != k). + 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("mgd") << "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("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 + << "\nt4 " << t4 << "\n"; + } + // inner index != outer index + // t3 is the outer index - Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node - << ". t3 is: " << t3 << std::endl - << "subproof is: " << subproof << std::endl; + Assert(pf.d_children.size() == 1); + std::stringstream ss; + Node subproof = + toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); - Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + 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 << " "; - // The subproof needs to show that t2 != t3. This can either be a direct disequality, - // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant. - if (subproof.getKind() == kind::NOT) { - // The subproof is for t2 != t3 (or t3 != t2) - 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() << ")"; - } - } else { - // Either t2 or t3 is a constant. - Assert(subproof.getKind() == kind::EQUAL); - Assert(subproof[0].isConst() || subproof[1].isConst()); - Assert(t2.isConst() || t3.isConst()); - Assert(!(t2.isConst() && t3.isConst())); - - bool t2IsConst = t2.isConst(); - if (subproof[0].isConst()) { - if (t2IsConst) { - // (t3 == subproof[1]) == subproof[0] != t2 - // goal is t2 != t3 - // subproof already shows constant = t3 - Assert(t3 == subproof[1]); - out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr(), map); - out << " "; - out << ss.str(); - out << ")"; - } else { - Assert(t2 == subproof[1]); - out << "(negsymm _ _ _ "; - out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr(), map); - out << " "; + Debug("pf::array") << "pf.d_children[0]->d_node is: " + << pf.d_children[0]->d_node << ". t3 is: " << t3 + << std::endl + << "subproof is: " << subproof << std::endl; + + Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + + // The subproof needs to show that t2 != t3. This can either be a direct + // disequality, + // or, if (wlog) t2 is constant, it can show that t3 is equal to another + // constant. + if (subproof.getKind() == kind::NOT) + { + // The subproof is for t2 != t3 (or t3 != t2) + if (subproof[0][1] == t3) + { + Debug("pf::array") << "Dont need symmetry!" << std::endl; out << ss.str(); - out << "))"; } - } else { - if (t2IsConst) { - // (t3 == subproof[0]) == subproof[1] != t2 - // goal is t2 != t3 - // subproof already shows constant = t3 - Assert(t3 == subproof[0]); - out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr(), map); - out << " "; - out << "(symm _ _ _ " << ss.str() << ")"; - out << ")"; - } else { - Assert(t2 == subproof[0]); - out << "(negsymm _ _ _ "; - out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr(), map); - out << " "; - out << "(symm _ _ _ " << ss.str() << ")"; - out << "))"; + else + { + Debug("pf::array") << "Need symmetry!" << std::endl; + out << "(negsymm _ _ _ " << ss.str() << ")"; + } + } + else + { + // Either t2 or t3 is a constant. + Assert(subproof.getKind() == kind::EQUAL); + Assert(subproof[0].isConst() || subproof[1].isConst()); + Assert(t2.isConst() || t3.isConst()); + Assert(!(t2.isConst() && t3.isConst())); + + bool t2IsConst = t2.isConst(); + if (subproof[0].isConst()) + { + if (t2IsConst) + { + // (t3 == subproof[1]) == subproof[0] != t2 + // goal is t2 != t3 + // subproof already shows constant = t3 + Assert(t3 == subproof[1]); + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof( + out, t2.toExpr(), subproof[0].toExpr(), map); + out << " "; + out << ss.str(); + out << ")"; + } + else + { + Assert(t2 == subproof[1]); + out << "(negsymm _ _ _ "; + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof( + out, t3.toExpr(), subproof[0].toExpr(), map); + out << " "; + out << ss.str(); + out << "))"; + } + } + else + { + if (t2IsConst) + { + // (t3 == subproof[0]) == subproof[1] != t2 + // goal is t2 != t3 + // subproof already shows constant = t3 + Assert(t3 == subproof[0]); + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof( + out, t2.toExpr(), subproof[1].toExpr(), map); + out << " "; + out << "(symm _ _ _ " << ss.str() << ")"; + out << ")"; + } + else + { + Assert(t2 == subproof[0]); + out << "(negsymm _ _ _ "; + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof( + out, t3.toExpr(), subproof[1].toExpr(), map); + out << " "; + out << "(symm _ _ _ " << ss.str() << ")"; + out << "))"; + } } } - } - - out << ")"; - return ret; - } else { - Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl; - - Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node << std::endl; - // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k]) + out << ")"; + return ret; + } + else + { + Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl; + + Debug("pf::array") << "pf.d_children[0]->d_node is: " + << pf.d_children[0]->d_node << std::endl; + + // This is the case where (i == k), and the sub-proof explains why + // ((a[i]:=t)[k] != a[k]) + + // If we wanted to remove the need for "negativerow", we would need to + // prove i==k using a new satlem. We would: + // 1. Create a new satlem. + // 2. Assume that i != k + // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k]) + // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), + // obtaining our contradiction + + TNode t1, t2, t3, t4; + Node ret; + + // pf.d_node is an equality, i==k. + t1 = pf.d_node[0]; + t2 = pf.d_node[1]; + + // pf.d_children[0]->d_node will have the form: (not (= (select (store + // a_565 i7 e_566) i1) (select a_565 i1))), + // or its symmetrical version. + + unsigned side; + if (pf.d_children[0]->d_node[0][0].getKind() == kind::SELECT + && pf.d_children[0]->d_node[0][0][0].getKind() == kind::STORE) + { + side = 0; + } + else if (pf.d_children[0]->d_node[0][1].getKind() == kind::SELECT + && pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE) + { + side = 1; + } + else + { + Unreachable(); + } - // If we wanted to remove the need for "negativerow", we would need to prove i==k using a new satlem. We would: - // 1. Create a new satlem. - // 2. Assume that i != k - // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k]) - // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), obtaining our contradiction + Debug("pf::array") << "Side is: " << side << std::endl; - TNode t1, t2, t3, t4; - Node ret; + // The array's index and element types will come from the subproof... + t3 = pf.d_children[0]->d_node[0][side][0][0]; + t4 = pf.d_children[0]->d_node[0][side][0][2]; + ret = pf.d_node; - // pf.d_node is an equality, i==k. - t1 = pf.d_node[0]; - t2 = pf.d_node[1]; + // 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]); - // pf.d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))), - // or its symmetrical version. + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " + << t4 << "\n"; - unsigned side; - if (pf.d_children[0]->d_node[0][0].getKind() == kind::SELECT && - pf.d_children[0]->d_node[0][0][0].getKind() == kind::STORE) { - side = 0; - } else if (pf.d_children[0]->d_node[0][1].getKind() == kind::SELECT && - pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE) { - side = 1; - } - else { - Unreachable(); - } + Assert(pf.d_children.size() == 1); + std::stringstream ss; + Node subproof = + toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); - Debug("pf::array") << "Side is: " << side << std::endl; + Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; - // The array's index and element types will come from the subproof... - t3 = pf.d_children[0]->d_node[0][side][0][0]; - t4 = pf.d_children[0]->d_node[0][side][0][2]; - ret = pf.d_node; + if (swap) + { + out << "(symm _ _ _ "; + } - // 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]); + out << "(negativerow _ _ "; + tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); + out << " "; + tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << " "; + tp->printTerm(t4.toExpr(), out, map); + out << " "; - Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + if (side != 0) + { + out << "(negsymm _ _ _ " << ss.str() << ")"; + } + else + { + out << ss.str(); + } - Assert(pf.d_children.size() == 1); - std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); + out << ")"; - Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + if (swap) + { + out << ") "; + } - if (swap) { - out << "(symm _ _ _ "; + return ret; } - - out << "(negativerow _ _ "; - tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); + } + 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; + 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("mgd") << "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("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + } + out << "(row1 _ _ "; + 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(); - } - out << ")"; - - if (swap) { - out << ") "; - } - return ret; - } - } - - 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; - 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("mgd") << "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("mgd") << "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; } - else if (pf.d_id == d_reasonExt) { Assert(pf.d_node.getKind() == kind::NOT); Assert(pf.d_node[0].getKind() == kind::EQUAL); @@ -1186,11 +1064,14 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf.d_node; } } + } +} ArrayProof::ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* pe) : TheoryProof(arrays, pe) {} +theory::TheoryId ArrayProof::getTheoryId() { return theory::THEORY_ARRAYS; } void ArrayProof::registerTerm(Expr term) { // already registered if (d_declarations.find(term) != d_declarations.end()) @@ -1214,8 +1095,10 @@ void ArrayProof::registerTerm(Expr term) { if (term.getKind() == kind::SELECT && term.getType().isBoolean()) { // Ensure cnf literals Node asNode(term); - ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true))); - ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false))); + ProofManager::currentPM()->ensureLiteral( + asNode.eqNode(NodeManager::currentNM()->mkConst(true))); + ProofManager::currentPM()->ensureLiteral( + asNode.eqNode(NodeManager::currentNM()->mkConst(false))); } // recursively declare all other terms diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 779624df0..ea865f9d8 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -79,8 +79,9 @@ protected: ExprSet d_declarations; // all the variable/function declarations ExprSet d_skolemDeclarations; // all the skolem variable declarations std::map d_skolemToLiteral; + theory::TheoryId getTheoryId(); -public: + public: ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine); std::string skolemToLiteral(Expr skolem); diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 7a2faba37..afddfd323 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -51,6 +51,7 @@ void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true); } +theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) { Assert (d_cnfProof == NULL); diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index b5487a352..a41d5d515 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -83,7 +83,7 @@ protected: std::map d_constantLetMap; bool d_useConstantLetification; - + theory::TheoryId getTheoryId(); context::Context d_fakeContext; public: BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 0dd573dc6..34f3a92ec 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -29,6 +29,7 @@ #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof.h" +#include "proof/simplify_boolean_node.h" #include "proof/uf_proof.h" #include "prop/sat_solver_types.h" #include "smt/smt_engine.h" @@ -38,13 +39,11 @@ #include "theory/bv/theory_bv.h" #include "theory/output_channel.h" #include "theory/term_registration_visitor.h" -#include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/valuation.h" #include "util/hash.h" #include "util/proof.h" - namespace CVC4 { unsigned CVC4::ProofLetCount::counter = 0; @@ -1099,6 +1098,7 @@ void BooleanProof::registerTerm(Expr term) { } } +theory::TheoryId BooleanProof::getTheoryId() { return theory::THEORY_BOOL; } void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { Node falseNode = NodeManager::currentNM()->mkConst(false); Node trueNode = NodeManager::currentNM()->mkConst(true); @@ -1264,4 +1264,373 @@ void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node os << "))"; } +inline bool TheoryProof::match(TNode n1, TNode n2) +{ + theory::TheoryId theoryId = this->getTheoryId(); + ProofManager* pm = ProofManager::currentPM(); + bool ufProof = (theoryId == theory::THEORY_UF); + Debug(ufProof ? "pf::uf" : "mgd") << "match " << n1 << " " << n2 << std::endl; + if (pm->hasOp(n1)) + { + n1 = pm->lookupOp(n1); + } + if (pm->hasOp(n2)) + { + n2 = pm->lookupOp(n2); + } + Debug(ufProof ? "pf::uf" : "mgd") << "+ match " << n1 << " " << n2 + << std::endl; + if (!ufProof) + { + Debug("pf::array") << "+ match: step 1" << std::endl; + } + if (n1 == n2) + { + return true; + } + + if (n1.getType().isFunction() && n2.hasOperator()) + { + if (pm->hasOp(n2.getOperator())) + { + return n1 == pm->lookupOp(n2.getOperator()); + } + else + { + return n1 == n2.getOperator(); + } + } + + if (n2.getType().isFunction() && n1.hasOperator()) + { + if (pm->hasOp(n1.getOperator())) + { + return n2 == pm->lookupOp(n1.getOperator()); + } + else + { + return n2 == n1.getOperator(); + } + } + + if (n1.hasOperator() && n2.hasOperator() + && n1.getOperator() != n2.getOperator()) + { + if (ufProof + || !((n1.getKind() == kind::SELECT + && n2.getKind() == kind::PARTIAL_SELECT_0) + || (n1.getKind() == kind::SELECT + && n2.getKind() == kind::PARTIAL_SELECT_1) + || (n1.getKind() == kind::PARTIAL_SELECT_1 + && n2.getKind() == kind::SELECT) + || (n1.getKind() == kind::PARTIAL_SELECT_1 + && n2.getKind() == kind::PARTIAL_SELECT_0) + || (n1.getKind() == kind::PARTIAL_SELECT_0 + && n2.getKind() == kind::SELECT) + || (n1.getKind() == kind::PARTIAL_SELECT_0 + && n2.getKind() == kind::PARTIAL_SELECT_1))) + { + return false; + } + } + + for (size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) + { + if (n1[i] != n2[i]) + { + return false; + } + } + + return true; +} + +int TheoryProof::assertAndPrint( + const theory::eq::EqProof& pf, + const ProofLetMap& map, + std::shared_ptr subTrans, + theory::eq::EqProof::PrettyPrinter* pPrettyPrinter) +{ + theory::TheoryId theoryId = getTheoryId(); + int neg = -1; + Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS); + bool ufProof = (theoryId == theory::THEORY_UF); + std::string theoryName = theory::getStatsPrefix(theoryId); + pf.debug_print(("pf::" + theoryName).c_str(), 0, pPrettyPrinter); + Debug("pf::" + theoryName) << std::endl; + + Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.size() >= 2); + + subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; + subTrans->d_node = pf.d_node; + + size_t i = 0; + while (i < pf.d_children.size()) + { + // special treatment for uf and not for array + if (ufProof + || pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + { + pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node); + } + + // Look for the negative clause, with which we will form a contradiction. + if (!pf.d_children[i]->d_node.isNull() + && pf.d_children[i]->d_node.getKind() == kind::NOT) + { + Assert(neg < 0); + (neg) = i; + ++i; + } + + // Handle congruence closures over equalities. + else if (pf.d_children[i]->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE + && pf.d_children[i]->d_node.isNull()) + { + Debug("pf::" + theoryName) << "Handling congruence over equalities" + << std::endl; + + // Gather the sequence of consecutive congruence closures. + std::vector> + congruenceClosures; + unsigned count; + Debug("pf::" + theoryName) << "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(); + ++count) + { + Debug("pf::" + theoryName) << "Found a congruence: " << std::endl; + pf.d_children[i + count]->debug_print( + ("pf::" + theoryName).c_str(), 0, pPrettyPrinter); + congruenceClosures.push_back(pf.d_children[i + count]); + } + + Debug("pf::" + theoryName) + << "Total number of congruences found: " << congruenceClosures.size() + << std::endl; + + // Determine if the "target" of the congruence sequence appears right + // before or right after the sequence. + bool targetAppearsBefore = true; + bool targetAppearsAfter = true; + + if ((i == 0) || (i == 1 && neg == 0)) + { + Debug("pf::" + theoryName) << "Target does not appear before" + << std::endl; + targetAppearsBefore = false; + } + + if ((i + count >= pf.d_children.size()) + || (!pf.d_children[i + count]->d_node.isNull() + && pf.d_children[i + count]->d_node.getKind() == kind::NOT)) + { + Debug("pf::" + theoryName) << "Target does not appear after" + << std::endl; + targetAppearsAfter = false; + } + + // Flow changes between uf and array + if (ufProof) + { + // Assert that we have precisely at least one possible clause. + Assert(targetAppearsBefore || targetAppearsAfter); + + // If both are valid, assume the one after the sequence is correct + if (targetAppearsAfter && targetAppearsBefore) + { + targetAppearsBefore = false; + } + } + else + { // not a uf proof + // Assert that we have precisely one target clause. + Assert(targetAppearsBefore != targetAppearsAfter); + } + + // Begin breaking up the congruences and ordering the equalities + // correctly. + std::vector> orderedEqualities; + + // Insert target clause first. + if (targetAppearsBefore) + { + orderedEqualities.push_back(pf.d_children[i - 1]); + // The target has already been added to subTrans; remove it. + subTrans->d_children.pop_back(); + } + else + { + orderedEqualities.push_back(pf.d_children[i + count]); + } + + // Start with the congruence closure closest to the target clause, and + // work our way back/forward. + if (targetAppearsBefore) + { + for (unsigned j = 0; j < count; ++j) + { + if (pf.d_children[i + j]->d_children[0]->d_id + != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), + pf.d_children[i + j]->d_children[0]); + if (pf.d_children[i + j]->d_children[1]->d_id + != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), + pf.d_children[i + j]->d_children[1]); + } + } + else + { + for (unsigned j = 0; j < count; ++j) + { + if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id + != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert( + orderedEqualities.begin(), + pf.d_children[i + count - 1 - j]->d_children[0]); + if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id + != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert( + orderedEqualities.end(), + pf.d_children[i + count - 1 - j]->d_children[1]); + } + } + + // Copy the result into the main transitivity proof. + subTrans->d_children.insert(subTrans->d_children.end(), + orderedEqualities.begin(), + orderedEqualities.end()); + + // Increase i to skip over the children that have been processed. + i += count; + if (targetAppearsAfter) + { + ++i; + } + } + + // Else, just copy the child proof as is + else + { + subTrans->d_children.push_back(pf.d_children[i]); + ++i; + } + } + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) + { + Debug("pf::" + theoryName) + << "A disequality was NOT found. UNSAT due to merged constants" + << std::endl; + Debug("pf::" + theoryName) << "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()); + } + return neg; +} + +std::pair TheoryProof::identicalEqualitiesPrinterHelper( + bool evenLengthSequence, + bool sequenceOver, + const theory::eq::EqProof& pf, + const ProofLetMap& map, + const std::string subproofStr, + std::stringstream* outStream, + Node n, + Node nodeAfterEqualitySequence) +{ + theory::TheoryId theoryId = getTheoryId(); + Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS); + bool ufProof = (theoryId == theory::THEORY_UF); + std::string theoryName = theory::getStatsPrefix(theoryId); + if (evenLengthSequence) + { + // If the length is even, we need to apply transitivity for the "correct" + // hand of the equality. + + Debug("pf::" + theoryName) << "Equality sequence of even length" + << std::endl; + Debug("pf::" + theoryName) << "n1 is: " << n << std::endl; + Debug("pf::" + theoryName) << "pf-d_node is: " << pf.d_node << std::endl; + Debug("pf::" + theoryName) << "Next node is: " << nodeAfterEqualitySequence + << std::endl; + + (*outStream) << "(trans _ _ _ _ "; + + // If the sequence is at the very end of the transitivity proof, use + // pf.d_node to guide us. + if (!sequenceOver) + { + if (match(n[0], pf.d_node[0])) + { + n = n[0].eqNode(n[0]); + (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")"; + } + else if (match(n[1], pf.d_node[1])) + { + n = n[1].eqNode(n[1]); + (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr; + } + else + { + Debug("pf::" + theoryName) << "Error: identical equalities over, but " + "hands don't match what we're proving." + << std::endl; + Assert(false); + } + } + else + { + // We have a "next node". Use it to guide us. + if (!ufProof && nodeAfterEqualitySequence.getKind() == kind::NOT) + { + nodeAfterEqualitySequence = nodeAfterEqualitySequence[0]; + } + + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); + + if ((n[0] == nodeAfterEqualitySequence[0]) + || (n[0] == nodeAfterEqualitySequence[1])) + { + // Eliminate n[1] + (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")"; + n = n[0].eqNode(n[0]); + } + else if ((n[1] == nodeAfterEqualitySequence[0]) + || (n[1] == nodeAfterEqualitySequence[1])) + { + // Eliminate n[0] + (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr; + n = n[1].eqNode(n[1]); + } + else + { + Debug("pf::" + theoryName) << "Error: even length sequence, but I " + "don't know which hand to keep!" + << std::endl; + Assert(false); + } + } + + (*outStream) << ")"; + } + else + { + Debug("pf::" + theoryName) << "Equality sequence length is odd!" + << std::endl; + (*outStream).str(subproofStr); + } + + Debug("pf::" + theoryName) << "Have proven: " << n << std::endl; + return std::make_pair(n, nodeAfterEqualitySequence); +} + } /* namespace CVC4 */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 4e599f570..efe05bce8 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -26,10 +26,10 @@ #include "expr/expr.h" #include "proof/clause_id.h" +#include "proof/proof_utils.h" #include "prop/sat_solver_types.h" +#include "theory/uf/equality_engine.h" #include "util/proof.h" -#include "proof/proof_utils.h" - namespace CVC4 { namespace theory { @@ -207,7 +207,9 @@ protected: // Pointer to the theory for this proof theory::Theory* d_theory; TheoryProofEngine* d_proofEngine; -public: + virtual theory::TheoryId getTheoryId() = 0; + + public: TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine) : d_theory(th) , d_proofEngine(proofEngine) @@ -238,6 +240,54 @@ public: void printSort(Type type, std::ostream& os) { d_proofEngine->printSort(type, os); } + + // congrence matching term helper + inline bool match(TNode n1, TNode n2); + + /** + * Helper function for ProofUF::toStreamRecLFSC and + * ProofArray::toStreamRecLFSC + * Inputs: + * - pf: equality engine proof + * - map: A map for the let-expressions in the proof + * - subTrans: main transitivity proof part + * - pPrettyPrinter: optional pretty printer for sub-proofs + * returns: + * - the index of the contradicting node in pf. + * */ + int assertAndPrint( + const theory::eq::EqProof& pf, + const ProofLetMap& map, + std::shared_ptr subTrans, + theory::eq::EqProof::PrettyPrinter* pPrettyPrinter = nullptr); + + /** + * Helper function for ProofUF::toStreamRecLFSC and + * ProofArray::toStreamRecLFSC + * Inputs: + * - evenLengthSequence: true iff the length of the sequence + * of the identical equalities is even. + * - sequenceOver: have we reached the last equality of this sequence? + * - pf: equality engine proof + * - map: A map for the let-expressions in the proof + * - subproofStr: current stringstream content + * - outStream: output stream to which the proof is printed + * - n: transitivity sub-proof + * - nodeAfterEqualitySequence: The node after the identical sequence. + * Returns: + * A pair of nodes, that are the updated nodes n and nodeAfterEqualitySequence + * + */ + std::pair identicalEqualitiesPrinterHelper( + bool evenLengthSequence, + bool sequenceOver, + const theory::eq::EqProof& pf, + const ProofLetMap& map, + const std::string subproofStr, + std::stringstream* outStream, + Node n, + Node nodeAfterEqualitySequence); + /** * Print the proof representation of the given type that belongs to THIS theory. * @@ -313,7 +363,9 @@ public: class BooleanProof : public TheoryProof { protected: ExprSet d_declarations; // all the boolean variables -public: + theory::TheoryId getTheoryId(); + + public: BooleanProof(TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 746cbbc54..9f7ae7ac1 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -24,48 +24,6 @@ namespace CVC4 { -inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); -} - -// congrence matching term helper -inline static bool match(TNode n1, TNode n2) { - Debug("pf::uf") << "match " << n1 << " " << n2 << std::endl; - if(ProofManager::currentPM()->hasOp(n1)) { - n1 = ProofManager::currentPM()->lookupOp(n1); - } - if(ProofManager::currentPM()->hasOp(n2)) { - n2 = ProofManager::currentPM()->lookupOp(n2); - } - Debug("pf::uf") << "+ match " << n1 << " " << n2 << std::endl; - if(n1 == n2) { - return true; - } - if(n1.getType().isFunction() && n2.hasOperator()) { - if(ProofManager::currentPM()->hasOp(n2.getOperator())) { - return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator()); - } else { - return n1 == n2.getOperator(); - } - } - if(n2.getType().isFunction() && n1.hasOperator()) { - if(ProofManager::currentPM()->hasOp(n1.getOperator())) { - return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator()); - } else { - return n2 == n1.getOperator(); - } - } - if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) { - return false; - } - for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) { - if(n1[i] != n2[i]) { - return false; - } - } - return true; -} - void ProofUF::toStream(std::ostream& out) const { ProofLetMap map; @@ -101,10 +59,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf.debug_print("pf::uf"); - Debug("pf::uf") << std::endl; - - if (tb == 0) { + if (tb == 0) + { // Special case: false was an input, so the proof is just "false". if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY && pf.d_node == NodeManager::currentNM()->mkConst(false)) { @@ -114,149 +70,38 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, return Node(); } - Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); - Assert(!pf.d_node.isNull()); - Assert(pf.d_children.size() >= 2); - - int neg = -1; std::shared_ptr subTrans = std::make_shared(); - subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; - subTrans->d_node = pf.d_node; - - size_t i = 0; - - while (i < pf.d_children.size()) { - pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node); - - // Look for the negative clause, with which we will form a contradiction. - if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) { - Assert(neg < 0); - Node node = pf.d_children[i]->d_node[0]; - neg = i; - ++i; - } - - // Handle congruence closures over equalities. - else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) { - Debug("pf::uf") << "Handling congruence over equalities" << std::endl; - - // Gather the sequence of consecutive congruence closures. - std::vector> congruenceClosures; - unsigned count; - Debug("pf::uf") << "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(); - ++count) { - Debug("pf::uf") << "Found a congruence: " << std::endl; - pf.d_children[i+count]->debug_print("pf::uf"); - congruenceClosures.push_back(pf.d_children[i+count]); - } - - Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; - // Determine if the "target" of the congruence sequence appears right before or right after the sequence. - bool targetAppearsBefore = true; - bool targetAppearsAfter = true; - - if ((i == 0) || (i == 1 && neg == 0)) { - Debug("pf::uf") << "Target does not appear before" << std::endl; - targetAppearsBefore = false; - } - - if ((i + count >= pf.d_children.size()) || - (!pf.d_children[i + count]->d_node.isNull() && - pf.d_children[i + count]->d_node.getKind() == kind::NOT)) { - Debug("pf::uf") << "Target does not appear after" << std::endl; - targetAppearsAfter = false; - } - - // Assert that we have precisely at least one possible clause. - Assert(targetAppearsBefore || targetAppearsAfter); - - // If both are valid, assume the one after the sequence is correct - if (targetAppearsAfter && targetAppearsBefore) - targetAppearsBefore = false; - - // Begin breaking up the congruences and ordering the equalities correctly. - std::vector> orderedEqualities; - - // Insert target clause first. - if (targetAppearsBefore) { - orderedEqualities.push_back(pf.d_children[i - 1]); - // The target has already been added to subTrans; remove it. - subTrans->d_children.pop_back(); - } else { - orderedEqualities.push_back(pf.d_children[i + count]); - } - - // Start with the congruence closure closest to the target clause, and work our way back/forward. - if (targetAppearsBefore) { - for (unsigned j = 0; j < count; ++j) { - if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]); - if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]); - } - } else { - for (unsigned j = 0; j < count; ++j) { - if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]); - if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]); - } - } - - // Copy the result into the main transitivity proof. - subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); - - // Increase i to skip over the children that have been processed. - i += count; - if (targetAppearsAfter) { - ++i; - } - } - - // Else, just copy the child proof as is - else { - subTrans->d_children.push_back(pf.d_children[i]); - ++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()); - } + int neg = tp->assertAndPrint(pf, map, subTrans); Node n1; - std::stringstream ss; + std::stringstream ss, ss2; Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n"; + bool disequalityFound = (neg >= 0); if(!disequalityFound || subTrans->d_children.size() >= 2) { n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map); - Debug("pf::uf") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + 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; out << "(clausify_false (contra _ "; - if (disequalityFound) { Node n2 = pf.d_children[neg]->d_node; Assert(n2.getKind() == kind::NOT); Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][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) { @@ -289,7 +134,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, out << ss.str(); out << " "; - ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr(), map); + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( + out, n1[0].toExpr(), n1[1].toExpr(), map); out << "))" << std::endl; } @@ -305,7 +151,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0].get()) { Assert(!pf2->d_node.isNull()); - Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE); + Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF + || pf2->d_node.getKind() == kind::BUILTIN + || pf2->d_node.getKind() == kind::APPLY_UF + || pf2->d_node.getKind() == kind::SELECT + || pf2->d_node.getKind() == kind::STORE); Assert(pf2->d_children.size() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); @@ -325,7 +175,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, Debug("pf::uf") << " " << n1 << "\n"; Debug("pf::uf") << " " << n2 << "\n"; int side = 0; - if(match(pf2->d_node, n1[0])) { + if (tp->match(pf2->d_node, n1[0])) + { //if(tb == 1) { Debug("pf::uf") << "SIDE IS 0\n"; //} @@ -334,15 +185,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, //if(tb == 1) { Debug("pf::uf") << "SIDE IS 1\n"; //} - if(!match(pf2->d_node, n1[1])) { + if (!tp->match(pf2->d_node, n1[1])) + { Debug("pf::uf") << "IN BAD CASE, our first subproof is\n"; pf2->d_children[0]->debug_print("pf::uf"); } - Assert(match(pf2->d_node, n1[1])); + Assert(tp->match(pf2->d_node, n1[1])); side = 1; } - if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) { - if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) { + if (n1[side].getKind() == kind::APPLY_UF + || n1[side].getKind() == kind::PARTIAL_APPLY_UF + || n1[side].getKind() == kind::SELECT + || n1[side].getKind() == kind::STORE) + { + if (n1[side].getKind() == kind::APPLY_UF + || n1[side].getKind() == kind::PARTIAL_APPLY_UF) + { b1 << n1[side].getOperator(); } else { b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); @@ -352,7 +210,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, b1 << n1[side]; } if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) { - if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) { + if (n1[1 - side].getKind() == kind::PARTIAL_APPLY_UF + || n1[1 - side].getKind() == kind::APPLY_UF) + { b2 << n1[1-side].getOperator(); } else { b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); @@ -435,7 +295,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, b2.append(n2.begin(), n2.end()); n2 = b2; } - Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); + Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1)); if(tb == 1) { Debug("pf::uf") << "\ncong proved: " << n << "\n"; } @@ -443,13 +303,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, } case 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); - + return pf.d_node.eqNode(pf.d_node); + } case theory::eq::MERGED_THROUGH_EQUALITY: Assert(!pf.d_node.isNull()); Assert(pf.d_children.empty()); @@ -468,128 +329,109 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; + Node n2; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n"; } bool identicalEqualities = false; bool evenLengthSequence; - Node nodeAfterEqualitySequence; + std::stringstream dontCare; + Node nodeAfterEqualitySequence = + toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map); std::map childToStream; - + std::stringstream ss1(ss.str()), ss2; + std::pair nodePair; for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node); - // It is possible that we've already converted the i'th child to stream. If so, + // It is possible that we've already converted the i'th child to stream. + // If so, // use previously stored result. Otherwise, convert and store. Node n2; if (childToStream.find(i) != childToStream.end()) n2 = childToStream[i]; - else { + else + { n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map); childToStream[i] = n2; } - // The following branch is dedicated to handling sequences of identical equalities, + // The following branch is dedicated to handling sequences of identical + // equalities, // i.e. trans[ a=b, a=b, a=b ]. // // There are two cases: - // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality, + // 1. The number of equalities is odd. Then, the sequence can be + // collapsed to just one equality, // i.e. a=b. - // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this, - // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs - // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, + // 2. The number of equalities is even. Now, we have two options: a=a + // or b=b. To determine this, + // we look at the node after the equality sequence. If it needs a, + // we go for a=a; and if it needs + // b, we go for b=b. If there is no following node, we look at the + // goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL) { - if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { + if (n2.getKind() == kind::EQUAL) + { + if (((n1[0] == n2[0]) && (n1[1] == n2[1])) + || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) + { // We are in a sequence of identical equalities - Debug("pf::uf") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + Debug("pf::uf") << "Detected identical equalities: " << std::endl + << "\t" << n1 << std::endl; - if (!identicalEqualities) { + if (!identicalEqualities) + { // The sequence of identical equalities has started just now identicalEqualities = true; - Debug("pf::uf") << "The sequence is just beginning. Determining length..." << std::endl; + Debug("pf::uf") + << "The sequence is just beginning. Determining length..." + << std::endl; // Determine whether the length of this sequence is odd or even. evenLengthSequence = true; bool sequenceOver = false; size_t j = i + 1; - while (j < pf.d_children.size() && !sequenceOver) { + while (j < pf.d_children.size() && !sequenceOver) + { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map ); - - if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || - ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { + nodeAfterEqualitySequence = toStreamRecLFSC( + dontCare, tp, *(pf.d_children[j]), tb + 1, map); + + if (((nodeAfterEqualitySequence[0] == n1[0]) + && (nodeAfterEqualitySequence[1] == n1[1])) + || ((nodeAfterEqualitySequence[0] == n1[1]) + && (nodeAfterEqualitySequence[1] == n1[0]))) + { evenLengthSequence = !evenLengthSequence; - } else { + } + else + { sequenceOver = true; } ++j; } - if (evenLengthSequence) { - // If the length is even, we need to apply transitivity for the "correct" hand of the equality. - - Debug("pf::uf") << "Equality sequence of even length" << std::endl; - Debug("pf::uf") << "n1 is: " << n1 << std::endl; - Debug("pf::uf") << "n2 is: " << n2 << std::endl; - Debug("pf::uf") << "pf-d_node is: " << pf.d_node << std::endl; - Debug("pf::uf") << "Next node is: " << nodeAfterEqualitySequence << std::endl; - - ss << "(trans _ _ _ _ "; - - // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us. - if (!sequenceOver) { - if (match(n1[0], pf.d_node[0])) { - n1 = eqNode(n1[0], n1[0]); - ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - } else if (match(n1[1], pf.d_node[1])) { - n1 = eqNode(n1[1], n1[1]); - ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); - } else { - Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving." - << std::endl; - Assert(false); - } - } else { - // We have a "next node". Use it to guide us. - - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); - - if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { - - // Eliminate n1[1] - ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - n1 = eqNode(n1[0], n1[0]); - - } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) { - - // Eliminate n1[0] - ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); - n1 = eqNode(n1[1], n1[1]); - - } else { - Debug("pf::uf") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; - Assert(false); - } - } - - ss << ")"; - - } else { - Debug("pf::uf") << "Equality sequence length is odd!" << std::endl; - ss.str(ss1.str()); - } - - Debug("pf::uf") << "Have proven: " << n1 << std::endl; + nodePair = + tp->identicalEqualitiesPrinterHelper(evenLengthSequence, + sequenceOver, + pf, + map, + ss1.str(), + &ss, + n1, + nodeAfterEqualitySequence); + n1 = nodePair.first; + nodeAfterEqualitySequence = nodePair.second; } else { ss.str(ss1.str()); } @@ -621,6 +463,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, Debug("pf::uf") << (n1[1] == n2[0]) << "\n"; } } + ss << "(trans _ _ _ _ "; if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL) @@ -628,20 +471,20 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, { if(n1[0] == n2[0]) { if(tb == 1) { Debug("pf::uf") << "case 1\n"; } - n1 = eqNode(n1[1], n2[1]); + n1 = n1[1].eqNode(n2[1]); ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); } else if(n1[1] == n2[1]) { if(tb == 1) { Debug("pf::uf") << "case 2\n"; } - n1 = eqNode(n1[0], n2[0]); + n1 = n1[0].eqNode(n2[0]); ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")"; } else if(n1[0] == n2[1]) { if(tb == 1) { Debug("pf::uf") << "case 3\n"; } - n1 = eqNode(n2[0], n1[1]); + n1 = n2[0].eqNode(n1[1]); ss << ss2.str() << " " << ss1.str(); if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; } } else if(n1[1] == n2[0]) { if(tb == 1) { Debug("pf::uf") << "case 4\n"; } - n1 = eqNode(n1[0], n2[1]); + n1 = n1[0].eqNode(n2[1]); ss << ss1.str() << " " << ss2.str(); } else { Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; @@ -734,6 +577,7 @@ UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe) : TheoryProof(uf, pe) {} +theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; } void UFProof::registerTerm(Expr term) { // already registered if (d_declarations.find(term) != d_declarations.end()) @@ -757,8 +601,10 @@ void UFProof::registerTerm(Expr term) { if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { // Ensure cnf literals Node asNode(term); - ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true))); - ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false))); + ProofManager::currentPM()->ensureLiteral( + asNode.eqNode(NodeManager::currentNM()->mkConst(true))); + ProofManager::currentPM()->ensureLiteral( + asNode.eqNode(NodeManager::currentNM()->mkConst(false))); } } diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 7aa00cc35..a4e4cff0b 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -62,8 +62,9 @@ class UFProof : public TheoryProof { protected: TypeSet d_sorts; // all the uninterpreted sorts in this theory ExprSet d_declarations; // all the variable/function declarations + theory::TheoryId getTheoryId(); -public: + public: UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; -- 2.30.2