diff options
Diffstat (limited to 'src/proof/alethe/alethe_post_processor.cpp')
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index b984119ae..5caf565c0 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1365,6 +1365,117 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + //================================================= Quantifiers rules + // ======== Instantiate + // See proof_rule.h for documentation on the INSTANTIATE rule. This + // comment uses variable names as introduced there. + // + // ----- FORALL_INST, (= x1 t1) ... (= xn tn) + // VP1 + // ----- OR + // VP2 P + // -------------------- RESOLUTION + // (cl F*sigma)^ + // + // VP1: (cl (or (not (forall ((x1 T1) ... (xn Tn)) F*sigma) + // VP2: (cl (not (forall ((x1 T1) ... (xn Tn)) F)) F*sigma) + // + // ^ the corresponding proof node is F*sigma + case PfRule::INSTANTIATE: + { + for (size_t i = 0, size = children[0][0].getNumChildren(); i < size; i++) + { + new_args.push_back(children[0][0][i].eqNode(args[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) + && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + {vp2, children[0]}, + {}, + *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, |