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