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 : : * Theory of strings.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_H
16 : : #define CVC5__THEORY__STRINGS__THEORY_STRINGS_H
17 : :
18 : : #include <climits>
19 : : #include <deque>
20 : :
21 : : #include "context/cdhashset.h"
22 : : #include "context/cdlist.h"
23 : : #include "expr/node_trie.h"
24 : : #include "proof/trust_proof_generator.h"
25 : : #include "theory/care_pair_argument_callback.h"
26 : : #include "theory/ext_theory.h"
27 : : #include "theory/strings/array_solver.h"
28 : : #include "theory/strings/base_solver.h"
29 : : #include "theory/strings/code_point_solver.h"
30 : : #include "theory/strings/core_solver.h"
31 : : #include "theory/strings/eager_solver.h"
32 : : #include "theory/strings/extf_solver.h"
33 : : #include "theory/strings/infer_info.h"
34 : : #include "theory/strings/inference_manager.h"
35 : : #include "theory/strings/model_cons_default.h"
36 : : #include "theory/strings/normal_form.h"
37 : : #include "theory/strings/proof_checker.h"
38 : : #include "theory/strings/regexp_elim.h"
39 : : #include "theory/strings/regexp_operation.h"
40 : : #include "theory/strings/regexp_solver.h"
41 : : #include "theory/strings/sequences_stats.h"
42 : : #include "theory/strings/solver_state.h"
43 : : #include "theory/strings/strategy.h"
44 : : #include "theory/strings/strings_fmf.h"
45 : : #include "theory/strings/strings_rewriter.h"
46 : : #include "theory/strings/term_registry.h"
47 : : #include "theory/theory.h"
48 : : #include "theory/uf/equality_engine.h"
49 : :
50 : : namespace cvc5::internal {
51 : : namespace theory {
52 : : namespace strings {
53 : :
54 : : /**
55 : : * A theory solver for strings. At a high level, the solver implements
56 : : * techniques described in:
57 : : * - Liang et al, CAV 2014,
58 : : * - Reynolds et al, CAV 2017,
59 : : * - Reynolds et al, IJCAR 2020.
60 : : * Its rewriter is described in:
61 : : * - Reynolds et al, CAV 2019.
62 : : */
63 : : class TheoryStrings : public Theory
64 : : {
65 : : friend class InferenceManager;
66 : : typedef context::CDHashSet<Node> NodeSet;
67 : : typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
68 : :
69 : : public:
70 : : TheoryStrings(Env& env, OutputChannel& out, Valuation valuation);
71 : : ~TheoryStrings();
72 : : //--------------------------------- initialization
73 : : /** get the official theory rewriter of this theory */
74 : : TheoryRewriter* getTheoryRewriter() override;
75 : : /** get the proof checker of this theory */
76 : : ProofRuleChecker* getProofChecker() override;
77 : : /**
78 : : * Returns true if we need an equality engine. If so, we initialize the
79 : : * information regarding how it should be setup. For details, see the
80 : : * documentation in Theory::needsEqualityEngine.
81 : : */
82 : : bool needsEqualityEngine(EeSetupInfo& esi) override;
83 : : /** finish initialization */
84 : : void finishInit() override;
85 : : //--------------------------------- end initialization
86 : : /** Identify this theory */
87 : : std::string identify() const override;
88 : : /** Explain */
89 : : TrustNode explain(TNode literal) override;
90 : : /** presolve */
91 : : void presolve() override;
92 : : /** preregister term */
93 : : void preRegisterTerm(TNode n) override;
94 : : //--------------------------------- standard check
95 : : /** Do we need a check call at last call effort? */
96 : : bool needsCheckLastEffort() override;
97 : : bool preNotifyFact(TNode atom,
98 : : bool pol,
99 : : TNode fact,
100 : : bool isPrereg,
101 : : bool isInternal) override;
102 : : void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
103 : : /** Post-check, called after the fact queue of the theory is processed. */
104 : : void postCheck(Effort level) override;
105 : : //--------------------------------- end standard check
106 : : /** propagate method */
107 : : bool propagateLit(TNode literal);
108 : : /** Conflict when merging two constants */
109 : : void conflict(TNode a, TNode b);
110 : : /** called when a new equivalence class is created */
111 : : void eqNotifyNewClass(TNode t);
112 : : /** Called just after the merge of two equivalence classes */
113 : : void eqNotifyMerge(TNode t1, TNode t2);
114 : : /** preprocess rewrite */
115 : : TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
116 : : TrustNode ppStaticRewrite(TNode atom) override;
117 : : /** Collect model values in m based on the relevant terms given by termSet */
118 : : bool collectModelValues(TheoryModel* m,
119 : : const std::set<Node>& termSet) override;
120 : :
121 : : private:
122 : : /** NotifyClass for equality engine */
123 : : class NotifyClass : public eq::EqualityEngineNotify
124 : : {
125 : : public:
126 : 28896 : NotifyClass(TheoryStrings& ts) : d_str(ts) {}
127 : 917939 : bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
128 : : {
129 [ + - ]: 1835878 : Trace("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
130 [ - - ]: 917939 : << ", " << (value ? "true" : "false") << ")"
131 : 917939 : << std::endl;
132 [ + + ]: 917939 : if (value)
133 : : {
134 : 521884 : return d_str.propagateLit(predicate);
135 : : }
136 : 396055 : return d_str.propagateLit(predicate.notNode());
137 : : }
138 : 1084963 : bool eqNotifyTriggerTermEquality(TheoryId tag,
139 : : TNode t1,
140 : : TNode t2,
141 : : bool value) override
142 : : {
143 [ + - ]: 2169926 : Trace("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag
144 : 1084963 : << ", " << t1 << ", " << t2 << ")" << std::endl;
145 [ + + ]: 1084963 : if (value)
146 : : {
147 : 805145 : return d_str.propagateLit(t1.eqNode(t2));
148 : : }
149 : 279818 : return d_str.propagateLit(t1.eqNode(t2).notNode());
150 : : }
151 : 3596 : void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
152 : : {
153 [ + - ]: 7192 : Trace("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
154 : 3596 : << ", " << t2 << ")" << std::endl;
155 : 3596 : d_str.conflict(t1, t2);
156 : 3596 : }
157 : 284800 : void eqNotifyNewClass(TNode t) override
158 : : {
159 [ + - ]: 284800 : Trace("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
160 : 284800 : d_str.eqNotifyNewClass(t);
161 : 284800 : }
162 : 2634137 : void eqNotifyMerge(TNode t1, TNode t2) override
163 : : {
164 [ + - ]: 5268274 : Trace("strings") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
165 : 2634137 : << std::endl;
166 : 2634137 : d_str.eqNotifyMerge(t1, t2);
167 : 2634137 : }
168 : 468987 : void eqNotifyDisequal(CVC5_UNUSED TNode t1,
169 : : CVC5_UNUSED TNode t2,
170 : : CVC5_UNUSED TNode reason) override
171 : : {
172 : 468987 : }
173 : :
174 : : private:
175 : : /** The theory of strings object to notify */
176 : : TheoryStrings& d_str;
177 : : }; /* class TheoryStrings::NotifyClass */
178 : : /** compute care graph */
179 : : void computeCareGraph() override;
180 : : /** notify shared term */
181 : : void notifySharedTerm(TNode n) override;
182 : : /** Collect model info for type tn
183 : : *
184 : : * Assigns model values (in m) to all relevant terms of the string-like type
185 : : * tn in the current context, which are stored in repSet[tn].
186 : : *
187 : : * @param tn The type to compute model values for
188 : : * @param toProcess Remaining types to compute model values for
189 : : * @param repSet A map of types to representatives of
190 : : * the equivalence classes of the given type
191 : : * @return false if a conflict is discovered while doing this assignment.
192 : : */
193 : : bool collectModelInfoType(
194 : : TypeNode tn,
195 : : std::unordered_set<TypeNode>& toProcess,
196 : : const std::map<TypeNode, std::unordered_set<Node>>& repSet,
197 : : TheoryModel* m);
198 : :
199 : : /** assert pending fact
200 : : *
201 : : * This asserts atom with polarity to the equality engine of this class,
202 : : * where exp is the explanation of why (~) atom holds.
203 : : *
204 : : * This call may trigger further initialization steps involving the terms
205 : : * of atom, including calls to registerTerm.
206 : : */
207 : : void assertPendingFact(Node atom, bool polarity, Node exp);
208 : : /**
209 : : * Turn a sequence constant into a skeleton specifying how to construct
210 : : * its value.
211 : : * In particular, this means that value:
212 : : * (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2))
213 : : * becomes:
214 : : * (seq.++ (seq.unit k_0) (seq.unit k_1) (seq.unit k_2))
215 : : * where k_0, k_1, k_2 are fresh integer variables. These
216 : : * variables will be assigned values in the standard way by the
217 : : * model. This construction is necessary during model construction since the
218 : : * strings solver must constrain the length of the model of an equivalence
219 : : * class (e.g. in this case to length 3); moreover we cannot assign a concrete
220 : : * value since it may conflict with other skeletons we have assigned.
221 : : */
222 : : Node mkSkeletonFor(Node value);
223 : : /**
224 : : * Make the skeleton for the basis of constructing sequence r between
225 : : * indices currIndex (inclusive) and nextIndex (exclusive). For example, if
226 : : * currIndex = 2 and nextIndex = 5, then this returns:
227 : : * (seq.++ (seq.unit k_{r,2}) (seq.unit k_{r,3}) (seq.unit k_{r,4}))
228 : : * where k_{r,2}, k_{r,3}, k_{r,4} are Skolem variables of the element type
229 : : * of r that are unique to the pairs (r,2), (r,3), (r,4). In other words,
230 : : * these Skolems abstractly represent the element at positions 2, 3, 4 in the
231 : : * model for r.
232 : : */
233 : : Node mkSkeletonFromBase(Node r, size_t currIndex, size_t nextIndex);
234 : : //-----------------------end inference steps
235 : : /** run the given inference step */
236 : : void runInferStep(InferStep s, Theory::Effort e, int effort);
237 : : /** run strategy for effort e */
238 : : void runStrategy(Theory::Effort e);
239 : : /** print strings equivalence classes for debugging */
240 : : std::string debugPrintStringsEqc();
241 : : /** Commonly used constants */
242 : : Node d_true;
243 : : Node d_false;
244 : : Node d_zero;
245 : : Node d_one;
246 : : Node d_neg_one;
247 : : /** The notify class */
248 : : NotifyClass d_notify;
249 : : /**
250 : : * Statistics for the theory of strings/sequences. All statistics for these
251 : : * theories is collected in this object.
252 : : */
253 : : SequencesStatistics d_statistics;
254 : : /** The solver state object */
255 : : SolverState d_state;
256 : : /** The term registry for this theory */
257 : : TermRegistry d_termReg;
258 : : /** An arithmetic entailment utility */
259 : : ArithEntail d_arithEntail;
260 : : /** A string entailment utility */
261 : : StringsEntail d_strEntail;
262 : : /** The theory rewriter for this theory. */
263 : : StringsRewriter d_rewriter;
264 : : /** The eager solver */
265 : : std::unique_ptr<EagerSolver> d_eagerSolver;
266 : : /** The extended theory callback */
267 : : StringsExtfCallback d_extTheoryCb;
268 : : /** The (custom) output channel of the theory of strings */
269 : : InferenceManager d_im;
270 : : /** Extended theory, responsible for context-dependent simplification. */
271 : : ExtTheory d_extTheory;
272 : : /** The proof rule checker */
273 : : StringProofRuleChecker d_checker;
274 : : /**
275 : : * The base solver, responsible for reasoning about congruent terms and
276 : : * inferring constants for equivalence classes.
277 : : */
278 : : BaseSolver d_bsolver;
279 : : /**
280 : : * The core solver, responsible for reasoning about string concatenation
281 : : * with length constraints.
282 : : */
283 : : CoreSolver d_csolver;
284 : : /**
285 : : * Extended function solver, responsible for reductions and simplifications
286 : : * involving extended string functions.
287 : : */
288 : : ExtfSolver d_esolver;
289 : : /** Code point solver */
290 : : CodePointSolver d_psolver;
291 : : /**
292 : : * The array solver, which implements specialized approaches for
293 : : * seq.nth/seq.update.
294 : : */
295 : : ArraySolver d_asolver;
296 : : /** regular expression solver module */
297 : : RegExpSolver d_rsolver;
298 : : /** regular expression elimination module */
299 : : RegExpElimination d_regexp_elim;
300 : : /** Strings finite model finding decision strategy */
301 : : StringsFmf d_stringsFmf;
302 : : /** Model constructor (default) */
303 : : ModelConsDefault d_mcd;
304 : : /** The representation of the strategy */
305 : : Strategy d_strat;
306 : : /**
307 : : * For model building, a counter on the number of abstract witness terms
308 : : * we have built, so that unique debug names can be assigned.
309 : : */
310 : : size_t d_absModelCounter;
311 : : /**
312 : : * For model building, a counter on the number of gaps constructed for
313 : : * string terms due to array reasoning. This is to allocate unique unspecified
314 : : * characters.
315 : : */
316 : : size_t d_strGapModelCounter;
317 : : /** The care pair argument callback, used for theory combination */
318 : : CarePairArgumentCallback d_cpacb;
319 : : /** For proof of ppStaticRewrite */
320 : : std::shared_ptr<TrustProofGenerator> d_psrewPg;
321 : : }; /* class TheoryStrings */
322 : :
323 : : } // namespace strings
324 : : } // namespace theory
325 : : } // namespace cvc5::internal
326 : :
327 : : #endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_H */
|
