1 /********************* */
2 /*! \file subs_minimize.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of substitution minimization.
15 #include "theory/subs_minimize.h"
17 #include "expr/node_algorithm.h"
18 #include "theory/bv/theory_bv_utils.h"
19 #include "theory/rewriter.h"
20 #include "theory/strings/word.h"
23 using namespace CVC4::kind
;
28 SubstitutionMinimize::SubstitutionMinimize() {}
30 bool SubstitutionMinimize::find(Node t
,
32 const std::vector
<Node
>& vars
,
33 const std::vector
<Node
>& subs
,
34 std::vector
<Node
>& reqVars
)
36 return findInternal(t
, target
, vars
, subs
, reqVars
);
39 void getConjuncts(Node n
, std::vector
<Node
>& conj
)
41 if (n
.getKind() == AND
)
43 for (const Node
& nc
: n
)
54 bool SubstitutionMinimize::findWithImplied(Node t
,
55 const std::vector
<Node
>& vars
,
56 const std::vector
<Node
>& subs
,
57 std::vector
<Node
>& reqVars
,
58 std::vector
<Node
>& impliedVars
)
60 NodeManager
* nm
= NodeManager::currentNM();
61 Node truen
= nm
->mkConst(true);
62 if (!findInternal(t
, truen
, vars
, subs
, reqVars
))
71 // map from conjuncts of t to whether they may be used to show an implied var
72 std::vector
<Node
> tconj
;
73 getConjuncts(t
, tconj
);
74 // map from conjuncts to their free symbols
75 std::map
<Node
, std::unordered_set
<Node
, NodeHashFunction
> > tcFv
;
77 std::unordered_set
<Node
, NodeHashFunction
> reqSet
;
78 std::vector
<Node
> reqSubs
;
79 std::map
<Node
, unsigned> reqVarToIndex
;
80 for (const Node
& v
: reqVars
)
82 reqVarToIndex
[v
] = reqSubs
.size();
83 const std::vector
<Node
>::const_iterator
& it
=
84 std::find(vars
.begin(), vars
.end(), v
);
85 Assert(it
!= vars
.end());
86 ptrdiff_t pos
= std::distance(vars
.begin(), it
);
87 reqSubs
.push_back(subs
[pos
]);
89 std::vector
<Node
> finalReqVars
;
90 for (const Node
& v
: vars
)
92 if (reqVarToIndex
.find(v
) == reqVarToIndex
.end())
94 // not a required variable, nothing to do
97 unsigned vindex
= reqVarToIndex
[v
];
98 Node prev
= reqSubs
[vindex
];
99 // make identity substitution
101 bool madeImplied
= false;
102 // it is a required variable, can we make an implied variable?
103 for (const Node
& tc
: tconj
)
105 // ensure we've computed its free symbols
106 std::map
<Node
, std::unordered_set
<Node
, NodeHashFunction
> >::iterator
108 if (itf
== tcFv
.end())
110 expr::getSymbols(tc
, tcFv
[tc
]);
113 // only have a chance if contains v
114 if (itf
->second
.find(v
) == itf
->second
.end())
118 // try the current substitution
119 Node tcs
= tc
.substitute(
120 reqVars
.begin(), reqVars
.end(), reqSubs
.begin(), reqSubs
.end());
121 Node tcsr
= Rewriter::rewrite(tcs
);
122 std::vector
<Node
> tcsrConj
;
123 getConjuncts(tcsr
, tcsrConj
);
124 for (const Node
& tcc
: tcsrConj
)
126 if (tcc
.getKind() == EQUAL
)
128 for (unsigned r
= 0; r
< 2; r
++)
132 Node res
= tcc
[1 - r
];
154 // revert the substitution
155 reqSubs
[vindex
] = prev
;
156 finalReqVars
.push_back(v
);
160 impliedVars
.push_back(v
);
164 reqVars
.insert(reqVars
.end(), finalReqVars
.begin(), finalReqVars
.end());
169 bool SubstitutionMinimize::findInternal(Node n
,
171 const std::vector
<Node
>& vars
,
172 const std::vector
<Node
>& subs
,
173 std::vector
<Node
>& reqVars
)
175 Trace("subs-min") << "Substitution minimize : " << std::endl
;
176 Trace("subs-min") << " substitution : " << vars
<< " -> " << subs
178 Trace("subs-min") << " node : " << n
<< std::endl
;
179 Trace("subs-min") << " target : " << target
<< std::endl
;
181 Trace("subs-min") << "--- Compute values for subterms..." << std::endl
;
182 // the value of each subterm in n under the substitution
183 std::unordered_map
<TNode
, Node
, TNodeHashFunction
> value
;
184 std::unordered_map
<TNode
, Node
, TNodeHashFunction
>::iterator it
;
185 std::vector
<TNode
> visit
;
192 it
= value
.find(cur
);
194 if (it
== value
.end())
198 const std::vector
<Node
>::const_iterator
& iit
=
199 std::find(vars
.begin(), vars
.end(), cur
);
200 if (iit
== vars
.end())
206 ptrdiff_t pos
= std::distance(vars
.begin(), iit
);
207 value
[cur
] = subs
[pos
];
212 value
[cur
] = Node::null();
213 visit
.push_back(cur
);
214 if (cur
.getKind() == APPLY_UF
)
216 visit
.push_back(cur
.getOperator());
218 visit
.insert(visit
.end(), cur
.begin(), cur
.end());
221 else if (it
->second
.isNull())
224 if (cur
.getNumChildren() > 0)
226 std::vector
<Node
> children
;
227 NodeBuilder
<> nb(cur
.getKind());
228 if (cur
.getMetaKind() == kind::metakind::PARAMETERIZED
)
230 if (cur
.getKind() == APPLY_UF
)
232 children
.push_back(cur
.getOperator());
236 nb
<< cur
.getOperator();
239 children
.insert(children
.end(), cur
.begin(), cur
.end());
240 for (const Node
& cn
: children
)
243 Assert(it
!= value
.end());
244 Assert(!it
->second
.isNull());
247 ret
= nb
.constructNode();
248 ret
= Rewriter::rewrite(ret
);
252 } while (!visit
.empty());
253 Assert(value
.find(n
) != value
.end());
254 Assert(!value
.find(n
)->second
.isNull());
256 Trace("subs-min") << "... got " << value
[n
] << std::endl
;
257 if (value
[n
] != target
)
259 Trace("subs-min") << "... not equal to target " << target
<< std::endl
;
263 Trace("subs-min") << "--- Compute relevant variables..." << std::endl
;
264 std::unordered_set
<Node
, NodeHashFunction
> rlvFv
;
265 // only variables that occur in assertions are relevant
268 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
269 std::unordered_set
<TNode
, TNodeHashFunction
>::iterator itv
;
274 itv
= visited
.find(cur
);
275 if (itv
== visited
.end())
278 it
= value
.find(cur
);
279 if (it
->second
== cur
)
281 // if its value is the same as current, there is nothing to do
283 else if (cur
.isVar())
288 else if (cur
.getKind() == ITE
)
290 // only recurse on relevant branch
291 Node bval
= value
[cur
[0]];
292 Assert(!bval
.isNull() && bval
.isConst());
293 unsigned cindex
= bval
.getConst
<bool>() ? 1 : 2;
294 visit
.push_back(cur
[0]);
295 visit
.push_back(cur
[cindex
]);
297 else if (cur
.getNumChildren() > 0)
299 Kind ck
= cur
.getKind();
300 bool alreadyJustified
= false;
302 // if the operator is an apply uf, check its value
303 if (cur
.getKind() == APPLY_UF
)
305 Node op
= cur
.getOperator();
307 Assert(it
!= value
.end());
308 TNode vop
= it
->second
;
309 if (vop
.getKind() == LAMBDA
)
312 // do iterative partial evaluation on the body of the lambda
314 for (unsigned i
= 0, size
= cur
.getNumChildren(); i
< size
; i
++)
316 it
= value
.find(cur
[i
]);
317 Assert(it
!= value
.end());
318 Node scurr
= curr
.substitute(vop
[0][i
], it
->second
);
319 // if the valuation of the i^th argument changes the
320 // interpretation of the body of the lambda, then the i^th
321 // argument is relevant to the substitution. Hence, we add
322 // i to visit, and update curr below.
325 curr
= Rewriter::rewrite(scurr
);
326 visit
.push_back(cur
[i
]);
329 alreadyJustified
= true;
332 if (!alreadyJustified
)
334 // a subset of the arguments of cur that fully justify the evaluation
335 std::vector
<unsigned> justifyArgs
;
336 if (cur
.getNumChildren() > 1)
338 for (unsigned i
= 0, size
= cur
.getNumChildren(); i
< size
; i
++)
342 Assert(it
!= value
.end());
343 Assert(!it
->second
.isNull());
344 if (isSingularArg(it
->second
, ck
, i
))
346 // have we seen this argument already? if so, we are done
347 if (visited
.find(cn
) != visited
.end())
349 alreadyJustified
= true;
352 justifyArgs
.push_back(i
);
356 // we need to recurse on at most one child
357 if (!alreadyJustified
&& !justifyArgs
.empty())
359 unsigned sindex
= justifyArgs
[0];
360 // could choose a best index, for now, we just take the first
361 visit
.push_back(cur
[sindex
]);
362 alreadyJustified
= true;
365 if (!alreadyJustified
)
367 // must recurse on all arguments, including operator
368 if (cur
.getKind() == APPLY_UF
)
370 visit
.push_back(cur
.getOperator());
372 for (const Node
& cn
: cur
)
379 } while (!visit
.empty());
381 for (const Node
& v
: rlvFv
)
383 Assert(std::find(vars
.begin(), vars
.end(), v
) != vars
.end());
384 reqVars
.push_back(v
);
387 Trace("subs-min") << "... requires " << reqVars
.size() << "/" << vars
.size()
388 << " : " << reqVars
<< std::endl
;
393 bool SubstitutionMinimize::isSingularArg(Node n
, Kind k
, unsigned arg
)
395 // Notice that this function is hardcoded. We could compute this function
396 // in a theory-independent way using partial evaluation. However, we
397 // prefer performance to generality here.
399 // TODO: a variant of this code is implemented in quantifiers::TermUtil.
400 // These implementations should be merged (see #1216).
407 return !n
.getConst
<bool>();
411 return n
.getConst
<bool>();
413 else if (k
== IMPLIES
)
415 return arg
== (n
.getConst
<bool>() ? 1 : 0);
419 && (k
== DIVISION_TOTAL
|| k
== INTS_DIVISION_TOTAL
420 || k
== INTS_MODULUS_TOTAL
))
421 || (arg
== 2 && k
== STRING_SUBSTR
))
424 if (n
.getConst
<Rational
>().sgn() == 0)
429 if (k
== BITVECTOR_AND
|| k
== BITVECTOR_MULT
|| k
== BITVECTOR_UDIV_TOTAL
430 || k
== BITVECTOR_UREM_TOTAL
432 && (k
== BITVECTOR_SHL
|| k
== BITVECTOR_LSHR
433 || k
== BITVECTOR_ASHR
)))
435 if (bv::utils::isZero(n
))
440 if (k
== BITVECTOR_OR
)
443 if (bv::utils::isOnes(n
))
449 if ((arg
== 1 && k
== STRING_STRCTN
) || (arg
== 0 && k
== STRING_SUBSTR
))
452 if (strings::Word::getLength(n
) == 0)
457 if ((arg
!= 0 && k
== STRING_SUBSTR
) || (arg
== 2 && k
== STRING_STRIDOF
))
460 if (n
.getConst
<Rational
>().sgn() < 0)
468 } // namespace theory