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 : : * Implementation of substitution minimization.
11 : : */
12 : :
13 : : #include "theory/subs_minimize.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "theory/bv/theory_bv_utils.h"
17 : : #include "theory/rewriter.h"
18 : : #include "theory/strings/word.h"
19 : : #include "util/rational.h"
20 : :
21 : : using namespace std;
22 : : using namespace cvc5::internal::kind;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : :
27 : 9 : SubstitutionMinimize::SubstitutionMinimize(Env& env) : EnvObj(env) {}
28 : :
29 : 6 : bool SubstitutionMinimize::find(Node t,
30 : : Node target,
31 : : const std::vector<Node>& vars,
32 : : const std::vector<Node>& subs,
33 : : std::vector<Node>& reqVars)
34 : : {
35 : 6 : return findInternal(t, target, vars, subs, reqVars);
36 : : }
37 : :
38 : 26 : void getConjuncts(Node n, std::vector<Node>& conj)
39 : : {
40 [ + + ]: 26 : if (n.getKind() == Kind::AND)
41 : : {
42 [ + + ]: 24 : for (const Node& nc : n)
43 : : {
44 : 19 : conj.push_back(nc);
45 : 19 : }
46 : : }
47 : : else
48 : : {
49 : 21 : conj.push_back(n);
50 : : }
51 : 26 : }
52 : :
53 : 3 : bool SubstitutionMinimize::findWithImplied(Node t,
54 : : const std::vector<Node>& vars,
55 : : const std::vector<Node>& subs,
56 : : std::vector<Node>& reqVars,
57 : : std::vector<Node>& impliedVars)
58 : : {
59 : 3 : NodeManager* nm = nodeManager();
60 : 3 : Node truen = nm->mkConst(true);
61 [ - + ]: 3 : if (!findInternal(t, truen, vars, subs, reqVars))
62 : : {
63 : 0 : return false;
64 : : }
65 [ - + ]: 3 : if (reqVars.empty())
66 : : {
67 : 0 : return true;
68 : : }
69 : :
70 : : // map from conjuncts of t to whether they may be used to show an implied var
71 : 3 : std::vector<Node> tconj;
72 : 3 : getConjuncts(t, tconj);
73 : : // map from conjuncts to their free symbols
74 : 3 : std::map<Node, std::unordered_set<Node> > tcFv;
75 : :
76 : 3 : std::unordered_set<Node> reqSet;
77 : 3 : std::vector<Node> reqSubs;
78 : 3 : std::map<Node, unsigned> reqVarToIndex;
79 [ + + ]: 10 : for (const Node& v : reqVars)
80 : : {
81 : 7 : reqVarToIndex[v] = reqSubs.size();
82 : : const std::vector<Node>::const_iterator& it =
83 : 7 : std::find(vars.begin(), vars.end(), v);
84 [ - + ][ - + ]: 7 : Assert(it != vars.end());
[ - - ]
85 : 7 : ptrdiff_t pos = std::distance(vars.begin(), it);
86 : 7 : reqSubs.push_back(subs[pos]);
87 : : }
88 : 3 : std::vector<Node> finalReqVars;
89 [ + + ]: 10 : for (const Node& v : vars)
90 : : {
91 [ - + ]: 7 : if (reqVarToIndex.find(v) == reqVarToIndex.end())
92 : : {
93 : : // not a required variable, nothing to do
94 : 0 : continue;
95 : : }
96 : 7 : unsigned vindex = reqVarToIndex[v];
97 : 7 : Node prev = reqSubs[vindex];
98 : : // make identity substitution
99 : 7 : reqSubs[vindex] = v;
100 : 7 : bool madeImplied = false;
101 : : // it is a required variable, can we make an implied variable?
102 [ + + ]: 50 : for (const Node& tc : tconj)
103 : : {
104 : : // ensure we've computed its free symbols
105 : 43 : std::map<Node, std::unordered_set<Node> >::iterator itf = tcFv.find(tc);
106 [ + + ]: 43 : if (itf == tcFv.end())
107 : : {
108 : 11 : expr::getSymbols(tc, tcFv[tc]);
109 : 11 : itf = tcFv.find(tc);
110 : : }
111 : : // only have a chance if contains v
112 [ + + ]: 43 : if (itf->second.find(v) == itf->second.end())
113 : : {
114 : 20 : continue;
115 : : }
116 : : // try the current substitution
117 : : Node tcs = tc.substitute(
118 : 23 : reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end());
119 : 23 : Node tcsr = rewrite(tcs);
120 : 23 : std::vector<Node> tcsrConj;
121 : 23 : getConjuncts(tcsr, tcsrConj);
122 [ + + ]: 48 : for (const Node& tcc : tcsrConj)
123 : : {
124 [ - + ]: 25 : if (tcc.getKind() == Kind::EQUAL)
125 : : {
126 [ - - ]: 0 : for (unsigned r = 0; r < 2; r++)
127 : : {
128 [ - - ]: 0 : if (tcc[r] == v)
129 : : {
130 : 0 : Node res = tcc[1 - r];
131 [ - - ]: 0 : if (res.isConst())
132 : : {
133 : 0 : Assert(res == prev);
134 : 0 : madeImplied = true;
135 : 0 : break;
136 : : }
137 [ - - ]: 0 : }
138 : : }
139 : : }
140 [ - + ]: 25 : if (madeImplied)
141 : : {
142 : 0 : break;
143 : : }
144 : : }
145 [ - + ]: 23 : if (madeImplied)
146 : : {
147 : 0 : break;
148 : : }
149 [ + - ][ + - ]: 23 : }
[ + - ]
150 [ + - ]: 7 : if (!madeImplied)
151 : : {
152 : : // revert the substitution
153 : 7 : reqSubs[vindex] = prev;
154 : 7 : finalReqVars.push_back(v);
155 : : }
156 : : else
157 : : {
158 : 0 : impliedVars.push_back(v);
159 : : }
160 : 7 : }
161 : 3 : reqVars.clear();
162 : 3 : reqVars.insert(reqVars.end(), finalReqVars.begin(), finalReqVars.end());
163 : :
164 : 3 : return true;
165 : 3 : }
166 : :
167 : 9 : bool SubstitutionMinimize::findInternal(Node n,
168 : : Node target,
169 : : const std::vector<Node>& vars,
170 : : const std::vector<Node>& subs,
171 : : std::vector<Node>& reqVars)
172 : : {
173 [ + - ]: 9 : Trace("subs-min") << "Substitution minimize : " << std::endl;
174 [ + - ]: 18 : Trace("subs-min") << " substitution : " << vars << " -> " << subs
175 : 9 : << std::endl;
176 [ + - ]: 9 : Trace("subs-min") << " node : " << n << std::endl;
177 [ + - ]: 9 : Trace("subs-min") << " target : " << target << std::endl;
178 : :
179 [ + - ]: 9 : Trace("subs-min") << "--- Compute values for subterms..." << std::endl;
180 : : // the value of each subterm in n under the substitution
181 : 9 : std::unordered_map<TNode, Node> value;
182 : 9 : std::unordered_map<TNode, Node>::iterator it;
183 : 9 : std::vector<TNode> visit;
184 : 9 : TNode cur;
185 : 9 : visit.push_back(n);
186 : : do
187 : : {
188 : 230 : cur = visit.back();
189 : 230 : visit.pop_back();
190 : 230 : it = value.find(cur);
191 : :
192 [ + + ]: 230 : if (it == value.end())
193 : : {
194 [ + + ]: 103 : if (cur.isVar())
195 : : {
196 : : const std::vector<Node>::const_iterator& iit =
197 : 21 : std::find(vars.begin(), vars.end(), cur);
198 [ - + ]: 21 : if (iit == vars.end())
199 : : {
200 : 0 : value[cur] = cur;
201 : : }
202 : : else
203 : : {
204 : 21 : ptrdiff_t pos = std::distance(vars.begin(), iit);
205 : 21 : value[cur] = subs[pos];
206 : : }
207 : : }
208 : : else
209 : : {
210 : 82 : value[cur] = Node::null();
211 : 82 : visit.push_back(cur);
212 [ + + ]: 82 : if (cur.getKind() == Kind::APPLY_UF)
213 : : {
214 : 2 : visit.push_back(cur.getOperator());
215 : : }
216 : 82 : visit.insert(visit.end(), cur.begin(), cur.end());
217 : : }
218 : : }
219 [ + + ]: 127 : else if (it->second.isNull())
220 : : {
221 : 82 : Node ret = cur;
222 [ + + ]: 82 : if (cur.getNumChildren() > 0)
223 : : {
224 : 71 : std::vector<Node> children;
225 : 71 : NodeBuilder nb(nodeManager(), cur.getKind());
226 [ + + ]: 71 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
227 : : {
228 [ + - ]: 2 : if (cur.getKind() == Kind::APPLY_UF)
229 : : {
230 : 2 : children.push_back(cur.getOperator());
231 : : }
232 : : else
233 : : {
234 : 0 : nb << cur.getOperator();
235 : : }
236 : : }
237 : 71 : children.insert(children.end(), cur.begin(), cur.end());
238 [ + + ]: 210 : for (const Node& cn : children)
239 : : {
240 : 139 : it = value.find(cn);
241 [ - + ][ - + ]: 139 : Assert(it != value.end());
[ - - ]
242 [ - + ][ - + ]: 139 : Assert(!it->second.isNull());
[ - - ]
243 : 139 : nb << it->second;
244 : : }
245 : 71 : ret = nb.constructNode();
246 : 71 : ret = rewrite(ret);
247 : 71 : }
248 : 82 : value[cur] = ret;
249 : 82 : }
250 [ + + ]: 230 : } while (!visit.empty());
251 [ - + ][ - + ]: 9 : Assert(value.find(n) != value.end());
[ - - ]
252 [ - + ][ - + ]: 9 : Assert(!value.find(n)->second.isNull());
[ - - ]
253 : :
254 [ + - ][ - + ]: 9 : Trace("subs-min") << "... got " << value[n] << std::endl;
[ - - ]
255 [ + + ]: 9 : if (value[n] != target)
256 : : {
257 [ + - ]: 2 : Trace("subs-min") << "... not equal to target " << target << std::endl;
258 : : // depends on all variables
259 [ + + ]: 14 : for (const std::pair<const TNode, Node>& v : value)
260 : : {
261 [ + + ]: 12 : if (v.first.isVar())
262 : : {
263 : 2 : reqVars.push_back(v.first);
264 : : }
265 : : }
266 : 2 : return false;
267 : : }
268 : :
269 [ + - ]: 7 : Trace("subs-min") << "--- Compute relevant variables..." << std::endl;
270 : 7 : std::unordered_set<Node> rlvFv;
271 : : // only variables that occur in assertions are relevant
272 : :
273 : 7 : visit.push_back(n);
274 : 7 : std::unordered_set<TNode> visited;
275 : 7 : std::unordered_set<TNode>::iterator itv;
276 : : do
277 : : {
278 : 107 : cur = visit.back();
279 : 107 : visit.pop_back();
280 : 107 : itv = visited.find(cur);
281 [ + + ]: 107 : if (itv == visited.end())
282 : : {
283 : 76 : visited.insert(cur);
284 : 76 : it = value.find(cur);
285 [ + + ]: 76 : if (it->second == cur)
286 : : {
287 : : // if its value is the same as current, there is nothing to do
288 : : }
289 [ + + ]: 68 : else if (cur.isVar())
290 : : {
291 : : // must include
292 : 15 : rlvFv.insert(cur);
293 : : }
294 [ - + ]: 53 : else if (cur.getKind() == Kind::ITE)
295 : : {
296 : : // only recurse on relevant branch
297 : 0 : Node bval = value[cur[0]];
298 : 0 : if (!bval.isNull() && bval.isConst())
299 : : {
300 [ - - ]: 0 : unsigned cindex = bval.getConst<bool>() ? 1 : 2;
301 : 0 : visit.push_back(cur[0]);
302 : 0 : visit.push_back(cur[cindex]);
303 : 0 : continue;
304 : 0 : }
305 : : // otherwise, we handle it normally below
306 [ - - ]: 0 : }
307 [ + + ]: 76 : if (cur.getNumChildren() > 0)
308 : : {
309 : 53 : Kind ck = cur.getKind();
310 : 53 : bool alreadyJustified = false;
311 : :
312 : : // if the operator is an apply uf, check its value
313 [ + + ]: 53 : if (cur.getKind() == Kind::APPLY_UF)
314 : : {
315 : 2 : Node op = cur.getOperator();
316 : 2 : it = value.find(op);
317 [ - + ][ - + ]: 2 : Assert(it != value.end());
[ - - ]
318 : 2 : TNode vop = it->second;
319 [ + - ]: 2 : if (vop.getKind() == Kind::LAMBDA)
320 : : {
321 : 2 : visit.push_back(op);
322 : : // do iterative partial evaluation on the body of the lambda
323 : 2 : Node curr = vop[1];
324 [ + + ]: 4 : for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
325 : : {
326 : 2 : it = value.find(cur[i]);
327 [ - + ][ - + ]: 2 : Assert(it != value.end());
[ - - ]
328 : 4 : Node scurr = curr.substitute(vop[0][i], it->second);
329 : : // if the valuation of the i^th argument changes the
330 : : // interpretation of the body of the lambda, then the i^th
331 : : // argument is relevant to the substitution. Hence, we add
332 : : // i to visit, and update curr below.
333 [ - + ]: 2 : if (scurr != curr)
334 : : {
335 : 0 : curr = rewrite(scurr);
336 : 0 : visit.push_back(cur[i]);
337 : : }
338 : 2 : }
339 : 2 : alreadyJustified = true;
340 : 2 : }
341 : 2 : }
342 [ + + ]: 53 : if (!alreadyJustified)
343 : : {
344 : : // a subset of the arguments of cur that fully justify the evaluation
345 : 51 : std::vector<unsigned> justifyArgs;
346 [ + + ]: 51 : if (cur.getNumChildren() > 1)
347 : : {
348 [ + + ]: 138 : for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
349 : : {
350 : 95 : Node cn = cur[i];
351 : 95 : it = value.find(cn);
352 [ - + ][ - + ]: 95 : Assert(it != value.end());
[ - - ]
353 [ - + ][ - + ]: 95 : Assert(!it->second.isNull());
[ - - ]
354 [ + + ]: 95 : if (isSingularArg(it->second, ck, i))
355 : : {
356 : : // have we seen this argument already? if so, we are done
357 [ - + ]: 6 : if (visited.find(cn) != visited.end())
358 : : {
359 : 0 : alreadyJustified = true;
360 : 0 : break;
361 : : }
362 : 6 : justifyArgs.push_back(i);
363 : : }
364 [ + - ]: 95 : }
365 : : }
366 : : // we need to recurse on at most one child
367 [ + - ][ + + ]: 51 : if (!alreadyJustified && !justifyArgs.empty())
[ + + ]
368 : : {
369 : 5 : unsigned sindex = justifyArgs[0];
370 : : // could choose a best index, for now, we just take the first
371 : 5 : visit.push_back(cur[sindex]);
372 : 5 : alreadyJustified = true;
373 : : }
374 : 51 : }
375 [ + + ]: 53 : if (!alreadyJustified)
376 : : {
377 : : // must recurse on all arguments, including operator
378 [ - + ]: 46 : if (cur.getKind() == Kind::APPLY_UF)
379 : : {
380 : 0 : visit.push_back(cur.getOperator());
381 : : }
382 [ + + ]: 139 : for (const Node& cn : cur)
383 : : {
384 : 93 : visit.push_back(cn);
385 : 93 : }
386 : : }
387 : : }
388 : : }
389 [ + + ]: 107 : } while (!visit.empty());
390 : :
391 [ + + ]: 22 : for (const Node& v : rlvFv)
392 : : {
393 [ - + ][ - + ]: 15 : Assert(std::find(vars.begin(), vars.end(), v) != vars.end());
[ - - ]
394 : 15 : reqVars.push_back(v);
395 : : }
396 : :
397 [ + - ]: 14 : Trace("subs-min") << "... requires " << reqVars.size() << "/" << vars.size()
398 : 7 : << " : " << reqVars << std::endl;
399 : :
400 : 7 : return true;
401 : 9 : }
402 : :
403 : 95 : bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
404 : : {
405 : : // Notice that this function is hardcoded. We could compute this function
406 : : // in a theory-independent way using partial evaluation. However, we
407 : : // prefer performance to generality here.
408 : :
409 : : // TODO: a variant of this code is implemented in quantifiers::TermUtil.
410 : : // These implementations should be merged (see #1216).
411 [ - + ]: 95 : if (!n.isConst())
412 : : {
413 : 0 : return false;
414 : : }
415 [ + + ]: 95 : if (k == Kind::AND)
416 : : {
417 : 27 : return !n.getConst<bool>();
418 : : }
419 [ + + ]: 68 : else if (k == Kind::OR)
420 : : {
421 : 10 : return n.getConst<bool>();
422 : : }
423 [ - + ]: 58 : else if (k == Kind::IMPLIES)
424 : : {
425 [ - - ]: 0 : return arg == (n.getConst<bool>() ? 1 : 0);
426 : : }
427 [ + + ]: 58 : if (k == Kind::MULT
428 [ + + ]: 54 : || (arg == 0
429 [ + - ][ + - ]: 27 : && (k == Kind::DIVISION_TOTAL || k == Kind::INTS_DIVISION_TOTAL
430 [ + - ]: 27 : || k == Kind::INTS_MODULUS_TOTAL))
431 [ - + ][ - - ]: 54 : || (arg == 2 && k == Kind::STRING_SUBSTR))
432 : : {
433 : : // zero
434 [ - + ]: 4 : if (n.getConst<Rational>().sgn() == 0)
435 : : {
436 : 0 : return true;
437 : : }
438 : : }
439 [ + - ][ + - ]: 58 : if (k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_MULT
440 [ + - ][ + - ]: 58 : || k == Kind::BITVECTOR_UDIV || k == Kind::BITVECTOR_UREM
441 [ + + ]: 58 : || (arg == 0
442 [ + - ][ + - ]: 29 : && (k == Kind::BITVECTOR_SHL || k == Kind::BITVECTOR_LSHR
443 [ - + ]: 29 : || k == Kind::BITVECTOR_ASHR)))
444 : : {
445 [ - - ]: 0 : if (bv::utils::isZero(n))
446 : : {
447 : 0 : return true;
448 : : }
449 : : }
450 [ - + ]: 58 : if (k == Kind::BITVECTOR_OR)
451 : : {
452 : : // bit-vector ones
453 [ - - ]: 0 : if (bv::utils::isOnes(n))
454 : : {
455 : 0 : return true;
456 : : }
457 : : }
458 : :
459 [ + + ][ + - ]: 58 : if ((arg == 1 && k == Kind::STRING_CONTAINS)
460 [ + + ][ - + ]: 58 : || (arg == 0 && k == Kind::STRING_SUBSTR))
461 : : {
462 : : // empty string
463 [ - - ]: 0 : if (strings::Word::getLength(n) == 0)
464 : : {
465 : 0 : return true;
466 : : }
467 : : }
468 [ + + ][ + - ]: 58 : if ((arg != 0 && k == Kind::STRING_SUBSTR)
469 [ - + ][ - - ]: 58 : || (arg == 2 && k == Kind::STRING_INDEXOF))
470 : : {
471 : : // negative integer
472 [ - - ]: 0 : if (n.getConst<Rational>().sgn() < 0)
473 : : {
474 : 0 : return true;
475 : : }
476 : : }
477 : 58 : return false;
478 : : }
479 : :
480 : : } // namespace theory
481 : : } // namespace cvc5::internal
|
