diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-25 15:12:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-25 15:12:51 -0700 |
commit | 1ae10032fb99ca1d8f73c5f51dce3cfc976b3dfb (patch) | |
tree | 9006c24edf5605145167cea0ce1d5df829bcac57 /src/proof/uf_proof.cpp | |
parent | 8cc4bc292c6ac60edfa356355ad235e51ad15310 (diff) |
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.
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 364 |
1 files changed, 105 insertions, 259 deletions
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<theory::eq::EqProof> subTrans = std::make_shared<theory::eq::EqProof>(); - 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<std::shared_ptr<const theory::eq::EqProof>> 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<std::shared_ptr<theory::eq::EqProof>> 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<size_t, Node> childToStream; - + std::stringstream ss1(ss.str()), ss2; + std::pair<Node, Node> 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))); } } |