diff options
Diffstat (limited to 'src/proof/alethe/alethe_post_processor.cpp')
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 01278134f..b94072ecb 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1398,6 +1398,82 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + //================================================= Arithmetic rules + // ======== Adding Inequalities + // + // ----- LIA_GENERIC + // VP1 P1 ... Pn + // ------------------------------- RESOLUTION + // (cl (>< t1 t2))* + // + // VP1: (cl (not l1) ... (not ln) (>< t1 t2)) + // + // * the corresponding proof node is (>< t1 t2) + case PfRule::MACRO_ARITH_SCALE_SUM_UB: + { + std::vector<Node> vp1s{d_cl}; + for (const Node& child : children) + { + vp1s.push_back(child.notNode()); + } + vp1s.push_back(res); + Node vp1 = nm->mkNode(kind::SEXPR, vp1s); + std::vector<Node> new_children = {vp1}; + new_children.insert(new_children.end(), children.begin(), children.end()); + return addAletheStep(AletheRule::LIA_GENERIC, vp1, vp1, {}, args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } + // ======== Tightening Strict Integer Upper Bounds + // + // ----- LA_GENERIC, 1 + // VP1 P + // ------------------------------------- RESOLUTION + // (cl (<= i greatestIntLessThan(c)))* + // + // VP1: (cl (not (< i c)) (<= i greatestIntLessThan(c))) + // + // * the corresponding proof node is (<= i greatestIntLessThan(c)) + case PfRule::INT_TIGHT_UB: + { + Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); + std::vector<Node> new_children = {vp1, children[0]}; + new_args.push_back(nm->mkConst<Rational>(1)); + return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } + // ======== Tightening Strict Integer Lower Bounds + // + // ----- LA_GENERIC, 1 + // VP1 P + // ------------------------------------- RESOLUTION + // (cl (>= i leastIntGreaterThan(c)))* + // + // VP1: (cl (not (> i c)) (>= i leastIntGreaterThan(c))) + // + // * the corresponding proof node is (>= i leastIntGreaterThan(c)) + case PfRule::INT_TIGHT_LB: + { + Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); + std::vector<Node> new_children = {vp1, children[0]}; + new_args.push_back(nm->mkConst<Rational>(1)); + return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |