{
return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp);
}
+ // See proof_rule.h for documentation on the SCOPE rule. This comment uses
+ // variable names as introduced there. Since the SCOPE rule originally
+ // concludes
+ // (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) but the ANCHOR rule
+ // concludes (cl (not F1) ... (not Fn) F), to keep the original shape of the
+ // proof node it is necessary to rederive the original conclusion. The
+ // transformation is described below, depending on the form of SCOPE's
+ // conclusion.
+ //
+ // Note that after the original conclusion is rederived the new proof node
+ // will actually have to be printed, respectively, (cl (=> (and F1 ... Fn)
+ // F)) or (cl (not (and F1 ... Fn))).
+ //
+ // Let (not (and F1 ... Fn))^i denote the repetition of (not (and F1 ...
+ // Fn)) for i times.
+ //
+ // T1:
+ //
+ // P
+ // ----- ANCHOR ------- ... ------- AND_POS
+ // VP1 VP2_1 ... VP2_n
+ // ------------------------------------ RESOLUTION
+ // VP2a
+ // ------------------------------------ REORDER
+ // VP2b
+ // ------ DUPLICATED_LITERALS ------- IMPLIES_NEG1
+ // VP3 VP4
+ // ------------------------------------ RESOLUTION ------- IMPLIES_NEG2
+ // VP5 VP6
+ // ----------------------------------------------------------- RESOLUTION
+ // VP7
+ //
+ // VP1: (cl (not F1) ... (not Fn) F)
+ // VP2_i: (cl (not (and F1 ... Fn)) Fi), for i = 1 to n
+ // VP2a: (cl F (not (and F1 ... Fn))^n)
+ // VP2b: (cl (not (and F1 ... Fn))^n F)
+ // VP3: (cl (not (and F1 ... Fn)) F)
+ // VP4: (cl (=> (and F1 ... Fn) F) (and F1 ... Fn)))
+ // VP5: (cl (=> (and F1 ... Fn) F) F)
+ // VP6: (cl (=> (and F1 ... Fn) F) (not F))
+ // VP7: (cl (=> (and F1 ... Fn) F) (=> (and F1 ... Fn) F))
+ //
+ // Note that if n = 1, then the ANCHOR step yields (cl (not F1) F), which is
+ // the same as VP3. Since VP1 = VP3, the steps for that transformation are
+ // not generated.
+ //
+ //
+ // If F = false:
+ //
+ // --------- IMPLIES_SIMPLIFY
+ // T1 VP9
+ // --------- DUPLICATED_LITERALS --------- EQUIV_1
+ // VP8 VP10
+ // -------------------------------------------- RESOLUTION
+ // (cl (not (and F1 ... Fn)))*
+ //
+ // VP8: (cl (=> (and F1 ... Fn))) (cl (not (=> (and F1 ... Fn) false))
+ // (not (and F1 ... Fn)))
+ // VP9: (cl (= (=> (and F1 ... Fn) false) (not (and F1 ... Fn))))
+ //
+ //
+ // Otherwise,
+ // T1
+ // ------------------------------ DUPLICATED_LITERALS
+ // (cl (=> (and F1 ... Fn) F))**
+ //
+ //
+ // * the corresponding proof node is (not (and F1 ... Fn))
+ // ** the corresponding proof node is (=> (and F1 ... Fn) F)
+ case PfRule::SCOPE:
+ {
+ bool success = true;
+
+ // Build vp1
+ std::vector<Node> negNode{d_cl};
+ std::vector<Node> sanitized_args;
+ for (Node arg : args)
+ {
+ negNode.push_back(arg.notNode()); // (not F1) ... (not Fn)
+ sanitized_args.push_back(d_anc.convert(arg));
+ }
+ negNode.push_back(children[0]); // (cl (not F1) ... (not Fn) F)
+ Node vp1 = nm->mkNode(kind::SEXPR, negNode);
+ success &= addAletheStep(AletheRule::ANCHOR_SUBPROOF,
+ vp1,
+ vp1,
+ children,
+ sanitized_args,
+ *cdp);
+
+ Node vp3 = vp1;
+
+ if (args.size() != 1)
+ {
+ // Build vp2i
+ Node andNode = nm->mkNode(kind::AND, args); // (and F1 ... Fn)
+ std::vector<Node> premisesVP2 = {vp1};
+ std::vector<Node> notAnd = {d_cl, children[0]}; // cl F
+ Node vp2_i;
+ for (size_t i = 0, size = args.size(); i < size; i++)
+ {
+ vp2_i = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), args[i]);
+ success &=
+ addAletheStep(AletheRule::AND_POS, vp2_i, vp2_i, {}, {}, *cdp);
+ premisesVP2.push_back(vp2_i);
+ notAnd.push_back(andNode.notNode()); // cl F (not (and F1 ... Fn))^i
+ }
+
+ Node vp2a = nm->mkNode(kind::SEXPR, notAnd);
+ success &= addAletheStep(
+ AletheRule::RESOLUTION, vp2a, vp2a, premisesVP2, {}, *cdp);
+
+ notAnd.erase(notAnd.begin() + 1); //(cl (not (and F1 ... Fn))^n)
+ notAnd.push_back(children[0]); //(cl (not (and F1 ... Fn))^n F)
+ Node vp2b = nm->mkNode(kind::SEXPR, notAnd);
+ success &=
+ addAletheStep(AletheRule::REORDER, vp2b, vp2b, {vp2a}, {}, *cdp);
+
+ Node vp3 =
+ nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]);
+ success &= addAletheStep(
+ AletheRule::DUPLICATED_LITERALS, vp3, vp3, {vp2b}, {}, *cdp);
+ }
+
+ Node vp8 = nm->mkNode(
+ kind::SEXPR, d_cl, nm->mkNode(kind::IMPLIES, andNode, children[0]));
+
+ Node vp4 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], andNode);
+ success &=
+ addAletheStep(AletheRule::IMPLIES_NEG1, vp4, vp4, {}, {}, *cdp);
+
+ Node vp5 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], children[0]);
+ success &=
+ addAletheStep(AletheRule::RESOLUTION, vp5, vp5, {vp4, vp3}, {}, *cdp);
+
+ Node vp6 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], children[0].notNode());
+ success &=
+ addAletheStep(AletheRule::IMPLIES_NEG2, vp6, vp6, {}, {}, *cdp);
+
+ Node vp7 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], vp8[1]);
+ success &=
+ addAletheStep(AletheRule::RESOLUTION, vp7, vp7, {vp5, vp6}, {}, *cdp);
+
+ if (children[0] != nm->mkConst(false))
+ {
+ success &= addAletheStep(
+ AletheRule::DUPLICATED_LITERALS, res, vp8, {vp7}, {}, *cdp);
+ }
+ else
+ {
+ success &= addAletheStep(
+ AletheRule::DUPLICATED_LITERALS, vp8, vp8, {vp7}, {}, *cdp);
+
+ Node vp9 =
+ nm->mkNode(kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::EQUAL, vp8[1], andNode.notNode()));
+
+ success &=
+ addAletheStep(AletheRule::IMPLIES_SIMPLIFY, vp9, vp9, {}, {}, *cdp);
+
+ Node vp10 =
+ nm->mkNode(kind::SEXPR, d_cl, vp8[1].notNode(), andNode.notNode());
+ success &=
+ addAletheStep(AletheRule::EQUIV1, vp10, vp10, {vp9}, {}, *cdp);
+
+ success &= addAletheStep(AletheRule::RESOLUTION,
+ res,
+ nm->mkNode(kind::SEXPR, d_cl, res),
+ {vp8, vp10},
+ {},
+ *cdp);
+ }
+
+ return success;
+ }
default:
{
return addAletheStep(AletheRule::UNDEFINED,
projects / cvc5.git / commitdiff