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