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