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 : : * Rewrite database proof reconstructor
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__REWRITE_DB_PROOF_CONS__H
16 : : #define CVC5__THEORY__REWRITE_DB_PROOF_CONS__H
17 : :
18 : : #include <map>
19 : :
20 : : #include "expr/match_trie.h"
21 : : #include "expr/node.h"
22 : : #include "proof/proof.h"
23 : : #include "proof/proof_generator.h"
24 : : #include "rewriter/basic_rewrite_rcons.h"
25 : : #include "rewriter/rewrite_db.h"
26 : : #include "rewriter/rewrite_db_term_process.h"
27 : : #include "rewriter/rewrite_proof_status.h"
28 : : #include "rewriter/rewrites.h"
29 : : #include "smt/env_obj.h"
30 : : #include "theory/evaluator.h"
31 : : #include "util/statistics_stats.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace rewriter {
35 : :
36 : : /**
37 : : * This class is used to reconstruct proofs of theory rewrites. It is described
38 : : * in detail in the paper "Reconstructing Fine-Grained Proofs of Rewrites Using
39 : : * a Domain-Specific Language", Noetzli et al FMCAD 2022.
40 : : */
41 : : class RewriteDbProofCons : protected EnvObj
42 : : {
43 : : public:
44 : : RewriteDbProofCons(Env& env, RewriteDb* db);
45 : : /**
46 : : * Prove a = b with recursion limit recLimit and step limit stepLimit.
47 : : * If cdp is provided, we add a proof for this fact on it.
48 : : *
49 : : * More specifically, the strategy used by this method is:
50 : : * 1. Try to prove a=b via THEORY_REWRITE in context
51 : : * TheoryRewriteCtx::PRE_DSL,
52 : : * 2. Try to prove a=b via a proof involving RARE rewrites,
53 : : * 3. Try to prove a'=b' via a proof involving RARE rewrites, where a' and b'
54 : : * are obtained by transforming a and b via RewriteDbNodeConverter.
55 : : * 4. Try to prove a=b via THEORY_REWRITE in context
56 : : * TheoryRewriteCtx::POST_DSL.
57 : : *
58 : : * The option --proof-granularity=dsl-rewrite-strict essentially moves step 1
59 : : * after step 3, that is, RARE rewrites are always preferred to
60 : : * THEORY_REWRITE.
61 : : *
62 : : * @param cdp The object to add the proof of (= a b) to.
63 : : * @param a The left hand side of the equality.
64 : : * @param b The right hand side of the equality.
65 : : * @param recLimit The recursion limit for this call.
66 : : * @param stepLimit The step limit for this call.
67 : : * @param tmode Determines if/when to try THEORY_REWRITE.
68 : : * @return true if we successfully added a proof of (= a b) to cdp
69 : : */
70 : : bool prove(CDProof* cdp,
71 : : const Node& a,
72 : : const Node& b,
73 : : int64_t recLimit,
74 : : int64_t stepLimit,
75 : : TheoryRewriteMode tmode);
76 : :
77 : : private:
78 : : /**
79 : : * Preprocess closure equality. This is called at the beginning of prove to
80 : : * simplify equalities between closures. In particular we apply two possible
81 : : * simplifications:
82 : : *
83 : : * For (forall x P) = (forall x Q), we return P = Q, where a CONG step
84 : : * is added to transform this step. That is, the proof is:
85 : : *
86 : : * P = Q
87 : : * ----------------------------- CONG
88 : : * (forall x. P) = (forall x. Q)
89 : : *
90 : : * where P = Q is left to prove.
91 : : *
92 : : * For (forall x. P) = (forall y. Q), we return
93 : : * (forall y. P[y/x]) = (forall y. Q). If P[y/x] is not Q, the proof is:
94 : : *
95 : : * ----------------------- ALPHA_EQUIV
96 : : * (forall x. P) = (forall y. P[y/x]) (forall y. P[y/x]) = (forall y. Q)
97 : : * ----------------------------------------------------------------- TRANS
98 : : * (forall x. P) = (forall y. Q)
99 : : *
100 : : * where (forall y. P[y/x]) = (forall y. Q) is left to prove. If P[y/x] is Q,
101 : : * the proof is:
102 : : *
103 : : * ----------------------------- ALPHA_EQUIV
104 : : * (forall x. P) = (forall y. Q)
105 : : *
106 : : * where (forall y. Q) = (forall y. Q) is left to prove (trivially).
107 : : *
108 : : * In either case, we add a proof of (= a b) whose free assumptions are
109 : : * either empty (if the returned equality is reflexive), or the returned
110 : : * equality.
111 : : */
112 : : Node preprocessClosureEq(CDProof* cdp, const Node& a, const Node& b);
113 : : /**
114 : : * Notify class for the match trie, which is responsible for calling this
115 : : * class to notify matches for heads of rewrite rules. It is used as a
116 : : * callback to the match procedure in the trie maintained by this class.
117 : : */
118 : : class RdpcMatchTrieNotify : public expr::NotifyMatch
119 : : {
120 : : public:
121 : 6833 : RdpcMatchTrieNotify(RewriteDbProofCons& p) : d_parent(p) {}
122 : : /** Reference to the parent */
123 : : RewriteDbProofCons& d_parent;
124 : : /** notify the parent */
125 : 1650414 : bool notify(Node s,
126 : : Node n,
127 : : std::vector<Node>& vars,
128 : : std::vector<Node>& subs) override
129 : : {
130 : 1650414 : return d_parent.notifyMatch(s, n, vars, subs);
131 : : }
132 : : };
133 : : /**
134 : : * Proven info, which stores information for each equality we attempt to
135 : : * prove, including whether we were successful and what is the maximum
136 : : * depth we have tried if we have failed.
137 : : */
138 : : class ProvenInfo
139 : : {
140 : : public:
141 : 14982787 : ProvenInfo()
142 : 14982787 : : d_id(RewriteProofStatus::FAIL),
143 : 14982787 : d_dslId(ProofRewriteRule::NONE),
144 : 14982787 : d_failMaxDepth(-1)
145 : : {
146 : 14982787 : }
147 : : /** The identifier of the proof rule, or fail if we failed */
148 : : RewriteProofStatus d_id;
149 : : /** The identifier of the DSL proof rule if d_id is DSL */
150 : : ProofRewriteRule d_dslId;
151 : : /** The substitution used, if successful */
152 : : std::vector<Node> d_vars;
153 : : std::vector<Node> d_subs;
154 : : /**
155 : : * The maximum depth tried for rules that have failed, where -1 indicates
156 : : * that the formula is unprovable at any depth.
157 : : */
158 : : int64_t d_failMaxDepth;
159 : : /**
160 : : * Is internal rule? these rules store children (if any) in d_vars.
161 : : */
162 : 1506890 : bool isInternalRule() const
163 : : {
164 : 1506890 : return d_id != RewriteProofStatus::DSL
165 [ + + ][ + + ]: 1506890 : && d_id != RewriteProofStatus::THEORY_REWRITE;
166 : : }
167 : : };
168 : : /**
169 : : * Prove and store the proof of eq with internal form eqi in cdp if possible,
170 : : * return true if successful. Tries the basic utility and all recursion depths
171 : : * up to recLimit.
172 : : *
173 : : * @param cdp The object to add the proof of eq to.
174 : : * @param eq The equality we are trying to prove.
175 : : * @param eqi The internal version of the equality that may have been
176 : : * converted from eq using d_rdnc.
177 : : * @param recLimit The recursion limit for this call.
178 : : * @param stepLimit The step limit for this call.
179 : : * @param tmode Determines if/when to try THEORY_REWRITE.
180 : : * @return true if we successfully added a proof of (= a b) to cdp
181 : : */
182 : : bool proveEqStratified(CDProof* cdp,
183 : : const Node& eq,
184 : : const Node& eqi,
185 : : int64_t recLimit,
186 : : int64_t stepLimit,
187 : : TheoryRewriteMode tmode);
188 : : /**
189 : : * Prove and store the proof of eq with internal form eqi in cdp if possible,
190 : : * return true if successful. Tries a single recursion depth.
191 : : *
192 : : * @param cdp The object to add the proof of eq to.
193 : : * @param eqi The equality we are trying to prove.
194 : : * @param recLimit The recursion limit for this call.
195 : : * @param stepLimit The step limit for this call.
196 : : * @return true if we successfully added a proof of (= a b) to cdp
197 : : */
198 : : bool proveEq(CDProof* cdp,
199 : : const Node& eqi,
200 : : int64_t recLimit,
201 : : int64_t stepLimit);
202 : : /**
203 : : * Prove internal, which is the main entry point for proven an equality eqi.
204 : : * Returns the proof rule that was used to prove eqi, or
205 : : * RewriteProofStatus::FAIL if we failed to prove.
206 : : *
207 : : * In detail, this runs a strategy of builtin tactics and otherwise consults
208 : : * the rewrite rule database for the set of rewrite rules that match the
209 : : * left hand side of eqi.
210 : : *
211 : : * If this call is successful (i.e. the returned rule is not
212 : : * RewriteProofStatus::FAIL), the proven info for eqi is stored in
213 : : * d_pcache[eqi].
214 : : *
215 : : * Note this method depends on the current step and recursion limits
216 : : * d_currRecLimit/d_currStepLimit.
217 : : */
218 : : RewriteProofStatus proveInternal(const Node& eqi);
219 : : /** Prove internal via strategy, a helper method for above. */
220 : : RewriteProofStatus proveInternalViaStrategy(const Node& eqi);
221 : : /**
222 : : * Prove internal base eqi via DSL rule id.
223 : : *
224 : : * The purpose of this method is to prove or disprove eqi without using
225 : : * recursion. If so, we store the rule used for eqi in its proven info
226 : : * (d_pcache[eqi]). Notice that this method returns true if eqi is
227 : : * proven or *disproven*, where in the latter case proven info has d_id
228 : : * RewriteProofStatus::FAIL.
229 : : */
230 : : bool proveInternalBase(const Node& eqi, RewriteProofStatus& id);
231 : : /**
232 : : * Ensure proof for proven fact exists in cdp. This method is called on
233 : : * equalities eqi after they have been successfully proven by this class.
234 : : * Based on the information in proven infos, it constructs the formal
235 : : * proof of eqi, which may involve recursing to premises of rules that
236 : : * prove eqi. For details, see IV.B of Noetzli et al FMCAD 2022.
237 : : *
238 : : * @param cdp The proof to add the proof of eqi to
239 : : * @param eqi The proven equality
240 : : */
241 : : bool ensureProofInternal(CDProof* cdp, const Node& eqi);
242 : : /** Return the evaluation of n, which uses local caching. */
243 : : Node doEvaluate(const Node& n);
244 : : /**
245 : : * Return the flattening of n. For example, this returns (+ a b c) for
246 : : * (+ (+ a b) c). This method is used in the FLATTEN tactic.
247 : : */
248 : : Node doFlatten(const Node& n);
249 : : /**
250 : : * A notification that s is equal to n * { vars -> subs }. In this context,
251 : : * s is the current left hand side of a term we are trying to prove and n is
252 : : * the head of a rewrite rule.
253 : : *
254 : : * This method attempts to prove the current equality
255 : : *
256 : : * This function should return false if we do not wish to be notified of
257 : : * further matches, e.g. if we successfully show a rewrite rule suffices to
258 : : * prove the current equality d_target.
259 : : */
260 : : bool notifyMatch(const Node& s,
261 : : const Node& n,
262 : : std::vector<Node>& vars,
263 : : std::vector<Node>& subs);
264 : : /**
265 : : * Prove with rule, which attempts to prove the equality target using the
266 : : * DSL proof rule id, which may be a builtin rule or a user-provided rule.
267 : : *
268 : : * @param id The rule to consider, which may be a DSL rule given by r if DSL.
269 : : * @param target The equality to prove
270 : : * @param vars The variables (arguments) of the proof rule
271 : : * @param subs The substitution (instantiated arguments) of the proof rule
272 : : * @param doTrans If true, then if we are trying to prove (= t s)
273 : : * and the given rule proves (= t r), then we recursively try to prove
274 : : * (= r s).
275 : : * @param doFixedPoint If true, we consider the current rule applied to fixed
276 : : * point
277 : : * @param doRecurse Whether we should attempt to prove the rule when premises
278 : : * are required, by making a recursive call to proveInternal.
279 : : * @param r The DSL rule to consider if id is DSL.
280 : : */
281 : : bool proveWithRule(RewriteProofStatus id,
282 : : const Node& target,
283 : : const std::vector<Node>& vars,
284 : : const std::vector<Node>& subs,
285 : : bool doTrans,
286 : : bool doFixedPoint,
287 : : bool doRecurse,
288 : : ProofRewriteRule r = ProofRewriteRule::NONE);
289 : : /**
290 : : * Get conclusion of rewrite rule rpr under the current variable and
291 : : * substitution. Store the information in proven info pi. If doFixedPoint
292 : : * is true, apply the rule to fixed point.
293 : : */
294 : : Node getRuleConclusion(const RewriteProofRule& rpr,
295 : : const std::vector<Node>& vars,
296 : : const std::vector<Node>& subs,
297 : : ProvenInfo& pi,
298 : : bool doFixedPoint = false);
299 : : /**
300 : : * Rewrite concrete, which returns the result of rewriting n if it contains
301 : : * no abstract subterms, or n itself otherwise.
302 : : *
303 : : * This method is required since the algorithm in this class often invokes
304 : : * the rewriter as an oracle. We operate on terms with abstract subterms
305 : : * in this class, and these terms should not be passed to the rewriter,
306 : : * since the rewriter does not properly handle abstract subterms (for
307 : : * instance, the BV theory rewriter assumes that all children of BV operators
308 : : * have concrete bitwidths).
309 : : */
310 : : Node rewriteConcrete(const Node& n);
311 : : /** Notify class for matches */
312 : : RdpcMatchTrieNotify d_notify;
313 : : /**
314 : : * Basic utility for (user-independent) rewrite rule reconstruction. Handles
315 : : * cases that should always be reconstructed, e.g. EVALUATE, REFL,
316 : : * BETA_REDUCE.
317 : : */
318 : : BasicRewriteRCons d_trrc;
319 : : /** Node converter utility */
320 : : RewriteDbNodeConverter d_rdnc;
321 : : /** Pointer to rewrite database */
322 : : RewriteDb* d_db;
323 : : /** the evaluator utility */
324 : : theory::Evaluator d_eval;
325 : : /** The set of equalities we are currently proving, to avoid loops */
326 : : std::unordered_set<Node> d_currProving;
327 : : /** Cache for the proven status of formulas */
328 : : std::unordered_map<Node, ProvenInfo> d_pcache;
329 : : /** the evaluation cache */
330 : : std::unordered_map<Node, Node> d_evalCache;
331 : : /** common constants */
332 : : Node d_true;
333 : : Node d_false;
334 : : /** current target equality to prove */
335 : : Node d_target;
336 : : /** current recursion limit */
337 : : int64_t d_currRecLimit;
338 : : /** current step recursion limit */
339 : : uint64_t d_currStepLimit;
340 : : /** Did we fail due to a resource limit in the current run? */
341 : : bool d_currFailResource;
342 : : /** The mode for if/when to try theory rewrites */
343 : : rewriter::TheoryRewriteMode d_tmode;
344 : : /** current rule we are applying to fixed point */
345 : : ProofRewriteRule d_currFixedPointId;
346 : : /** current substitution from fixed point */
347 : : std::vector<Node> d_currFixedPointSubs;
348 : : /** current conclusion from fixed point */
349 : : Node d_currFixedPointConc;
350 : : /** Total number of rewrites we were asked to prove */
351 : : IntStat d_statTotalInputs;
352 : : /** Total number of rewrites we tried to prove internally */
353 : : IntStat d_statTotalAttempts;
354 : : /** Total number of rewrites we proved successfully */
355 : : IntStat d_statTotalInputSuccess;
356 : : /** Fixed point limit */
357 : : static size_t s_fixedPointLimit;
358 : : };
359 : :
360 : : } // namespace rewriter
361 : : } // namespace cvc5::internal
362 : :
363 : : #endif /* CVC5__THEORY__REWRITE_DB_PROOF_CONS__H */
|
