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 : : * Customized inference manager for the theory of strings.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
16 : : #define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
17 : :
18 : : #include <map>
19 : : #include <vector>
20 : :
21 : : #include "context/cdhashset.h"
22 : : #include "context/context.h"
23 : : #include "expr/node.h"
24 : : #include "proof/proof_node_manager.h"
25 : : #include "theory/ext_theory.h"
26 : : #include "theory/inference_manager_buffered.h"
27 : : #include "theory/output_channel.h"
28 : : #include "theory/strings/infer_info.h"
29 : : #include "theory/strings/infer_proof_cons.h"
30 : : #include "theory/strings/sequences_stats.h"
31 : : #include "theory/strings/solver_state.h"
32 : : #include "theory/strings/term_registry.h"
33 : : #include "theory/theory_inference_manager.h"
34 : : #include "theory/uf/equality_engine.h"
35 : :
36 : : namespace cvc5::internal {
37 : : namespace theory {
38 : : namespace strings {
39 : :
40 : : /** Inference Manager
41 : : *
42 : : * The purpose of this class is to process inference steps for strategies
43 : : * in the theory of strings.
44 : : *
45 : : * In particular, inferences are given to this class via calls to functions:
46 : : *
47 : : * sendInternalInference, sendInference, sendSplit
48 : : *
49 : : * This class decides how the conclusion of these calls will be processed.
50 : : * It primarily has to decide whether the conclusions will be processed:
51 : : *
52 : : * (1) Internally in the strings solver, via calls to equality engine's
53 : : * assertLiteral and assertPredicate commands. We refer to these literals as
54 : : * "facts",
55 : : * (2) Externally on the output channel of theory of strings as "lemmas",
56 : : * (3) External on the output channel as "conflicts" (when a conclusion of an
57 : : * inference is false).
58 : : *
59 : : * It buffers facts and lemmas in vectors d_pending and d_pending_lem
60 : : * respectively.
61 : : *
62 : : * When applicable, facts can be flushed to the equality engine via a call to
63 : : * doPendingFacts, and lemmas can be flushed to the output channel via a call
64 : : * to doPendingLemmas.
65 : : *
66 : : * It also manages other kinds of interaction with the output channel of the
67 : : * theory of strings, e.g. sendPhaseRequirement, setModelUnsound, and
68 : : * with the extended theory object e.g. markCongruent.
69 : : */
70 : : class InferenceManager : public InferSideEffectProcess,
71 : : public InferenceManagerBuffered
72 : : {
73 : : typedef context::CDHashSet<Node> NodeSet;
74 : : typedef context::CDHashMap<Node, Node> NodeNodeMap;
75 : : friend class InferInfo;
76 : :
77 : : public:
78 : : InferenceManager(Env& env,
79 : : Theory& t,
80 : : SolverState& s,
81 : : TermRegistry& tr,
82 : : ExtTheory& e,
83 : : SequencesStatistics& statistics);
84 : 49636 : ~InferenceManager() {}
85 : :
86 : : /**
87 : : * Do pending method. This processes all pending facts, lemmas and pending
88 : : * phase requests based on the policy of this manager. This means that
89 : : * we process the pending facts first and abort if in conflict. Otherwise, we
90 : : * process the pending lemmas and then the pending phase requirements.
91 : : * Notice that we process the pending lemmas even if there were facts.
92 : : */
93 : : void doPending();
94 : :
95 : : /** send internal inferences
96 : : *
97 : : * This is called when we have inferred exp => conc, where exp is a set
98 : : * of equalities and disequalities that hold in the current equality engine.
99 : : * This method adds equalities and disequalities ~( s = t ) via
100 : : * sendInference such that both s and t are either constants or terms
101 : : * that already occur in the equality engine, and ~( s = t ) is a consequence
102 : : * of conc. This function can be seen as a "conservative" version of
103 : : * sendInference below in that it does not introduce any new non-constant
104 : : * terms to the state.
105 : : *
106 : : * The argument infer identifies the reason for the inference.
107 : : * This is used for debugging and statistics purposes.
108 : : *
109 : : * Return true if the inference is complete, in the sense that we infer
110 : : * inferences that are equivalent to conc. This returns false e.g. if conc
111 : : * (or one of its conjuncts if it is a conjunction) was not inferred due
112 : : * to the criteria mentioned above.
113 : : */
114 : : bool sendInternalInference(std::vector<Node>& exp,
115 : : Node conc,
116 : : InferenceId infer);
117 : :
118 : : /** send inference
119 : : *
120 : : * This function should be called when exp => eq. The set exp
121 : : * contains literals that are explainable, i.e. those that hold in the
122 : : * equality engine of the theory of strings. On the other hand, the set
123 : : * noExplain contains nodes that are not explainable by the theory of strings.
124 : : * This method may call sendLemma or otherwise add a InferInfo to d_pending,
125 : : * indicating a fact should be asserted to the equality engine. Overall, the
126 : : * result of this method is one of the following:
127 : : *
128 : : * [1] (No-op) Do nothing if eq is equivalent to true,
129 : : *
130 : : * [2] (Infer) Indicate that eq should be added to the equality engine of this
131 : : * class with explanation exp, where exp is a set of literals that currently
132 : : * hold in the equality engine. We add this to the pending vector d_pending.
133 : : *
134 : : * [3] (Lemma) Indicate that the lemma
135 : : * ( EXPLAIN(exp \ noExplain) ^ noExplain ) => eq
136 : : * should be sent on the output channel of the theory of strings, where
137 : : * EXPLAIN returns the explanation of the node in exp in terms of the literals
138 : : * asserted to the theory of strings, as computed by the equality engine.
139 : : * This is also added to a pending vector, d_pendingLem.
140 : : *
141 : : * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
142 : : * channel of the theory of strings.
143 : : *
144 : : * Determining which case to apply depends on the form of eq and whether
145 : : * noExplain is empty. In particular, lemmas must be used whenever noExplain
146 : : * is non-empty, conflicts are used when noExplain is empty and eq is false.
147 : : *
148 : : * @param exp The explanation of eq.
149 : : * @param noExplain The subset of exp that cannot be explained by the
150 : : * equality engine. This may impact whether we are processing this call as a
151 : : * fact or as a lemma.
152 : : * @param eq The conclusion.
153 : : * @param infer Identifies the reason for inference, used for
154 : : * debugging. This updates the statistics about the number of inferences made
155 : : * of each type.
156 : : * @param isRev Whether this is the "reverse variant" of the inference, which
157 : : * is used as a hint for proof reconstruction.
158 : : * @param asLemma If true, then this method will send a lemma instead
159 : : * of a fact whenever applicable.
160 : : * @return true if the inference was not trivial (e.g. its conclusion did
161 : : * not rewrite to true).
162 : : */
163 : : bool sendInference(const std::vector<Node>& exp,
164 : : const std::vector<Node>& noExplain,
165 : : Node eq,
166 : : InferenceId infer,
167 : : bool isRev = false,
168 : : bool asLemma = false);
169 : : /** same as above, but where noExplain is empty */
170 : : bool sendInference(const std::vector<Node>& exp,
171 : : Node eq,
172 : : InferenceId infer,
173 : : bool isRev = false,
174 : : bool asLemma = false);
175 : :
176 : : /** Send inference
177 : : *
178 : : * This implements the above methods for the InferInfo object. It is called
179 : : * by the methods above.
180 : : *
181 : : * The inference info ii should have a rewritten conclusion and should not be
182 : : * trivial (InferInfo::isTrivial). It is the responsibility of the caller to
183 : : * ensure this.
184 : : *
185 : : * If the flag asLemma is true, then this method will send a lemma instead
186 : : * of a fact whenever applicable.
187 : : */
188 : : void sendInference(InferInfo& ii, bool asLemma = false);
189 : : /** Send split
190 : : *
191 : : * This requests that ( a = b V a != b ) is sent on the output channel as a
192 : : * lemma. We additionally request a phase requirement for the equality a=b
193 : : * with polarity preq.
194 : : *
195 : : * The argument infer identifies the reason for inference, used for
196 : : * debugging. This updates the statistics about the number of
197 : : * inferences made of each type.
198 : : *
199 : : * This method returns true if the split was non-trivial, and false
200 : : * otherwise. A split is trivial if a=b rewrites to a constant.
201 : : */
202 : : bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true);
203 : :
204 : : //----------------------------constructing antecedants
205 : : /**
206 : : * Adds equality a = b to the vector exp if a and b are distinct terms. It
207 : : * must be the case that areEqual( a, b ) holds in this context.
208 : : */
209 : : void addToExplanation(Node a, Node b, std::vector<Node>& exp) const;
210 : : /** Adds lit to the vector exp if it is non-null */
211 : : void addToExplanation(Node lit, std::vector<Node>& exp) const;
212 : : //----------------------------end constructing antecedants
213 : : /**
214 : : * Have we processed an inference during this call to check? In particular,
215 : : * this returns true if we have a pending fact or lemma, or have encountered
216 : : * a conflict.
217 : : */
218 : : bool hasProcessed() const;
219 : :
220 : : // ------------------------------------------------- extended theory
221 : : /**
222 : : * Mark that extended function is inactive. If contextDepend is true,
223 : : * then this mark is SAT-context dependent, otherwise it is user-context
224 : : * dependent (see ExtTheory::markInactive).
225 : : */
226 : : void markInactive(Node n, ExtReducedId id, bool contextDepend = true);
227 : : // ------------------------------------------------- end extended theory
228 : :
229 : : /**
230 : : * Called when ii is ready to be processed as a conflict. This makes a
231 : : * trusted node whose generator is the underlying proof equality engine
232 : : * (if it exists), and sends it on the output channel.
233 : : */
234 : : void processConflict(const InferInfo& ii);
235 : : /** Called when ii is ready to be processed as a fact */
236 : : void processFact(InferInfo& ii, ProofGenerator*& pg) override;
237 : : /** Called when ii is ready to be processed as a lemma */
238 : : TrustNode processLemma(InferInfo& ii, LemmaProperty& p) override;
239 : :
240 : : private:
241 : : /**
242 : : * min prefix explain
243 : : *
244 : : * @param x A string term
245 : : * @param prefix The prefix (suffix).
246 : : * @param assumptions The set of assumptions we are minimizing
247 : : * @param emap The explanation map for assumptions (getExplanationMap).
248 : : * @param isSuf Whether prefix denotes a suffix
249 : : * @return A subset of assumptions that imply x does not have the given
250 : : * prefix.
251 : : */
252 : : Node mkPrefixExplainMin(Node x,
253 : : Node prefix,
254 : : const std::vector<TNode>& assumptions,
255 : : const std::map<TNode, TNode>& emap,
256 : : bool isSuf = false);
257 : : /**
258 : : * Returns a mapping from terms to equalities, where t -> E if E is an
259 : : * equality of the form (= t *) or (= * t) from assumptions.
260 : : */
261 : : static std::map<TNode, TNode> getExplanationMap(
262 : : const std::vector<TNode>& assumptions);
263 : : /** Reference to the solver state of the theory of strings. */
264 : : SolverState& d_state;
265 : : /** Reference to the term registry of theory of strings */
266 : : TermRegistry& d_termReg;
267 : : /** the extended theory object for the theory of strings */
268 : : ExtTheory& d_extt;
269 : : /** Reference to the statistics for the theory of strings/sequences. */
270 : : SequencesStatistics& d_statistics;
271 : : /** Conversion from inferences to proofs for facts */
272 : : std::unique_ptr<InferProofCons> d_ipc;
273 : : /**
274 : : * Conversion from inferences to proofs for lemmas and conflicts. This is
275 : : * separate from the above proof generator to avoid rare cases where the
276 : : * conclusion of a lemma is a duplicate of the conclusion of another lemma,
277 : : * or is a fact in the current equality engine.
278 : : */
279 : : std::unique_ptr<InferProofCons> d_ipcl;
280 : : /** Common constants */
281 : : Node d_true;
282 : : Node d_false;
283 : : Node d_zero;
284 : : Node d_one;
285 : : };
286 : :
287 : : } // namespace strings
288 : : } // namespace theory
289 : : } // namespace cvc5::internal
290 : :
291 : : #endif
|
