Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * The module for post-processing proof nodes for DSL rewrite reconstruction.
14 : : */
15 : :
16 : : #include "smt/proof_post_processor_dsl.h"
17 : :
18 : : #include "options/base_options.h"
19 : : #include "options/smt_options.h"
20 : : #include "proof/proof_ensure_closed.h"
21 : :
22 : : using namespace cvc5::internal::theory;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace smt {
26 : :
27 : 3563 : ProofPostprocessDsl::ProofPostprocessDsl(Env& env, rewriter::RewriteDb* rdb)
28 : 3563 : : EnvObj(env), d_rdbPc(env, rdb)
29 : : {
30 : 3563 : d_true = nodeManager()->mkConst(true);
31 : 3563 : d_tmode = (options().proof.proofGranularityMode
32 : : == options::ProofGranularityMode::DSL_REWRITE_STRICT)
33 [ - + ]: 3563 : ? rewriter::TheoryRewriteMode::RESORT
34 : : : rewriter::TheoryRewriteMode::STANDARD;
35 : 3563 : }
36 : :
37 : 3727 : void ProofPostprocessDsl::reconstruct(
38 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
39 : : {
40 [ + + ]: 3727 : if (pfs.empty())
41 : : {
42 : 176 : return;
43 : : }
44 [ + - ]: 7102 : Trace("pp-dsl") << "Reconstruct proofs for " << pfs.size()
45 : 3551 : << " trusted steps..." << std::endl;
46 : : // run an updater for this callback
47 : 7102 : ProofNodeUpdater pnu(d_env, *this, false);
48 [ + + ]: 483579 : for (std::shared_ptr<ProofNode> p : pfs)
49 : : {
50 : 480028 : d_traversing.clear();
51 [ + - ]: 480028 : Trace("pp-dsl-process") << "BEGIN update" << std::endl;
52 : 480028 : pnu.process(p);
53 [ + - ]: 480028 : Trace("pp-dsl-process") << "END update" << std::endl;
54 [ - + ][ - + ]: 480028 : Assert(d_traversing.empty());
[ - - ]
55 : : }
56 : : }
57 : :
58 : 1150050 : bool ProofPostprocessDsl::shouldUpdate(std::shared_ptr<ProofNode> pn,
59 : : const std::vector<Node>& fa,
60 : : bool& continueUpdate)
61 : : {
62 : 1150050 : ProofRule id = pn->getRule();
63 : 1150050 : continueUpdate = true;
64 : : // we should update if we
65 : : // - Have rule TRUST or TRUST_THEORY_REWRITE,
66 : : // - We have no premises
67 : : // - We are not already recursively expanding >= 3 steps of the above form.
68 : : // We check for the third criteria by tracking a d_traversing vector.
69 [ + + ]: 1136180 : if ((id == ProofRule::TRUST || id == ProofRule::TRUST_THEORY_REWRITE)
70 [ + + ][ + + ]: 2286230 : && pn->getChildren().empty() && d_traversing.size() < 3)
[ + + ][ + + ]
71 : : {
72 [ + - ]: 354448 : Trace("pp-dsl-process") << "...push " << pn.get() << std::endl;
73 : 354448 : d_traversing.push_back(pn);
74 : 354448 : return true;
75 : : }
76 : 795603 : return false;
77 : : }
78 : :
79 : 1150050 : bool ProofPostprocessDsl::shouldUpdatePost(std::shared_ptr<ProofNode> pn,
80 : : const std::vector<Node>& fa)
81 : : {
82 : : // clean up d_traversing at post-traversal
83 : : // note we may have pushed multiple copies of pn consecutively if a proof
84 : : // was updated to another trust step.
85 [ + + ][ + + ]: 1150050 : while (!d_traversing.empty() && d_traversing.back() == pn)
[ + + ]
86 : : {
87 [ + - ]: 351138 : Trace("pp-dsl-process") << "...pop " << pn.get() << std::endl;
88 : 351138 : d_traversing.pop_back();
89 : : }
90 : 798913 : return false;
91 : : }
92 : :
93 : 354448 : bool ProofPostprocessDsl::update(Node res,
94 : : ProofRule id,
95 : : const std::vector<Node>& children,
96 : : const std::vector<Node>& args,
97 : : CDProof* cdp,
98 : : bool& continueUpdate)
99 : : {
100 : 354448 : continueUpdate = false;
101 [ + + ][ - + ]: 354448 : Assert(id == ProofRule::TRUST || id == ProofRule::TRUST_THEORY_REWRITE);
[ - + ][ - - ]
102 [ - + ][ - + ]: 354448 : Assert(children.empty());
[ - - ]
103 [ - + ][ - + ]: 354448 : Assert(!res.isNull());
[ - - ]
104 : 354448 : bool reqTrueElim = false;
105 : : // if not an equality, make (= res true).
106 [ + + ]: 354448 : if (res.getKind() != Kind::EQUAL)
107 : : {
108 : 2288 : res = res.eqNode(d_true);
109 : 2288 : reqTrueElim = true;
110 : : }
111 : 354448 : TheoryId tid = THEORY_LAST;
112 : 354448 : MethodId mid = MethodId::RW_REWRITE;
113 : 354448 : rewriter::TheoryRewriteMode tm = d_tmode;
114 : : // if theory rewrite, get diagnostic information
115 [ + + ]: 354448 : if (id == ProofRule::TRUST_THEORY_REWRITE)
116 : : {
117 : 341296 : builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid);
118 : 341296 : getMethodId(args[2], mid);
119 : : }
120 [ + - ]: 13152 : else if (id == ProofRule::TRUST)
121 : : {
122 : : TrustId trid;
123 : 13152 : getTrustId(args[0], trid);
124 [ + + ]: 13152 : if (trid == TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE)
125 : : {
126 : : // If we are MACRO_THEORY_REWRITE_RCONS_SIMPLE, we do not use
127 : : // theory rewrites. This policy ensures that macro theory rewrites are
128 : : // disabled on rewrites which we use for their own reconstruction.
129 : 4608 : tm = rewriter::TheoryRewriteMode::NEVER;
130 : : }
131 : : }
132 [ + - ]: 708896 : Trace("pp-dsl") << "Prove " << res << " from " << tid << " / " << mid
133 : 354448 : << ", in mode " << tm << std::endl;
134 : 354448 : int64_t recLimit = options().proof.proofRewriteRconsRecLimit;
135 : 354448 : int64_t stepLimit = options().proof.proofRewriteRconsStepLimit;
136 : : // Attempt to reconstruct the proof of the equality into cdp using the
137 : : // rewrite database proof reconstructor.
138 : : // We record the subgoals in d_subgoals.
139 [ + + ]: 354448 : if (d_rdbPc.prove(cdp, res[0], res[1], recLimit, stepLimit, tm))
140 : : {
141 : : // we will update this again, in case the elaboration introduced
142 : : // new trust steps
143 : 351138 : continueUpdate = true;
144 : : // If we made (= res true) above, conclude the original res.
145 [ + + ]: 351138 : if (reqTrueElim)
146 : : {
147 : 304 : cdp->addStep(res[0], ProofRule::TRUE_ELIM, {res}, {});
148 : 152 : res = res[0];
149 : : }
150 [ + - ]: 351138 : Trace("check-dsl") << "Check closed..." << std::endl;
151 [ + - ]: 351138 : pfgEnsureClosed(options(), res, cdp, "check-dsl", "check dsl");
152 : : // if successful, we update the proof
153 : 351138 : return true;
154 : : }
155 : : // clean up traversing, since we are setting continueUpdate to false
156 [ - + ][ - + ]: 3310 : Assert (!d_traversing.empty());
[ - - ]
157 [ + - ]: 3310 : Trace("pp-dsl-process") << "...pop due to fail " << d_traversing.back().get() << std::endl;
158 : 3310 : d_traversing.pop_back();
159 : : // otherwise no update
160 : 3310 : return false;
161 : : }
162 : :
163 : : } // namespace smt
164 : : } // namespace cvc5::internal
|
