From: Haniel Barbosa Date: Thu, 16 Jul 2020 21:52:15 +0000 (-0300) Subject: (proof-new) Implements the conversion between EqProof and ProofNode (#4756) X-Git-Tag: cvc5-1.0.0~3096 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70353e7a7bdb5863edda8f2cabf6807d8f084525;p=cvc5.git (proof-new) Implements the conversion between EqProof and ProofNode (#4756) --- diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 3a60d246e..70edbd0dd 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -86,7 +86,31 @@ void EqProof::debug_print(std::ostream& os, os << ")" << std::endl; } -void EqProof::cleanReflPremises(std::vector& premises) const {} +void EqProof::cleanReflPremises(std::vector& premises) const +{ + std::vector newPremises; + unsigned size = premises.size(); + for (unsigned i = 0; i < size; ++i) + { + if (premises[i][0] == premises[i][1]) + { + continue; + } + newPremises.push_back(premises[i]); + } + if (newPremises.size() != size) + { + Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed " + << (newPremises.size() >= size + ? newPremises.size() - size + : 0) + << " refl premises from " << premises << "\n"; + premises.clear(); + premises.insert(premises.end(), newPremises.begin(), newPremises.end()); + Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises " + << premises << "\n"; + } +} bool EqProof::expandTransitivityForDisequalities( Node conclusion, @@ -94,12 +118,492 @@ bool EqProof::expandTransitivityForDisequalities( CDProof* p, std::unordered_set& assumptions) const { - return false; + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: check if need " + "to expand transitivity step to conclude " + << conclusion << " from premises " << premises << "\n"; + // Check premises to see if any of the form (= (= t1 t2) false), modulo + // symmetry + unsigned size = premises.size(); + // termPos is, in (= (= t1 t2) false) or (= false (= t1 t2)), the position of + // the equality. When the i-th premise has that form, offending = i + unsigned termPos = 2, offending = size; + for (unsigned i = 0; i < size; ++i) + { + Assert(premises[i].getKind() == kind::EQUAL); + for (unsigned j = 0; j < 2; ++j) + { + if (premises[i][j].getKind() == kind::CONST_BOOLEAN + && !premises[i][j].getConst() + && premises[i][1 - j].getKind() == kind::EQUAL) + { + // there is only one offending equality + Assert(offending == size); + offending = i; + termPos = 1 - j; + break; + } + } + } + // if no equality of the searched form, nothing to do + if (offending == size) + { + return false; + } + NodeManager* nm = NodeManager::currentNM(); + Assert(termPos == 0 || termPos == 1); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found " + "offending equality at index " + << offending << " : " << premises[offending] << "\n"; + // collect the premises to be used in the expansion, which are all but the + // offending one + std::vector expansionPremises; + for (unsigned i = 0; i < size; ++i) + { + if (i != offending) + { + expansionPremises.push_back(premises[i]); + } + } + // Eliminate spurious premises. Reasoning below assumes no refl steps. + cleanReflPremises(expansionPremises); + Assert(!expansionPremises.empty()); + // Check if we are in the substitution case + Node expansionConclusion; + std::vector substPremises; + bool inSubstCase = false, substConclusionInReverseOrder = false; + if ((conclusion[0].getKind() == kind::CONST_BOOLEAN) + != (conclusion[1].getKind() == kind::CONST_BOOLEAN)) + { + inSubstCase = true; + // reorder offending premise if constant is the first argument + if (termPos == 1) + { + premises[offending] = + premises[offending][1].eqNode(premises[offending][0]); + } + // reorder conclusion if constant is the first argument + conclusion = conclusion[1].getKind() == kind::CONST_BOOLEAN + ? conclusion + : conclusion[1].eqNode(conclusion[0]); + // equality term in premise disequality + Node premiseTermEq = premises[offending][0]; + // equality term in conclusion disequality + Node conclusionTermEq = conclusion[0]; + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: Substitition " + "case. Need to build subst from " + << premiseTermEq << " to " << conclusionTermEq << "\n"; + // If only one argument in the premise is substituted, premiseTermEq and + // conclusionTermEq will share one argument and the other argument change + // defines the single substitution. Otherwise both arguments are replaced, + // so there are two substitutions. + std::vector subs[2]; + subs[0].push_back(premiseTermEq[0]); + subs[1].push_back(premiseTermEq[1]); + // which of the arguments of premiseTermEq, if any, is equal to one argument + // of conclusionTermEq + int equalArg = -1; + for (unsigned i = 0; i < 2; ++i) + { + for (unsigned j = 0; j < 2; ++j) + { + if (premiseTermEq[i] == conclusionTermEq[j]) + { + equalArg = i; + // identity sub + subs[i].push_back(conclusionTermEq[j]); + // sub that changes argument + subs[1 - i].push_back(conclusionTermEq[1 - j]); + // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3) + substConclusionInReverseOrder = i != j; + break; + } + } + } + // simple case of single substitution + if (equalArg >= 0) + { + // case of + // (= (= t1 t2) false) (= t1 x1) ... (= xn t3) + // -------------------------------------------- EQP::TR + // (= (= t3 t2) false) + // where + // + // (= t1 x1) ... (= xn t3) - expansion premises + // ------------------------ TRANS + // (= t1 t3) - expansion conclusion + // + // will be the expansion made to justify the substitution for t1->t3. + expansionConclusion = subs[1 - equalArg][0].eqNode(subs[1 - equalArg][1]); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: " + "Need to expand premises into " + << expansionConclusion << "\n"; + // add refl step for the substitition t2->t2 + p->addStep(subs[equalArg][0].eqNode(subs[equalArg][1]), + PfRule::REFL, + {}, + {subs[equalArg][0]}); + } + else + { + // Hard case. We determine, and justify, the substitutions t1->t3/t4 and + // t2->t3/t4 based on the expansion premises. + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: " + "Need two substitutions. Look for " + << premiseTermEq[0] << " and " << premiseTermEq[1] + << " in premises " << expansionPremises << "\n"; + Assert(expansionPremises.size() >= 2) + << "Less than 2 expansion premises for substituting BOTH terms in " + "disequality.\nDisequality: " + << premises[offending] + << "\nExpansion premises: " << expansionPremises + << "\nConclusion: " << conclusion << "\n"; + // Easier case where we can determine the substitutions by directly + // looking at the premises, i.e. the two expansion premises are for + // example (= t1 t3) and (= t2 t4) + if (expansionPremises.size() == 2) + { + // iterate over args to be substituted + for (unsigned i = 0; i < 2; ++i) + { + // iterate over premises + for (unsigned j = 0; j < 2; ++j) + { + // iterate over args in premise + for (unsigned k = 0; k < 2; ++k) + { + if (premiseTermEq[i] == expansionPremises[j][k]) + { + subs[i].push_back(expansionPremises[j][1 - k]); + break; + } + } + } + Assert(subs[i].size() == 2) + << " did not find term " << subs[i][0] << "\n"; + // check if argument to be substituted is in the same order in the + // conclusion + substConclusionInReverseOrder = + premiseTermEq[i] != conclusionTermEq[i]; + } + } + else + { + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: " + "Build transitivity chains " + "for two subs among more than 2 premises: " + << expansionPremises << "\n"; + // Hardest case. Try building a transitivity chain for (= t1 t3). If it + // can be built, use the remaining expansion premises to build a chain + // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for + // (= t2 t3). It should always succeed. + subs[0].push_back(conclusionTermEq[0]); + subs[1].push_back(conclusionTermEq[1]); + for (unsigned i = 0; i < 2; ++i) + { + // copy premises, since buildTransitivityChain is destructive + std::vector copy1ofExpPremises(expansionPremises.begin(), + expansionPremises.end()); + Node transConclusion1 = subs[0][0].eqNode(subs[0][1]); + if (!buildTransitivityChain(transConclusion1, copy1ofExpPremises)) + { + AlwaysAssert(i == 0) + << "Couldn't find sub at all for substituting BOTH terms in " + "disequality.\nDisequality: " + << premises[offending] + << "\nExpansion premises: " << expansionPremises + << "\nConclusion: " << conclusion << "\n"; + // Failed. So flip sub and try again + subs[0][1] = conclusionTermEq[1]; + subs[1][1] = conclusionTermEq[0]; + substConclusionInReverseOrder = false; + continue; + } + // build next chain + std::vector copy2ofExpPremises(expansionPremises.begin(), + expansionPremises.end()); + Node transConclusion2 = subs[1][0].eqNode(subs[1][1]); + if (!buildTransitivityChain(transConclusion2, copy2ofExpPremises)) + { + Unreachable() << "Found sub " << transConclusion1 + << " but not other sub " << transConclusion2 + << ".\nDisequality: " << premises[offending] + << "\nExpansion premises: " << expansionPremises + << "\nConclusion: " << conclusion << "\n"; + } + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: Built trans " + "chains: " + "for two subs among more than 2 premises:\n"; + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: " + << transConclusion1 << " <- " << copy1ofExpPremises << "\n"; + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: " + << transConclusion2 << " <- " << copy2ofExpPremises << "\n"; + // do transitivity steps if need be to justify each substitution + if (copy1ofExpPremises.size() > 1 + && !assumptions.count(transConclusion1)) + { + p->addStep( + transConclusion1, PfRule::TRANS, copy1ofExpPremises, {}, true); + } + if (copy2ofExpPremises.size() > 1 + && !assumptions.count(transConclusion2)) + { + p->addStep( + transConclusion2, PfRule::TRANS, copy2ofExpPremises, {}, true); + } + } + } + } + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: Built substutitions " + << subs[0] << " and " << subs[1] << " to map " << premiseTermEq + << " -> " << conclusionTermEq << "\n"; + Assert(subs[0][1] == conclusion[0][0] || subs[0][1] == conclusion[0][1]) + << "EqProof::expandTransitivityForDisequalities: First substitution " + << subs[0] << " doest not map to conclusion " << conclusion << "\n"; + Assert(subs[1][1] == conclusion[0][0] || subs[1][1] == conclusion[0][1]) + << "EqProof::expandTransitivityForDisequalities: Second substitution " + << subs[1] << " doest not map to conclusion " << conclusion << "\n"; + // In the premises for the original conclusion, the substitution of + // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored + // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with + // the disequality is built as as + // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false) + // --------------------------------------------------------------------- TR + // (= (= t3 t4) false) + substPremises.push_back(subs[0][1].eqNode(subs[0][0])); + substPremises.push_back(subs[1][1].eqNode(subs[1][0])); + } + else + { + // In simple case the conclusion is always, modulo symmetry, false = true + Assert(conclusion[0].getKind() == kind::CONST_BOOLEAN + && conclusion[1].getKind() == kind::CONST_BOOLEAN); + // The expansion conclusion is the same as the equality term in the + // disequality, which is going to be justified by a transitivity step from + // the expansion premises + expansionConclusion = premises[offending][termPos]; + } + // Unless we are in the double-substitution case, the proof has the shape + // + // ... ... ... ... - expansionPremises + // ------------------ TRANS + // (= (= (t t') false) (= t'' t''') - expansionConclusion + // ---------------------------------------------- TRANS or PRED_TRANSFORM + // conclusion + // + // although note that if it's a TRANS step, (= t'' t''') will be turned into a + // predicate equality and the premises are ordered. + // + // We build the transitivity step for the expansionConclusion here. It being + // non-null marks that we are not in the double-substitution case. + if (!expansionConclusion.isNull()) + { + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: need to derive " + << expansionConclusion << " with premises " << expansionPremises + << "\n"; + Assert(expansionPremises.size() > 1 + || expansionConclusion == expansionPremises.back() + || (expansionConclusion[0] == expansionPremises.back()[1] + && expansionConclusion[1] == expansionPremises.back()[0])) + << "single expansion premise " << expansionPremises.back() + << " is not the same as expansionConclusion " << expansionConclusion + << " and not its symmetric\n"; + // We track assumptions to avoid cyclic proofs, which can happen in EqProofs + // such as: + // + // (= l1 "") (= "" t) + // ----------------------- EQP::TR + // (= l1 "") (= l1 t) (= (= "" t) false) + // ----------------------------------------------------------------- EQP::TR + // (= false true) + // + // which would lead to the cyclic expansion proof: + // + // (= l1 "") (= l1 "") (= "" t) + // --------- SYMM ----------------------- TRANS + // (= "" l1) (= l1 t) + // ------------------------------------------ TRANS + // (= "" t) + if (expansionPremises.size() > 1 && !assumptions.count(expansionConclusion)) + { + // create transitivity step to derive expected premise + buildTransitivityChain(expansionConclusion, expansionPremises); + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: add transitivity " + "step for " + << expansionConclusion << " with premises " << expansionPremises + << "\n"; + // create expansion step + p->addStep( + expansionConclusion, PfRule::TRANS, expansionPremises, {}, true); + } + } + Trace("eqproof-conv") + << "EqProof::expandTransitivityForDisequalities: now derive conclusion " + << conclusion; + premises.clear(); + premises.push_back(premises[offending]); + if (inSubstCase) + { + Trace("eqproof-conv") << (substConclusionInReverseOrder ? " [inverted]" + : "") + << " via subsitution from " << premises[offending] + << " and (inverted subst) " << substPremises << "\n"; + // By this point, for premise disequality (= (= t1 t2) false), we have + // potentially already built + // + // (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4) + // ------------------------ TR ------------------------ TR + // (= t1 t3) (= t2 t4) + // + // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3 + // or t2=4, the step will actually be a REFL one). Not do + // + // ----------- SYMM ----------- SYMM + // (= t3 t1) (= t4 t2) + // ---------------------------------------- CONG + // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false) + // --------------------------------------------------------------------- TR + // (= (= t3 t4) false) + // + // where note that the SYMM steps are implicitly added by CDProof. + Node congConclusion = nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::EQUAL, substPremises[0][0], substPremises[1][0]), + premises[offending][0]); + p->addStep(congConclusion, + PfRule::CONG, + substPremises, + {nm->operatorOf(kind::EQUAL)}, + true); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via " + "congruence derived " + << congConclusion << "\n"; + // transitivity step between that and the original premise + premises.insert(premises.begin(), congConclusion); + Node transConclusion = + !substConclusionInReverseOrder + ? conclusion + : nm->mkNode(kind::EQUAL, congConclusion[0], conclusion[1]); + // check to avoid cyclic proofs + if (!assumptions.count(transConclusion)) + { + p->addStep(transConclusion, PfRule::TRANS, premises, {}, true); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: " + "via transitivity derived " + << transConclusion << "\n"; + } + // if order is reversed, finish the proof of conclusion with + // (= (= t3 t4) false) + // --------------------- MACRO_SR_PRED_TRANSFORM + // (= (= t4 t3) false) + if (substConclusionInReverseOrder) + { + p->addStep(conclusion, + PfRule::MACRO_SR_PRED_TRANSFORM, + {transConclusion}, + {conclusion}, + true); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: " + "via macro transform derived " + << conclusion << "\n"; + } + } + else + { + // create TRUE_INTRO step for expansionConclusion and add it to the premises + Trace("eqproof-conv") + << " via transitivity.\nEqProof::expandTransitivityForDisequalities: " + "adding " + << PfRule::TRUE_INTRO << " step for " << expansionConclusion[0] << "\n"; + Node newExpansionConclusion = + expansionConclusion.eqNode(nm->mkConst(true)); + p->addStep( + newExpansionConclusion, PfRule::TRUE_INTRO, {expansionConclusion}, {}); + premises.push_back(newExpansionConclusion); + Trace("eqproof-conv") << PfRule::TRANS << " from " << premises << "\n"; + buildTransitivityChain(conclusion, premises); + // create final transitivity step + p->addStep(conclusion, PfRule::TRANS, premises, {}, true); + } + return true; } bool EqProof::buildTransitivityChain(Node conclusion, std::vector& premises) const { + Trace("eqproof-conv") << push + << "EqProof::buildTransitivityChain: Build chain for " + << conclusion << " with premises " << premises << "\n"; + for (unsigned i = 0, size = premises.size(); i < size; ++i) + { + bool occurs = false, correctlyOrdered = false; + if (conclusion[0] == premises[i][0]) + { + occurs = correctlyOrdered = true; + } + else if (conclusion[0] == premises[i][1]) + { + occurs = true; + } + if (occurs) + { + Trace("eqproof-conv") + << "EqProof::buildTransitivityChain: found " << conclusion[0] << " in" + << (correctlyOrdered ? "" : " non-") << " ordered premise " + << premises[i] << "\n"; + if (conclusion[1] == premises[i][correctlyOrdered ? 1 : 0]) + { + Trace("eqproof-conv") + << "EqProof::buildTransitivityChain: found " << conclusion[1] + << " in same premise. Closed chain.\n" + << pop; + premises.clear(); + premises.push_back(conclusion); + return true; + } + // Build chain with remaining equalities + std::vector recursivePremises; + for (unsigned j = 0; j < size; ++j) + { + if (j != i) + { + recursivePremises.push_back(premises[j]); + } + } + Node newTarget = + premises[i][correctlyOrdered ? 1 : 0].eqNode(conclusion[1]); + Trace("eqproof-conv") + << "EqProof::buildTransitivityChain: search recursively for " + << newTarget << "\n"; + if (buildTransitivityChain(newTarget, recursivePremises)) + { + Trace("eqproof-conv") + << "EqProof::buildTransitivityChain: closed chain with " + << 1 + recursivePremises.size() << " of the original " + << premises.size() << " premises\n" + << pop; + premises.clear(); + premises.insert(premises.begin(), + correctlyOrdered + ? premises[i] + : premises[i][1].eqNode(premises[i][0])); + premises.insert( + premises.end(), recursivePremises.begin(), recursivePremises.end()); + return true; + } + } + } + Trace("eqproof-conv") + << "EqProof::buildTransitivityChain: Could not build chain for" + << conclusion << " with premises " << premises << "\n"; + Trace("eqproof-conv") << pop; return false; } @@ -112,16 +616,673 @@ void EqProof::reduceNestedCongruence( std::unordered_set& assumptions, bool isNary) const { + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i + << "-th arg\n"; + if (d_id == MERGED_THROUGH_CONGRUENCE) + { + Assert(d_children.size() == 2); + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a " + "congruence step. Reduce second child\n" + << push; + transitivityMatrix[i].push_back( + d_children[1]->addToProof(p, visited, assumptions)); + Trace("eqproof-conv") + << pop << "EqProof::reduceNestedCongruence: child conclusion " + << 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); + // recurse + if (i > 0) + { + Trace("eqproof-conv") + << "EqProof::reduceNestedCongruence: Reduce first child\n" + << push; + d_children[0]->reduceNestedCongruence(i - 1, + conclusion, + transitivityMatrix, + p, + visited, + assumptions, + isNary); + Trace("eqproof-conv") << pop; + } + return; + } + Assert(d_id == MERGED_THROUGH_TRANS); + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a " + "transitivity step.\n"; + Assert(d_node.isNull() + || d_node[0].getNumChildren() == d_node[1].getNumChildren() || isNary) + << "Non-null (internal cong) transitivity conclusion of different arity " + "but not marked by isNary flag\n"; + // If handling n-ary kinds and got a transitivity conclusion, we process it + // with addToProof, store the result into row i, and stop. This marks an + // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining + // the adjustment in addToProof processing the congruence of the original + // conclusion. See details there. + if (isNary && !d_node.isNull()) + { + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, " + "break recursion and indepedently process " + << d_node << "\n" + << push; + transitivityMatrix[i].push_back(addToProof(p, visited, assumptions)); + Trace("eqproof-conv") << pop + << "EqProof::reduceNestedCongruence: Got conclusion " + << transitivityMatrix[i].back() + << " from n-ary transitivity processing\n"; + return; + } + // Regular recursive processing of each transitivity premise + for (unsigned j = 0, sizeTrans = d_children.size(); j < sizeTrans; ++j) + { + if (d_children[j]->d_id == MERGED_THROUGH_CONGRUENCE) + { + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j + << "-th transitivity congruence child\n" + << push; + d_children[j]->reduceNestedCongruence( + i, conclusion, transitivityMatrix, p, visited, assumptions, isNary); + Trace("eqproof-conv") << pop; + } + else + { + Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j + << "-th transitivity child to proof\n" + << push; + transitivityMatrix[i].push_back( + d_children[j]->addToProof(p, visited, assumptions)); + Trace("eqproof-conv") << pop; + } + } } -Node EqProof::addToProof(CDProof* p) const { return Node::null(); } +Node EqProof::addToProof(CDProof* p) const +{ + std::unordered_map cache; + std::unordered_set assumptions; + Node conclusion = addToProof(p, cache, assumptions); + Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion + << "\n"; + Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: " + << assumptions << "\n"; + // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in + // which t is not true/false, it must be turned into t or (not t) with + // TRUE/FALSE_ELIM. + Node newConclusion = conclusion; + Assert(conclusion.getKind() == kind::EQUAL); + if ((conclusion[0].getKind() == kind::CONST_BOOLEAN) + != (conclusion[1].getKind() == kind::CONST_BOOLEAN)) + { + Trace("eqproof-conv") + << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n"; + // Index of constant in equality + unsigned constIndex = + conclusion[0].getKind() == kind::CONST_BOOLEAN ? 0 : 1; + // The premise for the elimination rule must have the constant as the second + // argument of the equality. If that's not the case, build it as such, + // relying on an implicit SYMM step to be added to the proof when justifying + // t / (not t). + Node elimPremise = + constIndex == 1 ? conclusion : conclusion[1].eqNode(conclusion[0]); + // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant + // value. The new conclusion, whether t or (not t), is also determined + // accordingly. + PfRule elimRule; + if (conclusion[constIndex].getConst()) + { + elimRule = PfRule::TRUE_ELIM; + newConclusion = conclusion[1 - constIndex]; + } + else + { + elimRule = PfRule::FALSE_ELIM; + newConclusion = conclusion[1 - constIndex].notNode(); + } + // We also check if the final conclusion t / (not t) has already been + // justified, so that we can avoid a cyclic proof, which can be due to + // either t / (not t) being assumption in the original EqProof or it having + // a non-assumption proof step in the proof of (= t true/false). + if (!assumptions.count(newConclusion) && !p->hasStep(newConclusion)) + { + Trace("eqproof-conv") + << "EqProof::addToProof: conclude " << newConclusion << " via " + << elimRule << " step for " << elimPremise << "\n"; + p->addStep(newConclusion, elimRule, {elimPremise}, {}); + } + } + return newConclusion; +} Node EqProof::addToProof( CDProof* p, std::unordered_map& visited, std::unordered_set& assumptions) const { - return Node::null(); + std::unordered_map::const_iterator it = + visited.find(d_node); + if (it != visited.end()) + { + Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node + << ", returning " << it->second << "\n"; + return it->second; + } + Trace("eqproof-conv") << "EqProof::addToProof: adding step for " + << static_cast(d_id) + << " with conclusion " << d_node << "\n"; + // Assumption + if (d_id == MERGED_THROUGH_EQUALITY) + { + // Check that no (= true/false true/false) assumptions + if (Configuration::isDebugBuild() && d_node.getKind() == kind::EQUAL) + { + for (unsigned i = 0; i < 2; ++i) + { + Assert(d_node[i].getKind() != kind::CONST_BOOLEAN + || d_node[1 - i].getKind() != kind::CONST_BOOLEAN) + << "EqProof::addToProof: fully boolean constant assumption " + << d_node << " is disallowed\n"; + } + } + // If conclusion is (= t true/false), we add a proof step + // t + // ---------------- TRUE/FALSE_INTRO + // (= t true/false) + // according to the value of the Boolean constant + if (d_node.getKind() == kind::EQUAL + && ((d_node[0].getKind() == kind::CONST_BOOLEAN) + != (d_node[1].getKind() == kind::CONST_BOOLEAN))) + { + Trace("eqproof-conv") + << "EqProof::addToProof: add an intro step for " << d_node << "\n"; + // Index of constant in equality + unsigned constIndex = d_node[0].getKind() == kind::CONST_BOOLEAN ? 0 : 1; + // The premise for the intro rule is either t or (not t), according to the + // Boolean constant. + Node introPremise; + PfRule introRule; + if (d_node[constIndex].getConst()) + { + introRule = PfRule::TRUE_INTRO; + introPremise = d_node[1 - constIndex]; + // Track the new assumption. If it's an equality, also its symmetric + assumptions.insert(introPremise); + if (introPremise.getKind() == kind::EQUAL) + { + assumptions.insert(introPremise[1].eqNode(introPremise[0])); + } + } + else + { + introRule = PfRule::FALSE_INTRO; + introPremise = d_node[1 - constIndex].notNode(); + // Track the new assumption. If it's a disequality, also its symmetric + assumptions.insert(introPremise); + if (introPremise[0].getKind() == kind::EQUAL) + { + assumptions.insert( + introPremise[0][1].eqNode(introPremise[0][0]).notNode()); + } + } + // The original assumption can be e.g. (= false (= t1 t2)) in which case + // the necessary proof to be built is + // (not (= t1 t2)) + // -------------------- FALSE_INTRO + // (= (= t1 t2) false) + // -------------------- SYMM + // (= false (= t1 t2)) + // + // with the SYMM step happening automatically whenever the assumption is + // used in the proof p + Node introConclusion = + constIndex == 1 ? d_node : d_node[1].eqNode(d_node[0]); + p->addStep(introConclusion, introRule, {introPremise}, {}); + } + else + { + p->addStep(d_node, PfRule::ASSUME, {}, {d_node}); + } + // If non-equality predicate, turn into one via TRUE/FALSE intro + Node conclusion = d_node; + if (d_node.getKind() != kind::EQUAL) + { + // Track original assumption + assumptions.insert(d_node); + PfRule intro; + if (d_node.getKind() == kind::NOT) + { + intro = PfRule::FALSE_INTRO; + conclusion = + d_node[0].eqNode(NodeManager::currentNM()->mkConst(false)); + } + else + { + intro = PfRule::TRUE_INTRO; + conclusion = + d_node.eqNode(NodeManager::currentNM()->mkConst(true)); + } + Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro + << " step for " << d_node << "\n"; + p->addStep(conclusion, intro, {d_node}, {}); + } + // Keep track of assumptions to avoid cyclic proofs. Both the assumption and + // its symmetric are added + assumptions.insert(conclusion); + assumptions.insert(conclusion[1].eqNode(conclusion[0])); + Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions " + << conclusion << ", (= " << conclusion[1] << " " + << conclusion[0] << ")\n"; + visited[d_node] = conclusion; + return conclusion; + } + // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)), + // which can be safely turned into reflexivity steps. These laborious + // congruence steps are currently generated in the equality engine because of + // the suboptimal handling of n-ary operators. + if (d_id == MERGED_THROUGH_REFLEXIVITY + || (d_node.getKind() == kind::EQUAL && d_node[0] == d_node[1])) + { + Node conclusion = + d_node.getKind() == kind::EQUAL ? d_node : d_node.eqNode(d_node); + p->addStep(conclusion, PfRule::REFL, {}, {conclusion[0]}); + visited[d_node] = conclusion; + return conclusion; + } + // 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()) + << ". Conclusion " << d_node << " from " + << static_cast(d_id) + << " was expected to be (= (= t1 t2) false)\n"; + Assert(!assumptions.count(d_node)) + << "Conclusion " << d_node << " from " + << static_cast(d_id) << " is an assumption\n"; + // The step has the form + // [(= t1 c1)] [(= t2 c2)] + // ------------------------ + // (= (= t1 t2) false) + // where premises equating t1/t2 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). + // + // First recursively process premises, if any + std::vector premises; + for (unsigned i = 0; i < d_children.size(); ++i) + { + Trace("eqproof-conv") + << "EqProof::addToProof: recurse on child " << i << "\n" + << push; + 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 children; + for (unsigned i = 0; i < 2; ++i) + { + Node term = d_node[0][i]; + // term already is a constant, no need to add a premise to it + if (term.isConst()) + { + continue; + } + // Build the equality (= t c) as a premise, finding the respective c is + // the original premises + Node constant; + for (const Node& premise : premises) + { + Assert(premise.getKind() == kind::EQUAL); + if (premise[0] == term) + { + Assert(premise[1].isConst()); + constant = premise[1]; + } + else if (premise[1] == term) + { + Assert(premise[0].isConst()); + constant = premise[0]; + } + } + children.push_back(term.eqNode(constant)); + } + 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}); + visited[d_node] = d_node; + return d_node; + } + // Transtivity and disequality reasoning steps + if (d_id == MERGED_THROUGH_TRANS) + { + Assert(d_node.getKind() == kind::EQUAL + || (d_node.getKind() == kind::NOT + && d_node[0].getKind() == kind::EQUAL)) + << "EqProof::addToProof: transitivity step conclusion " << d_node + << " is not equality or negated equality\n"; + // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which + // is the correct conclusion of the equality reasoning step. A FALSE_ELIM + // step to revert this is only necessary when this is the root. That step is + // done in the non-recursive caller of this function. + Node conclusion = + d_node.getKind() != kind::NOT + ? d_node + : d_node[0].eqNode(NodeManager::currentNM()->mkConst(false)); + // If the conclusion is an assumption, its derivation was spurious, so it + // can be discarded. Moreover, reconstructing the step may lead to cyclic + // proofs, so we *must* cut here. + if (assumptions.count(conclusion)) + { + visited[d_node] = conclusion; + return conclusion; + } + // Process premises recursively + std::vector children; + for (unsigned i = 0, size = d_children.size(); i < size; ++i) + { + // If one of the steps is a "fake congruence" one, marked by a null + // conclusion, it must deleted. Its premises are moved down to premises of + // the transitivity step. + EqProof* childProof = d_children[i].get(); + if (childProof->d_id == MERGED_THROUGH_CONGRUENCE + && childProof->d_node.isNull()) + { + CVC4_UNUSED bool addedChild = false; + Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i + << " is fake cong step. Fold it.\n"; + Assert(childProof->d_children.size() == 2); + Trace("eqproof-conv") << push; + for (unsigned j = 0, sizeJ = childProof->d_children.size(); j < sizeJ; + ++j) + { + Trace("eqproof-conv") + << "EqProof::addToProof: recurse on child " << j << "\n" + << push; + Node child = + childProof->d_children[j]->addToProof(p, visited, assumptions); + Trace("eqproof-conv") << pop; + } + Trace("eqproof-conv") << pop; + Assert(addedChild); + continue; + } + Trace("eqproof-conv") + << "EqProof::addToProof: recurse on child " << i << "\n" + << push; + children.push_back(childProof->addToProof(p, visited, assumptions)); + Trace("eqproof-conv") << pop; + } + // Eliminate spurious premises. Reasoning below assumes no refl steps. + cleanReflPremises(children); + // If any premise is of the form (= (t1 t2) false), then the transitivity + // step may be coarse-grained and needs to be expanded. If the expansion + // happens it also finalizes the proof of conclusion. + if (!expandTransitivityForDisequalities( + conclusion, children, p, assumptions)) + { + Assert(!children.empty()); + Trace("eqproof-conv") + << "EqProof::addToProof: build chain for transitivity premises" + << children << " to conclude " << conclusion << "\n"; + // Build ordered transitivity chain from children to derive the conclusion + buildTransitivityChain(conclusion, children); + Assert(children.size() > 1 + || (!children.empty() + && (children[0] == conclusion + || children[0][1].eqNode(children[0][0]) == conclusion))); + // Only add transitivity step if there is more than one premise in the + // chain. Otherwise the premise will be the conclusion itself and it'll + // already have had a step added to it when the premises were recursively + // processed. + if (children.size() > 1) + { + p->addStep(conclusion, PfRule::TRANS, children, {}, true); + } + } + Assert(p->hasStep(conclusion)); + visited[d_node] = conclusion; + return conclusion; + } + Assert(d_id == MERGED_THROUGH_CONGRUENCE); + // The processing below is mainly dedicated to flattening congruence steps + // (since EqProof assumes currying) and to prossibly reconstructing the + // conclusion in case it involves n-ary steps. + Assert(d_node.getKind() == kind::EQUAL) + << "EqProof::addToProof: conclusion " << d_node << " is not equality\n"; + // The given conclusion is taken as ground truth. If the premises do not + // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we + // use (= t1 t2) as a premise and rely on a symmetry step to justify it. + unsigned arity = d_node[0].getNumChildren(); + Kind k = d_node[0].getKind(); + bool isNary = ExprManager::isNAryKind(k); + + // N-ary operators are fun. The following proof is a valid EqProof + // + // (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6)) + // -------------------------------------------------- TRANS + // (= (f t1 t2 t3) (f t5 t6)) (= t4 t7) + // ------------------------------------------------------------ CONG + // (= (f t1 t2 t3 t4) (f t5 t6 t7)) + // + // We modify the above proof to conclude + // + // (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)) + // + // which is a valid congruence conclusion (applications of f with the same + // arity). For the processing below to be// performed correctly we update + // arity to be maximal one among the two applications (4 in the above + // example). + if (d_node[0].getNumChildren() != d_node[1].getNumChildren()) + { + Assert(isNary); + 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) + std::vector> transitivityChildren; + for (unsigned i = 0; i < arity; ++i) + { + transitivityChildren.push_back(std::vector()); + } + reduceNestedCongruence( + arity - 1, 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 + // empty rows + Node conclusion = d_node; + NodeManager* nm = NodeManager::currentNM(); + if (isNary) + { + unsigned emptyRows = 0; + for (unsigned i = 0; i < arity; ++i) + { + if (transitivityChildren[i].empty()) + { + emptyRows++; + } + } + // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of + // arities n and m, arity = max(n,m), the number emptyRows establishes the + // sizes of the prefixes of f1 of f2 that have been equated via a + // transitivity step. The prefixes necessarily have different sizes. The + // suffixes have the same sizes. The new conclusion will be of the form + // (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1)) + // where + // k1 = emptyRows + 1 - (arity - n) + // k2 = emptyRows + 1 - (arity - m) + // k1 != k2 + // 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. + if (emptyRows > 0) + { + Trace("eqproof-conv") + << "EqProof::addToProof: Found " << emptyRows + << " empty rows. Rebuild conclusion " << d_node << "\n"; + // New transitivity matrix is as before except that the empty rows in the + // 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.clear(); + transitivityChildren.insert(transitivityChildren.begin(), + newTransitivityChildren.begin(), + newTransitivityChildren.end()); + unsigned arityPrefix1 = + emptyRows + 1 - (arity - d_node[0].getNumChildren()); + Assert(arityPrefix1 < d_node[0].getNumChildren()) + << "arityPrefix1 " << arityPrefix1 << " not smaller than " + << d_node[0] << "'s arity " << d_node[0].getNumChildren() << "\n"; + unsigned arityPrefix2 = + emptyRows + 1 - (arity - d_node[1].getNumChildren()); + Assert(arityPrefix2 < d_node[1].getNumChildren()) + << "arityPrefix2 " << arityPrefix2 << " not smaller than " + << d_node[1] << "'s arity " << d_node[1].getNumChildren() << "\n"; + Trace("eqproof-conv") << "EqProof::addToProof: New internal " + "applications with arities " + << arityPrefix1 << ", " << arityPrefix2 << ":\n"; + std::vector childrenPrefix1{d_node[0].begin(), + d_node[0].begin() + arityPrefix1}; + std::vector childrenPrefix2{d_node[1].begin(), + d_node[1].begin() + arityPrefix2}; + Node newFirstChild1 = nm->mkNode(k, childrenPrefix1); + Node newFirstChild2 = nm->mkNode(k, childrenPrefix2); + Trace("eqproof-conv") + << "EqProof::addToProof:\t " << newFirstChild1 << "\n"; + Trace("eqproof-conv") + << "EqProof::addToProof:\t " << newFirstChild2 << "\n"; + std::vector newChildren1{newFirstChild1}; + newChildren1.insert(newChildren1.end(), + d_node[0].begin() + arityPrefix1, + d_node[0].end()); + std::vector newChildren2{newFirstChild2}; + newChildren2.insert(newChildren2.end(), + d_node[1].begin() + arityPrefix2, + d_node[1].end()); + conclusion = nm->mkNode(kind::EQUAL, + nm->mkNode(k, newChildren1), + nm->mkNode(k, newChildren2)); + // update arity + Assert((arity - emptyRows) == conclusion[0].getNumChildren()); + arity = arity - emptyRows; + Trace("eqproof-conv") + << "EqProof::addToProof: New conclusion " << conclusion << "\n"; + } + } + if (Trace.isOn("eqproof-conv")) + { + Trace("eqproof-conv") + << "EqProof::addToProof: premises from reduced cong of " << conclusion + << ":\n"; + for (unsigned i = 0; i < arity; ++i) + { + Trace("eqproof-conv") << "EqProof::addToProof:\t" << i + << "-th arg: " << transitivityChildren[i] << "\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) + { + Node transConclusion = conclusion[0][i].eqNode(conclusion[1][i]); + 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 + if (transConclusion[0] == transConclusion[1]) + { + p->addStep(transConclusion, PfRule::REFL, {}, {transConclusion[0]}); + continue; + } + // Remove spurious refl steps from the premises for (= ai bi) + cleanReflPremises(transitivityChildren[i]); + Assert(transitivityChildren[i].size() > 1 || transitivityChildren[i].empty() + || CDProof::isSame(transitivityChildren[i][0], transConclusion)) + << "EqProof::addToProof: premises " << transitivityChildren[i] << "for " + << i << "-th cong premise " << transConclusion << " don't justify it\n"; + unsigned sizeTrans = transitivityChildren[i].size(); + // If no transitivity premise left or if (= ai bi) is an assumption (which + // might lead to a cycle with a transtivity step), nothing else to do. + if (sizeTrans == 0 || assumptions.count(transConclusion) > 0) + { + continue; + } + // If the transitivity conclusion, or its symmetric, occurs in the + // transitivity premises, nothing to do, as it is already justified and + // doing so again would lead to a cycle. + bool occurs = false; + for (unsigned j = 0; j < sizeTrans && !occurs; ++j) + { + if (CDProof::isSame(transitivityChildren[i][j], transConclusion)) + { + occurs = true; + } + } + if (!occurs) + { + // Build transitivity step + buildTransitivityChain(transConclusion, transitivityChildren[i]); + Trace("eqproof-conv") + << "EqProof::addToProof: adding trans step for cong premise " + << transConclusion << " with children " << transitivityChildren[i] + << "\n"; + p->addStep( + transConclusion, PfRule::TRANS, transitivityChildren[i], {}, true); + } + } + // Get node of the function operator over which congruence is being applied. + std::vector args; + 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] + << " 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 + // rewriting + if (conclusion != d_node) + { + Trace("eqproof-conv") << "EqProof::addToProof: add " + << PfRule::MACRO_SR_PRED_TRANSFORM + << " step to flatten rebuilt conclusion " + << conclusion << "into " << d_node << "\n"; + p->addStep( + d_node, PfRule::MACRO_SR_PRED_TRANSFORM, {conclusion}, {d_node}, true); + } + visited[d_node] = d_node; + return d_node; } } // namespace eq diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index c396da313..ac440dc84 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -116,7 +116,7 @@ class EqProof * Currently the equality engine can represent disequality reasoning in a * rather coarse-grained manner with EqProof. This is always the case when the * transitivity step contains a disequality, (= (= t t') false) or its - * symmetric. + * symmetric, as a premise. * * There are two cases. In the simplest one the general shape of the EqProof * is @@ -180,6 +180,9 @@ class EqProof * EqProof. These are necessary to avoid cyclic proofs, which could be * generated by creating transitivity steps for assumptions (which depend on * themselves). + * @return True if the EqProof transitivity step is in either of the above + * cases, symbolizing that the ProofNode justifying the conclusion has already + * beenproduced. */ bool expandTransitivityForDisequalities( Node conclusion,