#include "theory/uf/eq_proof.h"
#include "expr/proof.h"
+#include "options/uf_options.h"
namespace CVC4 {
namespace theory {
<< 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"
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<MergeReasonType>(d_id) << "\n";
Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
"transitivity step.\n";
Assert(d_node.isNull()
// 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<std::vector<Node>> transitivityChildren;
- for (unsigned i = 0; i < arity; ++i)
+ for (unsigned i = 0; i < arity + 1; ++i)
{
transitivityChildren.push_back(std::vector<Node>());
}
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
if (isNary)
{
unsigned emptyRows = 0;
- for (unsigned i = 0; i < arity; ++i)
+ for (unsigned i = 1; i <= arity; ++i)
{
if (transitivityChildren[i].empty())
{
// 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")
// beginning are eliminated, as the new arity is the maximal arity among
// the applications minus the number of empty rows.
std::vector<std::vector<Node>> newTransitivityChildren{
- transitivityChildren.begin() + emptyRows, transitivityChildren.end()};
+ transitivityChildren.begin() + 1 + emptyRows,
+ transitivityChildren.end()};
transitivityChildren.clear();
- transitivityChildren.insert(transitivityChildren.begin(),
+ transitivityChildren.push_back(std::vector<Node>());
+ transitivityChildren.insert(transitivityChildren.end(),
newTransitivityChildren.begin(),
newTransitivityChildren.end());
unsigned arityPrefix1 =
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<Node> 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<Node> 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]});
transConclusion, PfRule::TRANS, transitivityChildren[i], {}, true);
}
}
- // Get node of the function operator over which congruence is being applied.
- std::vector<Node> 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<Node> 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
projects / cvc5.git / commitdiff