diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 30cd7905654..c96740302fe 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1620,6 +1620,9 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + bool success = true; + Node lhsQ = res[0]; + std::vector transEqs; if (hasClash) { // create the variables to substitute the lhs variables @@ -1628,104 +1631,58 @@ bool AletheProofPostprocessCallback::update(Node res, { freshRenaming.emplace_back(NodeManager::mkBoundVar(v.getType())); } - - { - - std::vector vars{res[0][0].begin(), - res[0][0].end()}; - Node resRenamed = res[0].substitute(vars.begin(), - vars.end(), - freshRenaming.begin(), - freshRenaming.end()); - } + std::vector vars{res[0][0].begin(), res[0][0].end()}; + Node lhsRenamed = res[0].substitute(vars.begin(), + vars.end(), + freshRenaming.begin(), + freshRenaming.end()); // Reflexivity over the quantified bodies - Node reflConc = nm->mkNode( - Kind::SEXPR, d_cl, nm->mkNode(Kind::EQUAL, res[1], resRenamed[1])); + Node reflConc = + nm->mkNode(Kind::SEXPR, d_cl, res[0][1].eqNode(lhsRenamed[1])); addAletheStep(AletheRule::REFL, reflConc, reflConc, {}, {}, *cdp); // Collect RHS variables first for arguments, then add the entries for // the substitution. In a "bind" rule we must always list all the // variables - std::vector bindArgs{freshRenaming[0].begin(), freshRenaming[0].end()}; + std::vector bindArgs{freshRenaming.begin(), freshRenaming.end()}; for (size_t i = 0, size = freshRenaming.size(); i < size; ++i) { bindArgs.push_back(vars[i].eqNode(freshRenaming[i])); } - Node freshRenamingConc = binds.push_back(lhsQ.eqNode(rhsQ)); + transEqs.push_back(res[0].eqNode(lhsRenamed)); success &= addAletheStep(AletheRule::ANCHOR_BIND, - freshRenamingConc, - nm->mkNode(Kind::SEXPR, d_cl, binds.back()), + transEqs.back(), + nm->mkNode(Kind::SEXPR, d_cl, transEqs.back()), {reflConc}, bindArgs, *cdp); - + lhsQ = lhsRenamed; } - Node lhsQ = res[0]; - - - Node rhsQ; - { - Assert(renamingEndingPos <= lhsQ[0].getNumChildren()); - std::vector subLhs{res[0][0].begin() + prefixStart, - res[0][0].begin() + renamingEndingPos}; - std::vector subRhs{res[1][0].begin() + prefixStart, - res[1][0].begin() + renamingEndingPos}; - rhsQ = lhsQ.substitute( - subLhs.begin(), subLhs.end(), subRhs.begin(), subRhs.end()); - } - // Reflexivity over the quantified bodies - Node reflConc = nm->mkNode( - Kind::SEXPR, d_cl, nm->mkNode(Kind::EQUAL, lhsQ[1], rhsQ[1])); - addAletheStep(AletheRule::REFL, reflConc, reflConc, {}, {}, *cdp); - // Collect RHS variables first for arguments, then add the entries for - // the substitution. In a "bind" rule we must always list all the - // variables - std::vector bindArgs{rhsQ[0].begin(), rhsQ[0].end()}; - for (size_t i = 0; i < rhsQ[0].getNumChildren(); ++i) - { - bindArgs.push_back(lhsQ[0][i].eqNode(rhsQ[0][i])); - } - binds.push_back(lhsQ.eqNode(rhsQ)); - success &= addAletheStep(AletheRule::ANCHOR_BIND, - binds.back(), - nm->mkNode(Kind::SEXPR, d_cl, binds.back()), - {reflConc}, - bindArgs, - *cdp); - // get next valid segment. Note that this will be a no-op when the first - // check in the beginning of the translation did not find an invalid - // renaming, so the whole quantifier has already been processed above. - lhsQ = rhsQ; - lhsNames.clear(); - bool hasInvalidRenaming = false; - prefixStart = renamingEndingPos; - Trace("alethe-proof") << "\tcheck from " << renamingEndingPos << " to " - << res[0][0].getNumChildren() << "\n"; - for (size_t i = renamingEndingPos, size = res[0][0].getNumChildren(); - i < size; - ++i) - { - Node v0 = res[0][0][i], v1 = res[1][0][i]; - if (std::find(lhsNames.begin(), lhsNames.end(), v1.getName()) - != lhsNames.end()) - { - Assert(i > 0); - hasInvalidRenaming = true; - renamingEndingPos = i; - break; - } - lhsNames.push_back(v0.getName()); - } - renamingEndingPos = - hasInvalidRenaming ? renamingEndingPos : res[0][0].getNumChildren(); - - // if we added more than one "bind" step, we connect them via transitivity - if (binds.size() > 1) + // Reflexivity over the quantified bodies + Node reflConc = nm->mkNode(Kind::SEXPR, d_cl, lhsQ[1].eqNode(res[1][1])); + addAletheStep(AletheRule::REFL, reflConc, reflConc, {}, {}, *cdp); + // Collect RHS variables first for arguments, then add the entries for + // the substitution. In a "bind" rule we must always list all the + // variables + std::vector bindArgs{res[1][0].begin(), res[1][0].end()}; + for (size_t i = 0, size = res[1][0].getNumChildren(); i < size; ++i) + { + bindArgs.push_back(lhsQ[0][i].eqNode(res[1][0][i])); + } + transEqs.push_back(lhsQ.eqNode(res[1])); + success &= addAletheStep(AletheRule::ANCHOR_BIND, + transEqs.back(), + nm->mkNode(Kind::SEXPR, d_cl, transEqs.back()), + {reflConc}, + bindArgs, + *cdp); + Assert(!hasClash || transEqs.size() == 2); + if (hasClash) { return success && addAletheStep(AletheRule::TRANS, res, nm->mkNode(Kind::SEXPR, d_cl, res), - binds, + transEqs, {}, *cdp); } diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 3a13943b4b9..6e875fb75c1 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -154,9 +154,6 @@ class AletheProofPostprocessCallback : protected EnvObj, /** Nodes corresponding to the Boolean values. */ Node d_true; Node d_false; - - /** */ - uint_32 d_varIdCount; }; /** diff --git a/test/regress/cli/regress0/proofs/alpha-equiv-reusing-variable2.smt2 b/test/regress/cli/regress0/proofs/alpha-equiv-reusing-variable2.smt2 index 994b2b4c291..5d99ae2fa79 100644 --- a/test/regress/cli/regress0/proofs/alpha-equiv-reusing-variable2.smt2 +++ b/test/regress/cli/regress0/proofs/alpha-equiv-reusing-variable2.smt2 @@ -1,4 +1,4 @@ -; --full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear --no-stats --random-seed=1 --lang=smt2 --tlimit 300000 +; EXPECT: unsat (set-logic AUFLIA) (declare-sort Index$ 0) (declare-sort State1$ 0)