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 : : #include "proof/proof_node_algorithm.h"
22 : : #include "smt/env.h"
23 : :
24 : : using namespace cvc5::internal::theory;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace smt {
28 : :
29 : 6643 : ProofPostprocessDsl::ProofPostprocessDsl(Env& env, rewriter::RewriteDb* rdb)
30 : 6643 : : EnvObj(env), d_rdbPc(env, rdb)
31 : : {
32 : 6643 : d_true = nodeManager()->mkConst(true);
33 : 6643 : d_tmode = (options().proof.proofGranularityMode
34 : : == options::ProofGranularityMode::DSL_REWRITE_STRICT)
35 [ - + ]: 6643 : ? rewriter::TheoryRewriteMode::RESORT
36 : : : rewriter::TheoryRewriteMode::STANDARD;
37 : 6643 : }
38 : :
39 : 5606 : void ProofPostprocessDsl::reconstruct(
40 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
41 : : {
42 [ + + ]: 5606 : if (pfs.empty())
43 : : {
44 : 997 : return;
45 : : }
46 [ + - ]: 9218 : Trace("pp-dsl") << "Reconstruct proofs for " << pfs.size()
47 : 4609 : << " trusted steps..." << std::endl;
48 : : // Run an updater for this callback. We do subproof merging, as we may
49 : : // encounter "subgoals" of theory rewrites that are the same. Moreover,
50 : : // since subproof merging is only in scope for a single run of an updater,
51 : : // we tie the proofs in pfs together with an AND_INTRO step, if necessary.
52 : 4609 : d_traversing.clear();
53 : 9218 : ProofNodeUpdater pnu(d_env, *this, true);
54 : 0 : std::shared_ptr<ProofNode> pfn;
55 [ + + ]: 4609 : if (pfs.size() > 1)
56 : : {
57 : 4366 : ProofNodeManager* pnm = d_env.getProofNodeManager();
58 : 4366 : pfn = pnm->mkNode(ProofRule::AND_INTRO, pfs, {});
59 : : }
60 : : else
61 : : {
62 : 243 : pfn = pfs[0];
63 : : }
64 [ + - ]: 4609 : Trace("pp-dsl-process") << "BEGIN update" << std::endl;
65 : 4609 : pnu.process(pfn);
66 [ + - ]: 4609 : Trace("pp-dsl-process") << "END update" << std::endl;
67 : : }
68 : :
69 : 1048690 : bool ProofPostprocessDsl::shouldUpdate(std::shared_ptr<ProofNode> pn,
70 : : const std::vector<Node>& fa,
71 : : bool& continueUpdate)
72 : : {
73 : 1048690 : ProofRule id = pn->getRule();
74 : 1048690 : continueUpdate = true;
75 : : // we should update if we
76 : : // - Have rule TRUST or TRUST_THEORY_REWRITE,
77 : : // - We have no premises
78 : : // - We are not already recursively expanding >= 3 steps of the above form.
79 : : // We check for the third criteria by tracking a d_traversing vector.
80 [ + + ]: 999922 : if ((id == ProofRule::TRUST || id == ProofRule::TRUST_THEORY_REWRITE)
81 [ + + ][ + + ]: 2048610 : && pn->getChildren().empty() && d_traversing.size() < 3)
[ + - ][ + + ]
82 : : {
83 [ + - ]: 391264 : Trace("pp-dsl-process") << "...push " << pn.get() << std::endl;
84 : : // note that we may be pushing pn more than once, if it is updated from a
85 : : // trust step to another trust step.
86 : 391264 : d_traversing.push_back(pn);
87 : 391264 : return true;
88 : : }
89 : 657425 : return false;
90 : : }
91 : :
92 : 1045660 : void ProofPostprocessDsl::finalize(std::shared_ptr<ProofNode> pn)
93 : : {
94 : : // clean up d_traversing at post-traversal
95 : : // note we may have pushed multiple copies of pn consecutively if a proof
96 : : // was updated to another trust step.
97 [ + + ][ + + ]: 1045660 : while (!d_traversing.empty() && d_traversing.back() == pn)
[ + + ]
98 : : {
99 [ + - ]: 388237 : Trace("pp-dsl-process") << "...pop " << pn.get() << std::endl;
100 : 388237 : d_traversing.pop_back();
101 : : }
102 : 657425 : }
103 : :
104 : 391264 : bool ProofPostprocessDsl::update(Node res,
105 : : ProofRule id,
106 : : const std::vector<Node>& children,
107 : : const std::vector<Node>& args,
108 : : CDProof* cdp,
109 : : bool& continueUpdate)
110 : : {
111 : 391264 : continueUpdate = false;
112 [ + + ][ - + ]: 391264 : Assert(id == ProofRule::TRUST || id == ProofRule::TRUST_THEORY_REWRITE);
[ - + ][ - - ]
113 [ - + ][ - + ]: 391264 : Assert(children.empty());
[ - - ]
114 [ - + ][ - + ]: 391264 : Assert(!res.isNull());
[ - - ]
115 : 391264 : bool reqTrueElim = false;
116 : : // if not an equality, make (= res true).
117 [ + + ]: 391264 : if (res.getKind() != Kind::EQUAL)
118 : : {
119 : 2198 : res = res.eqNode(d_true);
120 : 2198 : reqTrueElim = true;
121 : : }
122 : 391264 : TheoryId tid = THEORY_LAST;
123 : 391264 : MethodId mid = MethodId::RW_REWRITE;
124 : 391264 : rewriter::TheoryRewriteMode tm = d_tmode;
125 [ + - ]: 782528 : Trace("pp-dsl") << "Prove " << res << " from " << tid << " / " << mid
126 : 391264 : << ", in mode " << tm << std::endl;
127 [ + - ]: 391264 : Trace("pp-dsl") << "...proof rule " << id << std::endl;
128 : : // if theory rewrite, get diagnostic information
129 [ + + ]: 391264 : if (id == ProofRule::TRUST_THEORY_REWRITE)
130 : : {
131 : 342893 : builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid);
132 : 342893 : getMethodId(args[2], mid);
133 : : }
134 [ + - ]: 48371 : else if (id == ProofRule::TRUST)
135 : : {
136 : : TrustId trid;
137 : 48371 : getTrustId(args[0], trid);
138 [ + - ]: 48371 : Trace("pp-dsl") << "...trust id " << trid << std::endl;
139 [ + + ]: 48371 : if (trid == TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE)
140 : : {
141 : : // If we are MACRO_THEORY_REWRITE_RCONS_SIMPLE, we do not use
142 : : // theory rewrites. This policy ensures that macro theory rewrites are
143 : : // disabled on rewrites which we use for their own reconstruction.
144 : 36670 : tm = rewriter::TheoryRewriteMode::NEVER;
145 : : }
146 : : }
147 : 391264 : int64_t recLimit = options().proof.proofRewriteRconsRecLimit;
148 : 391264 : int64_t stepLimit = options().proof.proofRewriteRconsStepLimit;
149 : : // Attempt to reconstruct the proof of the equality into cdp using the
150 : : // rewrite database proof reconstructor.
151 : : // We record the subgoals in d_subgoals.
152 [ + + ]: 391264 : if (d_rdbPc.prove(cdp, res[0], res[1], recLimit, stepLimit, tm))
153 : : {
154 : : // we will update this again, in case the elaboration introduced
155 : : // new trust steps
156 : 388237 : continueUpdate = true;
157 : : // If we made (= res true) above, conclude the original res.
158 [ + + ]: 388237 : if (reqTrueElim)
159 : : {
160 : 388 : cdp->addStep(res[0], ProofRule::TRUE_ELIM, {res}, {});
161 : 194 : res = res[0];
162 : : }
163 [ + - ]: 388237 : Trace("check-dsl") << "Check closed..." << std::endl;
164 [ + - ]: 388237 : pfgEnsureClosed(options(), res, cdp, "check-dsl", "check dsl");
165 : : // if successful, we update the proof
166 : 388237 : return true;
167 : : }
168 : : // clean up traversing, since we are setting continueUpdate to false
169 [ - + ][ - + ]: 3027 : Assert (!d_traversing.empty());
[ - - ]
170 [ + - ]: 3027 : Trace("pp-dsl-process") << "...pop due to fail " << d_traversing.back().get() << std::endl;
171 : 3027 : d_traversing.pop_back();
172 : : // otherwise no update
173 : 3027 : return false;
174 : : }
175 : :
176 : : } // namespace smt
177 : : } // namespace cvc5::internal
|
