From: Haniel Barbosa Date: Thu, 13 Aug 2020 00:01:40 +0000 (-0300) Subject: [proof-new] Adding support for corner case of transitivity simulating MERGED_THROUGH_... X-Git-Tag: cvc5-1.0.0~3008 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2fc0fea69f6350db55d217e710efcc08ac56b4db;p=cvc5.git [proof-new] Adding support for corner case of transitivity simulating MERGED_THROUGH_CONSTANTS (#4879) --- diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 15979bd44..513cf2f39 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -535,6 +535,88 @@ bool EqProof::expandTransitivityForDisequalities( return true; } +// TEMPORARY NOTE: This may not be enough. Worst case scenario I need to +// reproduce here a search for arbitrary chains between each of the variables in +// the conclusion and a constant +bool EqProof::expandTransitivityForTheoryDisequalities( + Node conclusion, std::vector& premises, CDProof* p) const +{ + // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry + unsigned termPos = -1; + for (unsigned i = 0; i < 2; ++i) + { + if (conclusion[i].getKind() == kind::CONST_BOOLEAN + && !conclusion[i].getConst() + && conclusion[1 - i].getKind() == kind::EQUAL) + { + termPos = i - 1; + break; + } + } + // no disequality + if (termPos == static_cast(-1)) + { + return false; + } + Trace("eqproof-conv") + << "EqProof::expandTransitivityForTheoryDisequalities: check if need " + "to expand transitivity step to conclude disequality " + << conclusion << " from premises " << premises << "\n"; + + // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry + std::vector subChildren, constChildren; + for (unsigned i = 0; i < 2; ++i) + { + Node term = conclusion[termPos][i]; + for (const Node& premise : premises) + { + for (unsigned j = 0; j < 2; ++j) + { + if (premise[j] == term && premise[1 - j].isConst()) + { + subChildren.push_back(premise[j].eqNode(premise[1 - j])); + constChildren.push_back(premise[1 - j]); + break; + } + } + } + } + if (subChildren.size() < 2) + { + return false; + } + // Now build + // (= t1 c1) (= t2 c2) + // ------------------------- CONG ------------------- MACRO_SR_PRED_INTRO + // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false) + // --------------------------------------------------------------------- TR + // (= (= t1 t2) false) + Node constApp = NodeManager::currentNM()->mkNode(kind::EQUAL, constChildren); + Node constEquality = constApp.eqNode(conclusion[1 - termPos]); + Trace("eqproof-conv") + << "EqProof::expandTransitivityForTheoryDisequalities: adding " + << PfRule::MACRO_SR_PRED_INTRO << " step for " << constApp << " = " + << conclusion[1 - termPos] << "\n"; + p->addStep(constEquality, PfRule::MACRO_SR_PRED_INTRO, {}, {constEquality}); + // build congruence conclusion (= (= t1 t2) (t c1 c2)) + Node congConclusion = conclusion[termPos].eqNode(constApp); + Trace("eqproof-conv") + << "EqProof::expandTransitivityForTheoryDisequalities: adding " + << PfRule::CONG << " step for " << congConclusion << " from " + << subChildren << "\n"; + p->addStep(congConclusion, + PfRule::CONG, + {subChildren}, + {ProofRuleChecker::mkKindNode(kind::EQUAL)}, + true); + Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via " + "congruence derived " + << congConclusion << "\n"; + std::vector transitivityChildren{congConclusion, constEquality}; + p->addStep(conclusion, PfRule::TRANS, {transitivityChildren}, {}); + return true; +} + bool EqProof::buildTransitivityChain(Node conclusion, std::vector& premises) const { @@ -1059,22 +1141,30 @@ Node EqProof::addToProof( 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) + // similarly, if a disequality is concluded because of theory reasoning, + // the step is coarse-grained and needs to be expanded, in which case the + // proof is finalized in the call + if (!expandTransitivityForTheoryDisequalities(conclusion, children, p)) { - p->addStep(conclusion, PfRule::TRANS, children, {}, true); + 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)); diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index ac440dc84..492252baa 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -182,7 +182,7 @@ class EqProof * 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. + * been produced. */ bool expandTransitivityForDisequalities( Node conclusion, @@ -190,6 +190,36 @@ class EqProof CDProof* p, std::unordered_set& assumptions) const; + /** Expand coarse-grained transitivity steps for theory disequalities + * + * Currently the equality engine can represent disequality reasoning of theory + * symbols in a rather coarse-grained manner with EqProof. This is the case + * when EqProof is + * (= t1 c1) (= t2 c2) + * ------------------------------------- EQP::TR + * (= (t1 t2) false) + * + * which is converted into + * + * (= t1 c1) (= t2 c2) + * -------------------------- CONG --------------------- MACRO_SR_PRED_INTRO + * (= (= t1 t2) (= c1 t2)) (= (= c1 c2) false) + * --------------------------------------------------------- TR + * (= (= t1 t2) false) + * + * @param conclusion the conclusion of the (possibly) coarse-grained + * transitivity step + * @param premises the premises of the (possibly) coarse-grained + * transitivity step + * @param p a pointer to a CDProof to store the conversion of this EqProof + * @return True if the EqProof transitivity step is the above case, + * indicating that the ProofNode justifying the conclusion has already been + * produced. + */ + bool expandTransitivityForTheoryDisequalities(Node conclusion, + std::vector& premises, + CDProof* p) const; + /** Builds a transitivity chain from equalities to derive a conclusion * * Given an equality (= t1 tn), and a list of equalities premises, attempts to