diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-05-12 23:05:17 -0300 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-05-12 23:05:17 -0300 |
commit | b750e7f52964457e321c9021f36d33c94d1dfed6 (patch) | |
tree | 5a3f32089bd58a64fd774e383b4f54e17d3544aa | |
parent | a9d891503c471a8b24b2c8176345b56cb36e4b80 (diff) |
formatting
-rw-r--r-- | src/theory/uf/eq_proof.cpp | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 81a426435..aec96b4f9 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -831,7 +831,7 @@ Node EqProof::addToProof( } reduceNestedCongruence(arity - 1, d_node, transtivityChildren, p, visited); if (Trace.isOn("eqproof-conv")) - { + { Trace("eqproof-conv") << "EqProof::addToProof: premises from reduced cong:\n"; for (unsigned i = 0; i < arity; ++i) @@ -843,20 +843,20 @@ Node EqProof::addToProof( // bulid transitivity steps for the arguments with transitivity proofs std::vector<Node> children(arity); for (unsigned i = 0; i < arity; ++i) - { + { Assert(!transtivityChildren[i].empty()) << "EqProof::addToProof: did not add any justification for " << i << "-th arg of congruence " << d_node << "\n"; // nothing to do if (transtivityChildren[i].size() == 1) - { + { children[i] = transtivityChildren[i][0]; continue; } cleanReflPremisesInTranstivity(transtivityChildren[i]); // if after refl elimination it has only one child, take that if (transtivityChildren[i].size() == 1) - { + { children[i] = transtivityChildren[i][0]; continue; } @@ -865,30 +865,30 @@ Node EqProof::addToProof( bool occurs = false; unsigned sizeTrans = transtivityChildren[i].size(); for (unsigned j = 0; j < sizeTrans; ++j) - { + { if (transtivityChildren[i][j] == transConclusion || (transtivityChildren[i][j][0] == transConclusion[1] && transtivityChildren[i][j][1] == transConclusion[0])) { occurs = true; - break; - } + break; + } } if (!occurs && sizeTrans > 0) { // Build transitivity step. Since premises might not be properly ordered, // process it as the transitivity premises - maybeAddSymmOrTrueIntroToProof( + maybeAddSymmOrTrueIntroToProof( 0, transtivityChildren[i], true, transConclusion[0], p); - for (unsigned j = 1; j < sizeTrans - 1; ++j) - { + for (unsigned j = 1; j < sizeTrans - 1; ++j) + { Assert(transtivityChildren[i][j - 1].getKind() == kind::EQUAL); - maybeAddSymmOrTrueIntroToProof(j, + maybeAddSymmOrTrueIntroToProof(j, transtivityChildren[i], - true, + true, transtivityChildren[i][j - 1][1], - p); - } + p); + } maybeAddSymmOrTrueIntroToProof( sizeTrans - 1, transtivityChildren[i], false, transConclusion[1], p); Trace("eqproof-conv") @@ -896,23 +896,23 @@ Node EqProof::addToProof( << transConclusion << " with children " << transtivityChildren[i] << "\n"; if (!p->addStep(transConclusion, - PfRule::TRANS, + PfRule::TRANS, transtivityChildren[i], - {}, - true, - true)) - { - Assert(false) << "EqProof::addToProof: couldn't add trans step\n"; - } - } - children[i] = transConclusion; + {}, + true, + true)) + { + Assert(false) << "EqProof::addToProof: couldn't add trans step\n"; + } } + children[i] = transConclusion; + } Trace("eqproof-conv") << "EqProof::addToProof: premises after adding trans steps:" << children << "\n"; // reorder children potentially for (unsigned i = 0; i < arity; ++i) - { + { if (children[i][0] != d_node[0][i]) { Assert(children[i][0] == d_node[1][i]) |