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