} // 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<theory::eq::EqProof> pf,
unsigned row,
<< "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<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()) {
- 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<std::shared_ptr<const theory::eq::EqProof>> 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<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::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);
}
out << "(clausify_false (contra _ ";
-
if (disequalityFound) {
Node n2 = pf.d_children[neg]->d_node;
Assert(n2.getKind() == kind::NOT);
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<const theory::eq::EqProof*> stk;
- for (const theory::eq::EqProof* pf2 = &pf;
- pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
- pf2 = pf2->d_children[0].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<const theory::eq::EqProof*> stk;
+ for (const theory::eq::EqProof* pf2 = &pf;
+ pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
+ pf2 = pf2->d_children[0].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());
}
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<Kind>());
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<Kind>());
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() << " ) = " <<
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;
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";
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;
- for(size_t i = 1; i < pf.d_children.size(); ++i) {
+ 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("");
- // 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());
}
}
}
- 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";
{
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";
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);
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())
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
#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"
#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;
}
}
+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);
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<theory::eq::EqProof> 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<std::shared_ptr<const theory::eq::EqProof>>
+ 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<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::" + 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<Node, Node> 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<Node&, Node&>(n, nodeAfterEqualitySequence);
+}
+
} /* namespace CVC4 */
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;
<< 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)) {
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) {
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;
}
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);
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";
//}
//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());
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());
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";
}
}
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());
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());
}
Debug("pf::uf") << (n1[1] == n2[0]) << "\n";
}
}
+
ss << "(trans _ _ _ _ ";
if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL)
{
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";
: 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())
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)));
}
}
projects / cvc5.git / commitdiff