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