From: Haniel Barbosa Date: Wed, 16 Sep 2020 03:30:49 +0000 (-0300) Subject: [proof-new] Extending eqproof conversion to HO congruence (#5071) X-Git-Tag: cvc5-1.0.0~2856 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85a3056bed70e226d9e17a1f5785d957628f9e26;p=cvc5.git [proof-new] Extending eqproof conversion to HO congruence (#5071) --- diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index d7b615ffa..8b1e05fb0 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -16,6 +16,7 @@ #include "theory/uf/eq_proof.h" #include "expr/proof.h" +#include "options/uf_options.h" namespace CVC4 { namespace theory { @@ -700,9 +701,10 @@ void EqProof::reduceNestedCongruence( << transitivityMatrix[i].back() << "\n"; // if i == 0, first child must be REFL step, standing for (= f f), which can // be ignored in a first-order calculus - Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY); + Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY + || options::ufHo()); // recurse - if (i > 0) + if (i > 1) { Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce first child\n" @@ -716,9 +718,21 @@ void EqProof::reduceNestedCongruence( isNary); Trace("eqproof-conv") << pop; } + // higher-order case + else if (d_children[0]->d_id != MERGED_THROUGH_REFLEXIVITY) + { + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. " + "Processing first child\n"; + // we only handle these cases + Assert(d_children[0]->d_id == MERGED_THROUGH_EQUALITY + || d_children[0]->d_id == MERGED_THROUGH_TRANS); + transitivityMatrix[0].push_back( + d_children[0]->addToProof(p, visited, assumptions)); + } return; } - Assert(d_id == MERGED_THROUGH_TRANS); + Assert(d_id == MERGED_THROUGH_TRANS) + << "id is " << static_cast(d_id) << "\n"; Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a " "transitivity step.\n"; Assert(d_node.isNull() @@ -1186,23 +1200,24 @@ Node EqProof::addToProof( // example). if (d_node[0].getNumChildren() != d_node[1].getNumChildren()) { - Assert(isNary); + Assert(isNary) << "We only handle congruences of apps with different " + "number of children for theory n-ary operators"; arity = d_node[1].getNumChildren() < arity ? arity : d_node[1].getNumChildren(); Trace("eqproof-conv") << "EqProof::addToProof: Mismatching arities in cong conclusion " << d_node << ". Use tentative arity " << arity << "\n"; } - // For a congruence proof of (= (f a0 ... an-1) (f b0 ... bn-1)), build a - // transitivity matrix where each row contains a transitivity chain justifying - // (= ai bi) + // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a + // transitivity matrix of n rows where the first row contains a transitivity + // chain justifying (= f g) and the next rows (= ai bi) std::vector> transitivityChildren; - for (unsigned i = 0; i < arity; ++i) + for (unsigned i = 0; i < arity + 1; ++i) { transitivityChildren.push_back(std::vector()); } reduceNestedCongruence( - arity - 1, d_node, transitivityChildren, p, visited, assumptions, isNary); + arity, d_node, transitivityChildren, p, visited, assumptions, isNary); // Congruences over n-ary operators may require changing the conclusion (as in // the above example). This is handled in a general manner below according to // whether the transitivity matrix computed by reduceNestedCongruence contains @@ -1212,7 +1227,7 @@ Node EqProof::addToProof( if (isNary) { unsigned emptyRows = 0; - for (unsigned i = 0; i < arity; ++i) + for (unsigned i = 1; i <= arity; ++i) { if (transitivityChildren[i].empty()) { @@ -1232,7 +1247,11 @@ Node EqProof::addToProof( // n - k1 == m - k2 // Note that by construction the equality between the first emptyRows + 1 // arguments of each application is justified by the transitivity step in - // the row emptyRows +1 in the matrix. + // the row emptyRows + 1 in the matrix. + // + // All of the above is with the very first row in the matrix, reserved for + // justifying the equality between the functions, which is not necessary in + // the n-ary case, notwithstanding. if (emptyRows > 0) { Trace("eqproof-conv") @@ -1242,9 +1261,11 @@ Node EqProof::addToProof( // beginning are eliminated, as the new arity is the maximal arity among // the applications minus the number of empty rows. std::vector> newTransitivityChildren{ - transitivityChildren.begin() + emptyRows, transitivityChildren.end()}; + transitivityChildren.begin() + 1 + emptyRows, + transitivityChildren.end()}; transitivityChildren.clear(); - transitivityChildren.insert(transitivityChildren.begin(), + transitivityChildren.push_back(std::vector()); + transitivityChildren.insert(transitivityChildren.end(), newTransitivityChildren.begin(), newTransitivityChildren.end()); unsigned arityPrefix1 = @@ -1293,27 +1314,40 @@ Node EqProof::addToProof( Trace("eqproof-conv") << "EqProof::addToProof: premises from reduced cong of " << conclusion << ":\n"; - for (unsigned i = 0; i < arity; ++i) + for (unsigned i = 0; i <= arity; ++i) { Trace("eqproof-conv") << "EqProof::addToProof:\t" << i << "-th arg: " << transitivityChildren[i] << "\n"; } } + std::vector children(arity + 1); + // Check if there is a justification for equality between functions (HO case) + if (!transitivityChildren[0].empty()) + { + Assert(k == kind::APPLY_UF) << "Congruence with different functions only " + "allowed for uninterpreted functions.\n"; + + children[0] = + conclusion[0].getOperator().eqNode(conclusion[1].getOperator()); + Assert(transitivityChildren[0].size() == 1 + && CDProof::isSame(children[0], transitivityChildren[0][0])) + << "Justification of operators equality is wrong: " + << transitivityChildren[0] << "\n"; + } // Proccess transitivity matrix to (possibly) generate transitivity steps for // congruence premises (= ai bi) - std::vector children(arity); - for (unsigned i = 0; i < arity; ++i) + for (unsigned i = 1; i <= arity; ++i) { - Node transConclusion = conclusion[0][i].eqNode(conclusion[1][i]); + Node transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]); children[i] = transConclusion; Assert(!transitivityChildren[i].empty()) << "EqProof::addToProof: did not add any justification for " << i << "-th arg of congruence " << conclusion << "\n"; // If the transitivity conclusion is a reflexivity step, just add it. Note - // that this can happen with with transitivityChildren containing several - // equalities in the case of (= ai bi) being the same n-ary application that - // was justified by a congruence step, which can happen in the current - // equality engine + // that this can happen even with the respective transitivityChildren row + // containing several equalities in the case of (= ai bi) being the same + // n-ary application that was justified by a congruence step, which can + // happen in the current equality engine. if (transConclusion[0] == transConclusion[1]) { p->addStep(transConclusion, PfRule::REFL, {}, {transConclusion[0]}); @@ -1355,18 +1389,34 @@ Node EqProof::addToProof( transConclusion, PfRule::TRANS, transitivityChildren[i], {}, true); } } - // Get node of the function operator over which congruence is being applied. - std::vector args; - args.push_back(ProofRuleChecker::mkKindNode(k)); - if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) + // first-order case + if (children[0].isNull()) + { + // remove placehold for function equality case + children.erase(children.begin()); + // Get node of the function operator over which congruence is being + // applied. + std::vector args; + args.push_back(ProofRuleChecker::mkKindNode(k)); + if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) + { + args.push_back(conclusion[0].getOperator()); + } + // Add congruence step + Trace("eqproof-conv") << "EqProof::addToProof: build cong step of " + << conclusion << " with op " << args[0] + << " and children " << children << "\n"; + p->addStep(conclusion, PfRule::CONG, children, args, true); + } + // higher-order case + else { - args.push_back(conclusion[0].getOperator()); + // Add congruence step + Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of " + << conclusion << " with children " << children + << "\n"; + p->addStep(conclusion, PfRule::HO_CONG, children, {}, true); } - // Add congruence step - Trace("eqproof-conv") << "EqProof::addToProof: build cong step of " - << conclusion << " with op " << args[0] - << " and children " << children << "\n"; - p->addStep(conclusion, PfRule::CONG, children, args, true); // If the conclusion of the congruence step changed due to the n-ary handling, // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via