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