diff options
| -rw-r--r-- | src/theory/uf/eq_proof.cpp | 83 |
1 files changed, 55 insertions, 28 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index c7a834b19..15979bd44 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -480,7 +480,7 @@ bool EqProof::expandTransitivityForDisequalities( p->addStep(congConclusion, PfRule::CONG, substPremises, - {nm->operatorOf(kind::EQUAL)}, + {ProofRuleChecker::mkKindNode(kind::EQUAL)}, true); Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via " "congruence derived " @@ -892,25 +892,22 @@ Node EqProof::addToProof( // Equalities due to theory reasoning if (d_id == MERGED_THROUGH_CONSTANTS) { - // Currently only supports case of negative merged throgh constants Assert(!d_node.isNull() && d_node.getKind() == kind::EQUAL - && d_node[0].getKind() == kind::EQUAL - && d_node[1].getKind() == kind::CONST_BOOLEAN - && !d_node[1].getConst<bool>()) + && d_node[1].isConst()) << ". Conclusion " << d_node << " from " << static_cast<MergeReasonType>(d_id) - << " was expected to be (= (= t1 t2) false)\n"; + << " was expected to be (= (f t1 ... tn) c)\n"; Assert(!assumptions.count(d_node)) << "Conclusion " << d_node << " from " << static_cast<MergeReasonType>(d_id) << " is an assumption\n"; // The step has the form - // [(= t1 c1)] [(= t2 c2)] + // [(= t1 c1)] ... [(= tn cn)] // ------------------------ - // (= (= t1 t2) false) - // where premises equating t1/t2 to constants are present when they are not + // (= (f t1 ... tn) c) + // where premises equating ti to constants are present when they are not // already constants. Note that the premises may be in any order, e.g. with // the equality for the second term being justified in the first premise. - // Moreover, they may be of the form (= c t). + // Moreover, they may be of the form (= ci ti). // // First recursively process premises, if any std::vector<Node> premises; @@ -922,21 +919,32 @@ Node EqProof::addToProof( premises.push_back(d_children[i]->addToProof(p, visited, assumptions)); Trace("eqproof-conv") << pop; } - // A step - // [(= t1 c1)] [(= t2 c2)] - // ------------------------ MACRO_SR_PRED_INTRO - // (= (= t1 t2) false) - // is gonna be built, with the premises is the correct order. - std::vector<Node> children; - for (unsigned i = 0; i < 2; ++i) + // After building the proper premises we could build a step like + // [(= t1 c1)] ... [(= tn cn)] + // ---------------------------- MACRO_SR_PRED_INTRO + // (= (f t1 ... tn) c) + // but note that since the substitution applied by MACRO_SR_PRED_INTRO is + // *not* simultenous this could lead to issues if t_{i+1} occurred in some + // t_{i}. So we build proofs as + // + // [(= t1 c1)] ... [(= tn cn)] + // ------------------------------- CONG -------------- MACRO_SR_PRED_INTRO + // (= (f t1 ... tn) (f c1 ... cn)) (= (f c1 ... cn) c) + // ---------------------------------------------------------- TRANS + // (= (f t1 ... tn) c) + std::vector<Node> subChildren, constChildren; + for (unsigned i = 0, size = d_node[0].getNumChildren(); i < size; ++i) { Node term = d_node[0][i]; - // term already is a constant, no need to add a premise to it + // term already is a constant, add a REFL step if (term.isConst()) { + subChildren.push_back(term.eqNode(term)); + p->addStep(subChildren.back(), PfRule::REFL, {}, {term}); + constChildren.push_back(term); continue; } - // Build the equality (= t c) as a premise, finding the respective c is + // Build the equality (= ti ci) as a premise, finding the respective ci is // the original premises Node constant; for (const Node& premise : premises) @@ -946,19 +954,41 @@ Node EqProof::addToProof( { Assert(premise[1].isConst()); constant = premise[1]; + break; } - else if (premise[1] == term) + if (premise[1] == term) { Assert(premise[0].isConst()); constant = premise[0]; + break; } } - children.push_back(term.eqNode(constant)); + Assert(!constant.isNull()); + subChildren.push_back(term.eqNode(constant)); + constChildren.push_back(constant); } + // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c) + Kind k = d_node[0].getKind(); + Node constApp = NodeManager::currentNM()->mkNode(k, constChildren); + Node constEquality = constApp.eqNode(d_node[1]); Trace("eqproof-conv") << "EqProof::addToProof: adding " - << PfRule::MACRO_SR_PRED_INTRO << " step from " - << children << "\n"; - p->addStep(d_node, PfRule::MACRO_SR_PRED_INTRO, children, {d_node}); + << PfRule::MACRO_SR_PRED_INTRO << " step for " + << constApp << " = " << d_node[1] << "\n"; + p->addStep(constEquality, PfRule::MACRO_SR_PRED_INTRO, {}, {constEquality}); + // build congruence conclusion (= (f t1 ... tn) (f c1 ... cn)) + Node congConclusion = d_node[0].eqNode(constApp); + Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG + << " step for " << congConclusion << " from " + << subChildren << "\n"; + p->addStep(congConclusion, + PfRule::CONG, + {subChildren}, + {ProofRuleChecker::mkKindNode(k)}, + true); + Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS + << " step for original conclusion " << d_node << "\n"; + std::vector<Node> transitivityChildren{congConclusion, constEquality}; + p->addStep(d_node, PfRule::TRANS, {transitivityChildren}, {}); visited[d_node] = d_node; return d_node; } @@ -1253,14 +1283,11 @@ Node EqProof::addToProof( } // 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()); } - else - { - args.push_back(nm->operatorOf(k)); - } // Add congruence step Trace("eqproof-conv") << "EqProof::addToProof: build cong step of " << conclusion << " with op " << args[0] |