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 : : * Inference to proof conversion.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
16 : : #define CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
17 : :
18 : : #include <vector>
19 : :
20 : : #include "cvc5/cvc5_proof_rule.h"
21 : : #include "expr/node.h"
22 : : #include "expr/term_context.h"
23 : : #include "proof/conv_proof_generator.h"
24 : : #include "proof/proof_checker.h"
25 : : #include "proof/theory_proof_step_buffer.h"
26 : : #include "smt/env_obj.h"
27 : : #include "theory/builtin/proof_checker.h"
28 : : #include "theory/strings/infer_info.h"
29 : : #include "theory/strings/sequences_stats.h"
30 : : #include "theory/uf/proof_equality_engine.h"
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace strings {
35 : :
36 : : /**
37 : : * Converts between the strings-specific (untrustworthy) InferInfo class and
38 : : * information about how to construct a trustworthy proof step
39 : : * (ProofRule, children, args). It acts as a (lazy) proof generator where the
40 : : * former is registered via notifyFact and the latter is asked for in
41 : : * getProofFor, typically by the proof equality engine.
42 : : *
43 : : * The main (private) method of this class is convert below, which is
44 : : * called when we need to construct a proof node from an InferInfo.
45 : : *
46 : : * This class uses lazy proof reconstruction. Namely, the getProofFor method
47 : : * returns applications of the rule MACRO_STRING_INFERENCE, which store the
48 : : * arguments to the proof conversion routine "convert" below.
49 : : */
50 : : class InferProofCons : protected EnvObj, public ProofGenerator
51 : : {
52 : : typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>> NodeInferInfoMap;
53 : :
54 : : public:
55 : : InferProofCons(Env& env, context::Context* c);
56 : 40620 : ~InferProofCons() {}
57 : : /**
58 : : * This is called to notify that ii is an inference that may need a proof
59 : : * in the future.
60 : : *
61 : : * In detail, this class should be prepared to respond to a call to:
62 : : * getProofFor(ii.d_conc)
63 : : * in the remainder of the SAT context. This method copies ii and stores it
64 : : * in the context-dependent map d_lazyFactMap below.
65 : : *
66 : : * This is used for lazy proof construction, where proofs are constructed
67 : : * only for facts that are explained.
68 : : */
69 : : void notifyFact(const InferInfo& ii);
70 : : /**
71 : : * Same as above, but always overwrites. This is used for lemmas and
72 : : * conflicts, which do not necessarily have unique conclusions.
73 : : */
74 : : void notifyLemma(const InferInfo& ii);
75 : :
76 : : /**
77 : : * This returns the proof for fact. This is required for using this class as
78 : : * a lazy proof generator.
79 : : *
80 : : * It should be the case that a call was made to notifyFact(ii) where
81 : : * ii.d_conc is fact in this SAT context.
82 : : *
83 : : * This returns the appropriate application of MACRO_STRING_INFERENCE so that
84 : : * it can be reconstructed if necessary during proof post-processing.
85 : : */
86 : : std::shared_ptr<ProofNode> getProofFor(Node fact) override;
87 : : /** Identify this generator (for debugging, etc..) */
88 : : virtual std::string identify() const override;
89 : : /**
90 : : * Pack arguments of a MACRO_STRING_INFERENCE rule application in args. This
91 : : * proof rule stores the arguments to the convert method of this class below.
92 : : */
93 : : static void packArgs(Node conc,
94 : : InferenceId infer,
95 : : bool isRev,
96 : : const std::vector<Node>& exp,
97 : : std::vector<Node>& args);
98 : : /**
99 : : * Inverse of the above method, which recovers the arguments that were packed
100 : : * into the vector args.
101 : : */
102 : : static bool unpackArgs(const std::vector<Node>& args,
103 : : Node& conc,
104 : : InferenceId& infer,
105 : : bool& isRev,
106 : : std::vector<Node>& exp);
107 : :
108 : : /** convert
109 : : *
110 : : * Add proof of running convert on the given arguments to CDProof pf. This is
111 : : * called lazily during proof post-processing.
112 : : *
113 : : * This method is called when the theory of strings makes an inference
114 : : * described by an InferInfo, whose fields are given by the first four
115 : : * arguments of this method.
116 : : *
117 : : * @param env Reference to the environment.
118 : : * @param infer The inference id.
119 : : * @param isRev Whether this was the reverse form of the inference id.
120 : : * @param conc The conclusion of the inference.
121 : : * @param exp The explanation of the inference.
122 : : * @param pf The proof to add to.
123 : : * @return true if we successfully added a proof of conc to pf, whose free
124 : : * assumptions are a subset of exp.
125 : : */
126 : : static bool convert(Env& env,
127 : : InferenceId infer,
128 : : bool isRev,
129 : : Node conc,
130 : : const std::vector<Node>& exp,
131 : : CDProof* pf);
132 : :
133 : : private:
134 : : /**
135 : : * Convert length proof. If this method returns true, it adds proof step(s)
136 : : * to the buffer psb that conclude lenReq from premises lenExp.
137 : : */
138 : : static bool convertLengthPf(Node lenReq,
139 : : const std::vector<Node>& lenExp,
140 : : TheoryProofStepBuffer& psb);
141 : : /**
142 : : * Helper method, adds the proof of (TRANS eqa eqb) into the proof step
143 : : * buffer psb, where eqa and eqb are flipped as needed. Returns the
144 : : * conclusion, or null if we were not able to construct a TRANS step.
145 : : */
146 : : static Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb);
147 : : /**
148 : : * Helper method for convert. Concludes tgt from src, using AND_ELIM
149 : : * if necessary.
150 : : * @param nm Pointer to the node manager.
151 : : * @param src The source predicate, assumed to have a proof in psb.
152 : : * @param tgt The target predicate.
153 : : * @param psb The proof step buffer.
154 : : * @return true if we guarantee psb has a proof of tgt.
155 : : */
156 : : static bool convertAndElim(NodeManager* nm,
157 : : const Node& src,
158 : : const Node& tgt,
159 : : TheoryProofStepBuffer& psb);
160 : : /**
161 : : * Helper method for convert.
162 : : * Convert core substitution. This is used to apply a
163 : : * substitution given by exp to src. The indices determine
164 : : * which contexts to apply the substitution to apply, based
165 : : * on the definition of StringCoreTermContext.
166 : : * We add a proof of src = src' to pf, where src' is the result
167 : : * of applying the substitution to src'.
168 : : * If proveSrc is false, we add a proof of src' given free
169 : : * assumption src to psb. Otherwise we add a proof of src given
170 : : * free assumption src' to psb.
171 : : * @param env Reference to the environment
172 : : * @param pf Pointer to proof.
173 : : * @param psb Reference to proof step buffer.
174 : : * @param src The predicate to apply the substitution to.
175 : : * @param exp A list of equalities defining the substitution.
176 : : * @param minIndex The minimum term context value to consider.
177 : : * @param maxIndex The maximum term context value to consider.
178 : : * @param proveSrc Whether we prove src from src' or vice versa.
179 : : * @return The result of applying the substituion to src.
180 : : */
181 : : static Node convertCoreSubs(Env& env,
182 : : CDProof* pf,
183 : : TheoryProofStepBuffer& psb,
184 : : const Node& src,
185 : : const std::vector<Node>& exp,
186 : : size_t minIndex = 0,
187 : : size_t maxIndex = 0,
188 : : bool proveSrc = false);
189 : : /**
190 : : * This method ensures that constants in eq have been spliced to match
191 : : * the requirements of the given proof rule (possibly in its reverse form).
192 : : * If necessary, we rewrite eq to a new equality eqr and add a proof of eqr
193 : : * from eq as a step to psb and return eqr. Otherwise, eq is returned.
194 : : * @param psb Reference to proof step buffer.
195 : : * @param rule The rule whose premise is eq.
196 : : * @param eq The equality to ensure constants are spliced in.
197 : : * @param conc The target conclusion of the rule, used if rule is
198 : : * CONCAT_UNIFY.
199 : : * @param isRev Whether rule is being applied in the reverse direction.
200 : : * @return The result of splicing the appropriate constants (if any) in eq.
201 : : */
202 : : static Node spliceConstants(ProofRule rule,
203 : : TheoryProofStepBuffer& psb,
204 : : const Node& eq,
205 : : const Node& conc,
206 : : bool isRev);
207 : : /**
208 : : * Prove b assuming a, return true if successful.
209 : : * This method relies on applying MACRO_SR_PRED_TRANSFORM to prove a rewrites
210 : : * to b. To make things more robust, we additionally look for subterms where
211 : : * a and b differ, and prove these separately. This often corresponds to
212 : : * showing the equivalence between two skolems, e.g. where b contains a
213 : : * skolem for an unrewritten term and a contains a skolem for a rewritten
214 : : * term.
215 : : * @param a The first predicate.
216 : : * @param b The second predicate.
217 : : * @param psb Reference to proof step buffer.
218 : : * @return true if we successfully add a step proving b via
219 : : * MACRO_SR_PRED_TRANSFORM from a.
220 : : */
221 : : static bool applyPredTransformConversion(const Node& a,
222 : : const Node& b,
223 : : TheoryProofStepBuffer& psb);
224 : : /** The lazy fact map */
225 : : NodeInferInfoMap d_lazyFactMap;
226 : : };
227 : :
228 : : } // namespace strings
229 : : } // namespace theory
230 : : } // namespace cvc5::internal
231 : :
232 : : #endif /* CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H */
|
