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 : : * The eager solver.
11 : : */
12 : :
13 : : #include "theory/strings/eager_solver.h"
14 : :
15 : : #include "options/strings_options.h"
16 : : #include "theory/strings/theory_strings_utils.h"
17 : : #include "util/rational.h"
18 : :
19 : : using namespace cvc5::internal::kind;
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace strings {
24 : :
25 : 51016 : EagerSolver::EagerSolver(Env& env, SolverState& state)
26 : : : EnvObj(env),
27 : 51016 : d_state(state),
28 : 51016 : d_aent(env.getNodeManager(), env.getRewriter()),
29 : 102032 : d_rent(env.getNodeManager(), env.getRewriter())
30 : : {
31 : 51016 : }
32 : :
33 : 101336 : EagerSolver::~EagerSolver() {}
34 : :
35 : 275863 : void EagerSolver::eqNotifyNewClass(TNode t)
36 : : {
37 : 275863 : Kind k = t.getKind();
38 [ + + ]: 275863 : if (k == Kind::STRING_LENGTH)
39 : : {
40 : : // also assume it as upper/lower bound as applicable for the equivalence
41 : : // class info of t.
42 : 78484 : EqcInfo* eil = nullptr;
43 [ + + ]: 235452 : for (size_t i = 0; i < 2; i++)
44 : : {
45 : 156968 : Node b = getBoundForLength(t, i == 0);
46 [ + + ]: 156968 : if (b.isNull())
47 : : {
48 : 68534 : continue;
49 : : }
50 [ + + ]: 88434 : if (eil == nullptr)
51 : : {
52 : 78484 : eil = d_state.getOrMakeEqcInfo(t);
53 : : }
54 [ + + ]: 88434 : if (i == 0)
55 : : {
56 : 78484 : eil->d_firstBound = t;
57 : : }
58 [ + - ]: 9950 : else if (i == 1)
59 : : {
60 : 9950 : eil->d_secondBound = t;
61 : : }
62 [ + + ]: 156968 : }
63 : : }
64 [ + + ]: 197379 : else if (t.isConst())
65 : : {
66 : 53637 : TypeNode tn = t.getType();
67 [ + + ][ + + ]: 53637 : if (tn.isStringLike() || tn.isInteger())
[ + + ]
68 : : {
69 : 41491 : EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
70 : 41491 : ei->d_firstBound = t;
71 : 41491 : ei->d_secondBound = t;
72 : : }
73 : 53637 : }
74 [ + + ]: 143742 : else if (k == Kind::STRING_CONCAT)
75 : : {
76 : 26590 : addEndpointsToEqcInfo(t, t, t);
77 : : }
78 : 275863 : }
79 : :
80 : 1622738 : void EagerSolver::eqNotifyMerge(EqcInfo* e1, TNode t1, EqcInfo* e2, TNode t2)
81 : : {
82 [ - + ][ - + ]: 1622738 : Assert(e1 != nullptr);
[ - - ]
83 [ - + ][ - + ]: 1622738 : Assert(e2 != nullptr);
[ - - ]
84 : : // check for conflict
85 [ + + ]: 1622738 : if (checkForMergeConflict(t1, t2, e1, e2))
86 : : {
87 : 1133 : return;
88 : : }
89 : : }
90 : :
91 : 30352 : bool EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
92 : : {
93 [ + + ][ + - ]: 30352 : Assert(concat.getKind() == Kind::STRING_CONCAT
[ - + ][ - + ]
[ - - ]
94 : : || concat.getKind() == Kind::REGEXP_CONCAT);
95 : 30352 : EqcInfo* ei = nullptr;
96 : : // check each side
97 [ + + ]: 91035 : for (size_t r = 0; r < 2; r++)
98 : : {
99 [ + + ]: 60700 : size_t index = r == 0 ? 0 : concat.getNumChildren() - 1;
100 : 60700 : Node c = utils::getConstantComponent(concat[index]);
101 [ + + ]: 60700 : if (!c.isNull())
102 : : {
103 [ + + ]: 11503 : if (ei == nullptr)
104 : : {
105 : 10382 : ei = d_state.getOrMakeEqcInfo(eqc);
106 : : }
107 [ + - ]: 23006 : Trace("strings-eager-pconf-debug")
108 : 0 : << "New term: " << concat << " for " << t << " with prefix " << c
109 : 11503 : << " (" << (r == 1) << ")" << std::endl;
110 [ + + ]: 11503 : if (addEndpointConst(ei, t, c, r == 1))
111 : : {
112 : 17 : return true;
113 : : }
114 : : }
115 [ + + ]: 60700 : }
116 : 30335 : return false;
117 : : }
118 : :
119 : 1622738 : bool EagerSolver::checkForMergeConflict(Node a,
120 : : Node b,
121 : : EqcInfo* ea,
122 : : EqcInfo* eb)
123 : : {
124 [ + - ][ + - ]: 1622738 : Assert(eb != nullptr && ea != nullptr);
[ - + ][ - + ]
[ - - ]
125 : 4868214 : AssertEqual(a.getType(), b.getType())
126 [ - + ][ - + ]: 1622738 : << "bad types for merge " << a << ", " << b;
[ - - ]
127 : : // usages of isRealOrInt are only due to subtyping, where seq.nth for
128 : : // sequences of Real are merged to integer equivalence classes
129 : 1622738 : Assert(a.getType().isStringLike() || a.getType().isRealOrInt());
130 : : // check prefix, suffix
131 [ + + ]: 4866383 : for (size_t i = 0; i < 2; i++)
132 : : {
133 [ + + ]: 3244778 : Node n = i == 0 ? eb->d_firstBound.get() : eb->d_secondBound.get();
134 [ + + ]: 3244778 : if (!n.isNull())
135 : : {
136 : : bool isConflict;
137 [ + + ]: 967721 : if (a.getType().isStringLike())
138 : : {
139 : 145727 : isConflict = addEndpointConst(ea, n, Node::null(), i == 1);
140 : : }
141 : : else
142 : : {
143 [ + - ]: 1643988 : Trace("strings-eager-aconf-debug")
144 : 0 : << "addArithmeticBound " << n << " into " << a << " from " << b
145 : 821994 : << std::endl;
146 : 821994 : isConflict = addArithmeticBound(ea, n, i == 0);
147 : : }
148 [ + + ]: 967721 : if (isConflict)
149 : : {
150 : 1133 : return true;
151 : : }
152 : : }
153 [ + + ]: 3244778 : }
154 : 1621605 : return false;
155 : : }
156 : :
157 : 2181904 : void EagerSolver::notifyFact(TNode atom,
158 : : bool polarity,
159 : : CVC5_UNUSED TNode fact,
160 : : CVC5_UNUSED bool isInternal)
161 : : {
162 [ + + ]: 2181904 : if (atom.getKind() == Kind::STRING_IN_REGEXP)
163 : : {
164 [ + + ][ + + ]: 11528 : if (polarity && atom[1].getKind() == Kind::REGEXP_CONCAT)
[ + + ][ + + ]
[ - - ]
165 : : {
166 : 3762 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
167 : 7524 : Node eqc = ee->getRepresentative(atom[0]);
168 : : // add prefix constraints
169 [ + + ]: 3762 : if (addEndpointsToEqcInfo(atom, atom[1], eqc))
170 : : {
171 : : // conflict, we are done
172 : 17 : return;
173 : : }
174 [ + + ]: 3745 : else if (!options().strings.stringsEagerLenEntRegexp)
175 : : {
176 : : // do not infer length constraints if option is disabled
177 : 3732 : return;
178 : : }
179 : : // also infer length constraints if the first is a variable
180 [ + + ]: 13 : if (atom[0].isVar())
181 : : {
182 : 9 : EqcInfo* blenEqc = nullptr;
183 [ + + ]: 27 : for (size_t i = 0; i < 2; i++)
184 : : {
185 : 18 : bool isLower = (i == 0);
186 : 18 : Node b = d_rent.getConstantBoundLengthForRegexp(atom[1], isLower);
187 [ + + ]: 18 : if (!b.isNull())
188 : : {
189 [ + + ]: 11 : if (blenEqc == nullptr)
190 : : {
191 : : Node lenTerm =
192 : 9 : nodeManager()->mkNode(Kind::STRING_LENGTH, atom[0]);
193 [ - + ]: 9 : if (!ee->hasTerm(lenTerm))
194 : : {
195 : 0 : break;
196 : : }
197 : 9 : lenTerm = ee->getRepresentative(lenTerm);
198 : 9 : blenEqc = d_state.getOrMakeEqcInfo(lenTerm);
199 [ + - ]: 9 : }
200 [ - + ]: 11 : if (addArithmeticBound(blenEqc, atom, isLower))
201 : : {
202 : 0 : return;
203 : : }
204 : : }
205 [ + - ][ - ]: 18 : }
206 : : }
207 [ + + ]: 3762 : }
208 : : }
209 : : }
210 : :
211 : 157230 : bool EagerSolver::addEndpointConst(EqcInfo* e, Node t, Node c, bool isSuf)
212 : : {
213 [ - + ][ - + ]: 157230 : Assert(e != nullptr);
[ - - ]
214 [ - + ][ - + ]: 157230 : Assert(!t.isNull());
[ - - ]
215 : 314460 : Node conf = e->addEndpointConst(t, c, isSuf);
216 [ + + ]: 157230 : if (!conf.isNull())
217 : : {
218 : 768 : d_state.setPendingMergeConflict(
219 : : conf, InferenceId::STRINGS_PREFIX_CONFLICT, isSuf);
220 : 768 : return true;
221 : : }
222 : 156462 : return false;
223 : 157230 : }
224 : :
225 : 822005 : bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
226 : : {
227 [ + - ]: 1644010 : Trace("strings-eager-aconf-debug")
228 : 0 : << "addArithmeticBound " << t << ", isLower = " << isLower << "..."
229 : 822005 : << std::endl;
230 [ - + ][ - + ]: 822005 : Assert(e != nullptr);
[ - - ]
231 [ - + ][ - + ]: 822005 : Assert(!t.isNull());
[ - - ]
232 [ - + ][ + - ]: 822005 : Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
[ - - ]
233 : 1644010 : Assert(!tb.isNull() && tb.isConst() && tb.getType().isRealOrInt())
234 [ - + ][ - + ]: 822005 : << "Unexpected bound " << tb << " from " << t;
[ - - ]
235 : 822005 : Rational br = tb.getConst<Rational>();
236 [ + + ]: 822005 : Node prev = isLower ? e->d_firstBound : e->d_secondBound;
237 : : // check if subsumed
238 [ + + ]: 822005 : if (!prev.isNull())
239 : : {
240 : : // convert to bound
241 [ + + ][ + + ]: 818943 : Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
[ - - ]
242 : 818943 : Assert(!prevb.isNull() && prevb.isConst() && prevb.getType().isRealOrInt());
243 : 818943 : Rational prevbr = prevb.getConst<Rational>();
244 [ + + ][ + + ]: 818943 : if (prevbr == br || (br < prevbr) == isLower)
[ + + ]
245 : : {
246 : : // subsumed
247 : 778103 : return false;
248 : : }
249 [ + + ][ + + ]: 1597046 : }
250 [ + - ]: 43902 : Node prevo = isLower ? e->d_secondBound : e->d_firstBound;
251 [ + - ]: 87804 : Trace("strings-eager-aconf-debug")
252 : 43902 : << "Check conflict for bounds " << t << " " << prevo << std::endl;
253 [ + + ]: 43902 : if (!prevo.isNull())
254 : : {
255 : : // are we in conflict?
256 [ + - ][ - + ]: 382 : Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
[ - - ]
257 : 382 : Assert(!prevob.isNull() && prevob.isConst()
258 : : && prevob.getType().isRealOrInt());
259 : 382 : Rational prevobr = prevob.getConst<Rational>();
260 [ + - ]: 764 : Trace("strings-eager-aconf-debug")
261 : 0 : << "Previous opposite bound was " << prevobr << ", current bound is "
262 : 382 : << br << ", isLower = " << isLower << std::endl;
263 [ + - ][ + - ]: 382 : if (prevobr != br && (prevobr < br) == isLower)
[ + - ]
264 : : {
265 : : // conflict
266 : 764 : Node ret = EqcInfo::mkMergeConflict(t, prevo, true);
267 [ + - ]: 764 : Trace("strings-eager-aconf")
268 : 382 : << "String: eager arithmetic bound conflict: " << ret << std::endl;
269 : 382 : d_state.setPendingMergeConflict(
270 : : ret, InferenceId::STRINGS_ARITH_BOUND_CONFLICT);
271 : 382 : return true;
272 : 382 : }
273 [ - + ][ - + ]: 764 : }
274 [ + - ]: 43520 : if (isLower)
275 : : {
276 : 43520 : e->d_firstBound = t;
277 : : }
278 : : else
279 : : {
280 : 0 : e->d_secondBound = t;
281 : : }
282 : 43520 : return false;
283 : 822005 : }
284 : :
285 : 1209440 : Node EagerSolver::getBoundForLength(Node t, bool isLower) const
286 : : {
287 [ + + ]: 1209440 : if (t.getKind() == Kind::STRING_IN_REGEXP)
288 : : {
289 : 25 : return d_rent.getConstantBoundLengthForRegexp(t[1], isLower);
290 : : }
291 [ - + ][ - + ]: 1209415 : Assert(t.getKind() == Kind::STRING_LENGTH);
[ - - ]
292 : : // it is prohibitively expensive to convert to original form and rewrite,
293 : : // since this may invoke the rewriter on lengths of complex terms. Instead,
294 : : // we convert to original term the argument, then call the utility method
295 : : // for computing the length of the argument, implicitly under an application
296 : : // of length (ArithEntail::getConstantBoundLength).
297 : : // convert to original form
298 : 1209415 : Node olent = SkolemManager::getOriginalForm(t[0]);
299 : : // get the bound
300 : 1209415 : Node c = d_aent.getConstantBoundLength(olent, isLower);
301 [ + - ]: 2418830 : Trace("strings-eager-aconf-debug")
302 [ - - ]: 0 : << "Constant " << (isLower ? "lower" : "upper") << " bound for " << t
303 : 1209415 : << " is " << c << ", from original form " << olent << std::endl;
304 : 1209415 : return c;
305 : 1209415 : }
306 : :
307 : : } // namespace strings
308 : : } // namespace theory
309 : : } // namespace cvc5::internal
|
