Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Solver for extended functions of theory of strings.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__STRINGS__EXTF_SOLVER_H
19 : : #define CVC5__THEORY__STRINGS__EXTF_SOLVER_H
20 : :
21 : : #include <map>
22 : : #include <vector>
23 : :
24 : : #include "context/cdo.h"
25 : : #include "expr/node.h"
26 : : #include "smt/env_obj.h"
27 : : #include "theory/ext_theory.h"
28 : : #include "theory/strings/base_solver.h"
29 : : #include "theory/strings/core_solver.h"
30 : : #include "theory/strings/inference_manager.h"
31 : : #include "theory/strings/sequences_stats.h"
32 : : #include "theory/strings/skolem_cache.h"
33 : : #include "theory/strings/solver_state.h"
34 : : #include "theory/strings/strings_rewriter.h"
35 : : #include "theory/strings/theory_strings_preprocess.h"
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace strings {
40 : :
41 : : /**
42 : : * Non-static information about an extended function t. This information is
43 : : * constructed and used during the check extended function evaluation
44 : : * inference schema.
45 : : *
46 : : * In the following, we refer to the "context-dependent simplified form"
47 : : * of a term t to be the result of rewriting t * sigma, where sigma is a
48 : : * derivable substitution in the current context. For example, the
49 : : * context-depdendent simplified form of contains( x++y, "a" ) given
50 : : * sigma = { x -> "" } is contains(y,"a").
51 : : */
52 : : class ExtfInfoTmp
53 : : {
54 : : public:
55 : 844928 : ExtfInfoTmp() : d_modelActive(true) {}
56 : : /**
57 : : * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s )
58 : : * (resp. ~contains( t, s )) holds in the current context. The vector
59 : : * d_ctnFrom is the explanation for why this holds. For example,
60 : : * if d_ctn[false][i] is "A", then d_ctnFrom[false][i] might be
61 : : * t = x ++ y AND x = "" AND y = "B".
62 : : */
63 : : std::map<bool, std::vector<Node> > d_ctn;
64 : : std::map<bool, std::vector<Node> > d_ctnFrom;
65 : : /**
66 : : * The constant that t is entailed to be equal to, or null if none exist.
67 : : */
68 : : Node d_const;
69 : : /**
70 : : * The explanation for why t is equal to its context-dependent simplified
71 : : * form.
72 : : */
73 : : std::vector<Node> d_initExp;
74 : : std::vector<Node> d_exp;
75 : : /** This flag is false if t is reduced in the model. */
76 : : bool d_modelActive;
77 : : };
78 : :
79 : : /**
80 : : * Extended function solver for the theory of strings. This manages extended
81 : : * functions for the theory of strings using a combination of context-dependent
82 : : * simplification (Reynolds et al CAV 2017) and lazy reductions.
83 : : */
84 : : class ExtfSolver : public InferSideEffectProcess, protected EnvObj
85 : : {
86 : : typedef context::CDHashSet<Node> NodeSet;
87 : :
88 : : public:
89 : : ExtfSolver(Env& env,
90 : : SolverState& s,
91 : : InferenceManager& im,
92 : : TermRegistry& tr,
93 : : StringsRewriter& rewriter,
94 : : BaseSolver& bs,
95 : : CoreSolver& cs,
96 : : ExtTheory& et,
97 : : SequencesStatistics& statistics);
98 : : ~ExtfSolver();
99 : : /** check extended functions evaluation
100 : : *
101 : : * This applies "context-dependent simplification" for all active extended
102 : : * function terms in this SAT context. This infers facts of the form:
103 : : * x = c => f( t1 ... tn ) = c'
104 : : * where the rewritten form of f( t1...tn ) { x |-> c } is c', and x = c
105 : : * is a (tuple of) equalities that are asserted in this SAT context, and
106 : : * f( t1 ... tn ) is a term from this SAT context.
107 : : *
108 : : * For more details, this is steps 4 when effort=0 and step 6 when
109 : : * effort=1 from Strategy 1 in Reynolds et al, "Scaling up DPLL(T) String
110 : : * Solvers using Context-Dependent Simplification", CAV 2017. When called with
111 : : * effort=3, we apply context-dependent simplification based on model values.
112 : : */
113 : : void checkExtfEval(int effort);
114 : : /** check extended function reductions
115 : : *
116 : : * This adds "reduction" lemmas for each active extended function in this SAT
117 : : * context. These are generally lemmas of the form:
118 : : * F[t1...tn,k] ^ f( t1 ... tn ) = k
119 : : * where f( t1 ... tn ) is an active extended function, k is a fresh constant
120 : : * and F is a formula that constrains k based on the definition of f.
121 : : *
122 : : * For more details, this is step 7 from Strategy 1 in Reynolds et al,
123 : : * CAV 2017. We stratify this in practice based on the effort level,
124 : : * where for instance, we reduce negatively asserted str.contains only
125 : : * at LAST_CALL effort. For more information see discussion of "model-based
126 : : * reductions" in Reynolds et al CAV 2022.
127 : : */
128 : : void checkExtfReductions(Theory::Effort e);
129 : : /**
130 : : * Check for extended functions that should be applied eagerly. This is
131 : : * called earlier in the search strategy of strings, in particular before
132 : : * the core equality reasoning is done.
133 : : */
134 : : void checkExtfReductionsEager();
135 : : /** get preprocess module */
136 : : StringsPreprocess* getPreprocess() { return &d_preproc; }
137 : :
138 : : /**
139 : : * Get the current substitution for term n.
140 : : *
141 : : * This method returns a term that n is currently equal to in the current
142 : : * context. It updates exp to contain an explanation of why it is currently
143 : : * equal to that term.
144 : : *
145 : : * The argument effort determines what kind of term to return, either
146 : : * a constant in the equivalence class of n (effort=0), the normal form of
147 : : * n (effort=1,2) or the model value of n (effort>=3). The latter is only
148 : : * valid at LAST_CALL effort. If a term of the above form cannot be returned,
149 : : * then n itself is returned.
150 : : */
151 : : Node getCurrentSubstitutionFor(int effort, Node n, std::vector<Node>& exp);
152 : : /** get mapping from extended functions to their information
153 : : *
154 : : * This information is valid during a full effort check after a call to
155 : : * checkExtfEval.
156 : : */
157 : : const std::map<Node, ExtfInfoTmp>& getInfo() const;
158 : : //---------------------------------- information about ExtTheory
159 : : /** Are there any active extended functions? */
160 : : bool hasExtendedFunctions() const;
161 : : /**
162 : : * Get the function applications of kind k that are active in the current
163 : : * context (see ExtTheory::getActive).
164 : : */
165 : : std::vector<Node> getActive(Kind k) const;
166 : : /**
167 : : * Return true if n is active in the model. If this method returns false,
168 : : * then n is already satisfied in the model (its value in the model is
169 : : * the same as its representative in the equality engine).
170 : : */
171 : : bool isActiveInModel(Node n) const;
172 : : /**
173 : : * @return The relevant active terms. This method retrieves the relevant
174 : : * terms from the term registry and filters out inactive terms.
175 : : *
176 : : * Note that the set of active terms is not a subset of the relevant terms
177 : : * since active terms may include preregistered terms that don't appear
178 : : * in any current assertions.
179 : : */
180 : : std::vector<Node> getRelevantActive() const;
181 : : //---------------------------------- end information about ExtTheory
182 : : /**
183 : : * Print the relevant information regarding why we have a model, return as a
184 : : * string.
185 : : */
186 : : std::string debugPrintModel();
187 : :
188 : : /**
189 : : * Is extended function (or regular expression membership) reduced? Note that
190 : : * if n has Boolean type, our reductions are dependent upon the polarity of n,
191 : : * in which case n may be the negation of an extended function. For
192 : : * example, (not (str.in_re x R)) indicates that we have reduced
193 : : * (str.in_re x R) based on its negative unfolding.
194 : : */
195 : : bool isReduced(const Node& n) const;
196 : : /**
197 : : * Mark that extended function (or regular expression membership) n has been
198 : : * reduced. Like above, n could be a negation of an extended function of
199 : : * Boolean type.
200 : : */
201 : : void markReduced(const Node& n);
202 : :
203 : : /** Called when ii is ready to be processed as a fact */
204 : : void processFact(InferInfo& ii, ProofGenerator*& pg) override;
205 : : /** Called when ii is ready to be processed as a lemma */
206 : : TrustNode processLemma(InferInfo& ii, LemmaProperty& p) override;
207 : :
208 : : private:
209 : : /**
210 : : * Helper method for checkExtfReductions / maybeHasCandidateModel, returns
211 : : * true if a reduction lemma was sent if doSend = true, or would have been
212 : : * sent if doSend = false.
213 : : */
214 : : bool checkExtfReductionsInternal(int effort, bool doSend);
215 : : /**
216 : : * Determines if n should be reduced based on the effort level.
217 : : *
218 : : * @param effort the effort level
219 : : * @param n the term to reduce
220 : : * @param pol polarity of n, where 1 true, -1 false, 0 neither
221 : : */
222 : : bool shouldDoReduction(int effort, Node n, int pol);
223 : : /** do reduction
224 : : *
225 : : * This is called when an extended function application n is not able to be
226 : : * simplified by context-depdendent simplification, and we are resorting to
227 : : * expanding n to its full semantics via a reduction. This method returns
228 : : * true if it successfully reduced n by some reduction. If so, it either
229 : : * caches that the reduction lemma was sent, or marks n as reduced in this
230 : : * SAT-context. The argument effort has the same meaning as in
231 : : * checkExtfReductions.
232 : : *
233 : : * @param n the term to reduce
234 : : * @param pol polarity of n, where 1 true, -1 false, 0 neither
235 : : */
236 : : void doReduction(Node n, int pol);
237 : : /** check extended function inferences
238 : : *
239 : : * This function makes additional inferences for n that do not contribute
240 : : * to its reduction, but may help show a refutation.
241 : : *
242 : : * This function is called when the context-depdendent simplified form of
243 : : * n is nr. The argument "in" is the information object for n. The argument
244 : : * "effort" has the same meaning as the effort argument of checkExtfEval.
245 : : */
246 : : void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort);
247 : : /** The solver state object */
248 : : SolverState& d_state;
249 : : /** The (custom) output channel of the theory of strings */
250 : : InferenceManager& d_im;
251 : : /** Reference to the term registry of theory of strings */
252 : : TermRegistry& d_termReg;
253 : : /** The theory rewriter for this theory. */
254 : : StringsRewriter& d_rewriter;
255 : : /** reference to the base solver, used for certain queries */
256 : : BaseSolver& d_bsolver;
257 : : /** reference to the core solver, used for certain queries */
258 : : CoreSolver& d_csolver;
259 : : /** the extended theory object for the theory of strings */
260 : : ExtTheory& d_extt;
261 : : /** Reference to the statistics for the theory of strings/sequences. */
262 : : SequencesStatistics& d_statistics;
263 : : /** preprocessing utility, for performing strings reductions */
264 : : StringsPreprocess d_preproc;
265 : : /** Common constants */
266 : : Node d_true;
267 : : Node d_false;
268 : : /** Empty vector */
269 : : std::vector<Node> d_emptyVec;
270 : : /** map extended functions to the above information */
271 : : std::map<Node, ExtfInfoTmp> d_extfInfoTmp;
272 : : /** map from reduced extended functions to their original */
273 : : std::map<Node, Node> d_extfToOrig;
274 : : /** any non-reduced extended functions exist? */
275 : : context::CDO<bool> d_hasExtf;
276 : : /** extended functions inferences cache */
277 : : NodeSet d_extfInferCache;
278 : : /** The set of extended functions we have sent reduction lemmas for */
279 : : NodeSet d_reduced;
280 : : /** Map from lemmas to the terms they justify the reduction of */
281 : : std::map<Node, Node> d_reductionWaitingMap;
282 : : };
283 : :
284 : : /** An extended theory callback */
285 : : class StringsExtfCallback : public ExtTheoryCallback
286 : : {
287 : : public:
288 : 50196 : StringsExtfCallback() : d_esolver(nullptr) {}
289 : : /**
290 : : * Get current substitution based on the underlying extended function
291 : : * solver.
292 : : */
293 : : bool getCurrentSubstitution(int effort,
294 : : const std::vector<Node>& vars,
295 : : std::vector<Node>& subs,
296 : : std::map<Node, std::vector<Node> >& exp) override;
297 : : /** The extended function solver */
298 : : ExtfSolver* d_esolver;
299 : : };
300 : :
301 : : } // namespace strings
302 : : } // namespace theory
303 : : } // namespace cvc5::internal
304 : :
305 : : #endif /* CVC5__THEORY__STRINGS__EXTF_SOLVER_H */
|
