From bff7e108a4163f01cbe4947692f126fd091f62dd Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 7 Aug 2024 10:17:31 -0300 Subject: [PATCH] [alethe] Update processing of ProofRule::FORALL_INST (#11129) --- src/proof/alethe/alethe_post_processor.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 58c15667011..8ba071ebc87 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1437,7 +1437,7 @@ bool AletheProofPostprocessCallback::update(Node res, // See proof_rule.h for documentation on the INSTANTIATE rule. This // comment uses variable names as introduced there. // - // ----- FORALL_INST, (= x1 t1) ... (= xn tn) + // ----- FORALL_INST, t1 ... tn // VP1 // ----- OR // VP2 P @@ -1450,15 +1450,15 @@ bool AletheProofPostprocessCallback::update(Node res, // ^ the corresponding proof node is F*sigma case ProofRule::INSTANTIATE: { - for (size_t i = 0, size = children[0][0].getNumChildren(); i < size; i++) - { - new_args.push_back(children[0][0][i].eqNode(args[0][i])); - } Node vp1 = nm->mkNode( Kind::SEXPR, d_cl, nm->mkNode(Kind::OR, children[0].notNode(), res)); Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res); - return addAletheStep( - AletheRule::FORALL_INST, vp1, vp1, {}, new_args, *cdp) + return addAletheStep(AletheRule::FORALL_INST, + vp1, + vp1, + {}, + std::vector{args[0].begin(), args[0].end()}, + *cdp) && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp) && addAletheStep(AletheRule::RESOLUTION, res,