1 /********************* */
2 /*! \file unconstrained_simplifier.cpp
4 ** Original author: Clark Barrett
5 ** Major contributors: none
6 ** Minor contributors (to current version): Tim King, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Simplifications based on unconstrained variables
14 ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions
15 ** by variables. Based on Roberto Bruttomesso's PhD thesis.
19 #include "theory/unconstrained_simplifier.h"
20 #include "theory/rewriter.h"
21 #include "theory/logic_info.h"
25 using namespace theory
;
28 UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context
* context
,
29 const LogicInfo
& logicInfo
)
30 : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
31 d_context(context
), d_substitutions(context
), d_logicInfo(logicInfo
)
33 StatisticsRegistry::registerStat(&d_numUnconstrainedElim
);
37 UnconstrainedSimplifier::~UnconstrainedSimplifier()
39 StatisticsRegistry::unregisterStat(&d_numUnconstrainedElim
);
43 struct unc_preprocess_stack_element
{
46 unc_preprocess_stack_element(TNode n
) : node(n
) {}
47 unc_preprocess_stack_element(TNode n
, TNode p
) : node(n
), parent(p
) {}
48 };/* struct unc_preprocess_stack_element */
51 void UnconstrainedSimplifier::visitAll(TNode assertion
)
53 // Do a topological sort of the subexpressions and substitute them
54 vector
<unc_preprocess_stack_element
> toVisit
;
55 toVisit
.push_back(assertion
);
57 while (!toVisit
.empty())
59 // The current node we are processing
60 unc_preprocess_stack_element
& stackHead
= toVisit
.back();
62 TNode current
= stackHead
.node
;
64 TNodeCountMap::iterator find
= d_visited
.find(current
);
65 if (find
!= d_visited
.end()) {
66 if (find
->second
== 1) {
67 d_visitedOnce
.erase(current
);
68 if (current
.isVar()) {
69 d_unconstrained
.erase(current
);
76 d_visited
[current
] = 1;
77 d_visitedOnce
[current
] = stackHead
.parent
;
79 if (current
.getNumChildren() == 0) {
80 if (current
.isVar()) {
81 d_unconstrained
.insert(current
);
85 for(TNode::iterator child_it
= current
.begin(); child_it
!= current
.end(); ++ child_it
) {
86 TNode childNode
= *child_it
;
87 toVisit
.push_back(unc_preprocess_stack_element(childNode
, current
));
93 Node
UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t
, TNode var
)
95 Node n
= NodeManager::currentNM()->mkSkolem("unconstrained", t
, "a new var introduced because of unconstrained variable " + var
.toString());
100 void UnconstrainedSimplifier::processUnconstrained()
102 TNodeSet::iterator it
= d_unconstrained
.begin(), iend
= d_unconstrained
.end();
103 vector
<TNode
> workList
;
104 for ( ; it
!= iend
; ++it
) {
105 workList
.push_back(*it
);
112 vector
<TNode
> delayQueueLeft
;
113 vector
<Node
> delayQueueRight
;
115 TNode current
= workList
.back();
118 Assert(d_visitedOnce
.find(current
) != d_visitedOnce
.end());
119 parent
= d_visitedOnce
[current
];
120 if (!parent
.isNull()) {
121 swap
= isSigned
= strict
= false;
122 switch (parent
.getKind()) {
124 // If-then-else operator - any two unconstrained children makes the parent unconstrained
126 Assert(parent
[0] == current
|| parent
[1] == current
|| parent
[2] == current
);
127 bool uCond
= parent
[0] == current
|| d_unconstrained
.find(parent
[0]) != d_unconstrained
.end();
128 bool uThen
= parent
[1] == current
|| d_unconstrained
.find(parent
[1]) != d_unconstrained
.end();
129 bool uElse
= parent
[2] == current
|| d_unconstrained
.find(parent
[2]) != d_unconstrained
.end();
130 if ((uCond
&& uThen
) || (uCond
&& uElse
) || (uThen
&& uElse
)) {
131 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
132 !d_substitutions
.hasSubstitution(parent
)) {
133 ++d_numUnconstrainedElim
;
135 if (parent
[1] != current
) {
136 if (parent
[1].isVar()) {
137 currentSub
= parent
[1];
140 Assert(d_substitutions
.hasSubstitution(parent
[1]));
141 currentSub
= d_substitutions
.apply(parent
[1]);
144 else if (currentSub
.isNull()) {
145 currentSub
= current
;
148 else if (parent
[2] != current
) {
149 if (parent
[2].isVar()) {
150 currentSub
= parent
[2];
153 Assert(d_substitutions
.hasSubstitution(parent
[2]));
154 currentSub
= d_substitutions
.apply(parent
[2]);
157 else if (currentSub
.isNull()) {
158 currentSub
= current
;
167 Cardinality card
= parent
.getType().getCardinality();
168 if (card
.isFinite() && !card
.isLargeFinite() && card
.getFiniteCardinality() == 2) {
169 // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
172 if (parent
.getType().isBoolean()) {
173 test
= Rewriter::rewrite(parent
[1].iffNode(parent
[2]));
176 test
= Rewriter::rewrite(parent
[1].eqNode(parent
[2]));
178 if (test
== NodeManager::currentNM()->mkConst
<bool>(false)) {
179 ++d_numUnconstrainedElim
;
180 if (currentSub
.isNull()) {
181 currentSub
= current
;
183 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
191 // Comparisons that return a different type - assuming domains are larger than 1, any
192 // unconstrained child makes parent unconstrained as well
194 if (parent
[0].getType() != parent
[1].getType()) {
195 TNode other
= (parent
[0] == current
) ? parent
[1] : parent
[0];
196 if (current
.getType().isSubtypeOf(other
.getType())) {
200 case kind::BITVECTOR_COMP
:
206 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
207 !d_substitutions
.hasSubstitution(parent
)) {
208 ++d_numUnconstrainedElim
;
209 Assert(parent
[0] != parent
[1] &&
210 (parent
[0] == current
|| parent
[1] == current
));
211 if (currentSub
.isNull()) {
212 currentSub
= current
;
214 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
223 // Unary operators that propagate unconstrainedness
225 case kind::BITVECTOR_NOT
:
226 case kind::BITVECTOR_NEG
:
228 ++d_numUnconstrainedElim
;
229 Assert(parent
[0] == current
);
230 if (currentSub
.isNull()) {
231 currentSub
= current
;
236 // Unary operators that propagate unconstrainedness and return a different type
237 case kind::BITVECTOR_EXTRACT
:
238 ++d_numUnconstrainedElim
;
239 Assert(parent
[0] == current
);
240 if (currentSub
.isNull()) {
241 currentSub
= current
;
243 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
247 // Operators returning same type requiring all children to be unconstrained
251 case kind::BITVECTOR_AND
:
252 case kind::BITVECTOR_OR
:
253 case kind::BITVECTOR_NAND
:
254 case kind::BITVECTOR_NOR
:
256 bool allUnconstrained
= true;
257 for(TNode::iterator child_it
= parent
.begin(); child_it
!= parent
.end(); ++child_it
) {
258 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end()) {
259 allUnconstrained
= false;
263 if (allUnconstrained
) {
264 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
265 !d_substitutions
.hasSubstitution(parent
)) {
266 ++d_numUnconstrainedElim
;
267 if (currentSub
.isNull()) {
268 currentSub
= current
;
279 // Require all children to be unconstrained and different
280 case kind::BITVECTOR_SHL
:
281 case kind::BITVECTOR_LSHR
:
282 case kind::BITVECTOR_ASHR
:
283 case kind::BITVECTOR_UDIV
:
284 case kind::BITVECTOR_UREM
:
285 case kind::BITVECTOR_SDIV
:
286 case kind::BITVECTOR_SREM
:
287 case kind::BITVECTOR_SMOD
: {
288 bool allUnconstrained
= true;
289 bool allDifferent
= true;
290 for(TNode::iterator child_it
= parent
.begin(); child_it
!= parent
.end(); ++child_it
) {
291 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end()) {
292 allUnconstrained
= false;
295 for(TNode::iterator child_it2
= child_it
+ 1; child_it2
!= parent
.end(); ++child_it2
) {
296 if (*child_it
== *child_it2
) {
297 allDifferent
= false;
302 if (allUnconstrained
&& allDifferent
) {
303 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
304 !d_substitutions
.hasSubstitution(parent
)) {
305 ++d_numUnconstrainedElim
;
306 if (currentSub
.isNull()) {
307 currentSub
= current
;
318 // Requires all children to be unconstrained and different, and returns a different type
319 case kind::BITVECTOR_CONCAT
:
321 bool allUnconstrained
= true;
322 bool allDifferent
= true;
323 for(TNode::iterator child_it
= parent
.begin(); child_it
!= parent
.end(); ++child_it
) {
324 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end()) {
325 allUnconstrained
= false;
328 for(TNode::iterator child_it2
= child_it
+ 1; child_it2
!= parent
.end(); ++child_it2
) {
329 if (*child_it
== *child_it2
) {
330 allDifferent
= false;
335 if (allUnconstrained
&& allDifferent
) {
336 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
337 !d_substitutions
.hasSubstitution(parent
)) {
338 ++d_numUnconstrainedElim
;
339 if (currentSub
.isNull()) {
340 currentSub
= current
;
342 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
352 // N-ary operators returning same type requiring at least one child to be unconstrained
355 if (current
.getType().isInteger() &&
356 !parent
.getType().isInteger()) {
361 case kind::BITVECTOR_XOR
:
362 case kind::BITVECTOR_XNOR
:
363 case kind::BITVECTOR_PLUS
:
364 case kind::BITVECTOR_SUB
:
365 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
366 !d_substitutions
.hasSubstitution(parent
)) {
367 ++d_numUnconstrainedElim
;
368 if (currentSub
.isNull()) {
369 currentSub
= current
;
378 // Multiplication/division: must be non-integer and other operand must be non-zero
381 Assert(parent
.getNumChildren() == 2);
383 if (parent
[0] == current
) {
387 Assert(parent
[1] == current
);
390 if (d_unconstrained
.find(other
) != d_unconstrained
.end()) {
391 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
392 !d_substitutions
.hasSubstitution(parent
)) {
393 if (current
.getType().isInteger() && other
.getType().isInteger()) {
394 Assert(parent
.getKind() == kind::DIVISION
|| parent
.getType().isInteger());
395 if (parent
.getKind() == kind::DIVISION
) {
399 ++d_numUnconstrainedElim
;
400 if (currentSub
.isNull()) {
401 currentSub
= current
;
410 // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained
411 if (parent
.getKind() == kind::DIVISION
&& current
== parent
[1]) {
414 NodeManager
* nm
= NodeManager::currentNM();
415 // if we are an integer, the only way we are unconstrained is if we are a MULT by -1
416 if (current
.getType().isInteger()) {
417 // div/mult by 1 should have been simplified
418 Assert(other
!= nm
->mkConst
<Rational
>(1));
419 if (other
== nm
->mkConst
<Rational
>(-1)) {
420 // div by -1 should have been simplified
421 Assert(parent
.getKind() == kind::MULT
);
422 Assert(parent
.getType().isInteger());
429 // TODO: could build ITE here
430 Node test
= other
.eqNode(nm
->mkConst
<Rational
>(0));
431 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(false)) {
435 ++d_numUnconstrainedElim
;
436 if (currentSub
.isNull()) {
437 currentSub
= current
;
444 // Bitvector MULT - current must only appear once in the children:
445 // all other children must be unconstrained or odd
446 case kind::BITVECTOR_MULT
:
450 for(TNode::iterator child_it
= parent
.begin(); child_it
!= parent
.end(); ++child_it
) {
451 if ((*child_it
) == current
) {
459 else if (d_unconstrained
.find(*child_it
) != d_unconstrained
.end()) {
463 NodeManager
* nm
= NodeManager::currentNM();
464 Node extractOp
= nm
->mkConst
<BitVectorExtract
>(BitVectorExtract(0,0));
465 vector
<Node
> children
;
466 children
.push_back(*child_it
);
467 Node test
= nm
->mkNode(extractOp
, children
);
468 BitVector
one(1,unsigned(1));
469 test
= test
.eqNode(nm
->mkConst
<BitVector
>(one
));
470 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(true)) {
479 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
480 !d_substitutions
.hasSubstitution(parent
)) {
481 ++d_numUnconstrainedElim
;
482 if (currentSub
.isNull()) {
483 currentSub
= current
;
493 // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained
495 if (d_logicInfo
.isQuantified() || !current
.getType().getCardinality().isInfinite()) {
498 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
499 !d_substitutions
.hasSubstitution(parent
)) {
500 ++d_numUnconstrainedElim
;
501 if (currentSub
.isNull()) {
502 currentSub
= current
;
504 if (parent
.getType() != current
.getType()) {
505 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
514 // Array select - if array is unconstrained, so is result
516 if (parent
[0] == current
) {
517 ++d_numUnconstrainedElim
;
518 Assert(current
.getType().isArray());
519 if (currentSub
.isNull()) {
520 currentSub
= current
;
522 currentSub
= newUnconstrainedVar(current
.getType().getArrayConstituentType(), currentSub
);
527 // Array store - if both store and value are unconstrained, so is resulting store
529 if (((parent
[0] == current
&&
530 d_unconstrained
.find(parent
[2]) != d_unconstrained
.end()) ||
531 (parent
[2] == current
&&
532 d_unconstrained
.find(parent
[0]) != d_unconstrained
.end()))) {
533 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
534 !d_substitutions
.hasSubstitution(parent
)) {
535 ++d_numUnconstrainedElim
;
536 if (parent
[0] != current
) {
537 if (parent
[0].isVar()) {
538 currentSub
= parent
[0];
541 Assert(d_substitutions
.hasSubstitution(parent
[0]));
542 currentSub
= d_substitutions
.apply(parent
[0]);
545 else if (currentSub
.isNull()) {
546 currentSub
= current
;
556 // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition
557 // as there is always one case when the comparison is forced to be false
558 case kind::BITVECTOR_ULT
:
560 case kind::BITVECTOR_UGE
:
563 case kind::BITVECTOR_UGT
:
565 case kind::BITVECTOR_ULE
:
569 case kind::BITVECTOR_SLT
:
571 case kind::BITVECTOR_SGE
:
575 case kind::BITVECTOR_SGT
:
577 case kind::BITVECTOR_SLE
:
584 if (parent
[0] == current
) {
589 Assert(parent
[1] == current
);
592 if (d_unconstrained
.find(other
) != d_unconstrained
.end()) {
593 if (d_unconstrained
.find(parent
) == d_unconstrained
.end() &&
594 !d_substitutions
.hasSubstitution(parent
)) {
595 ++d_numUnconstrainedElim
;
596 if (currentSub
.isNull()) {
597 currentSub
= current
;
599 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
607 unsigned size
= current
.getType().getBitVectorSize();
608 BitVector bv
= isSigned
? BitVector(size
, Integer(1).multiplyByPow2(size
- 1)) : BitVector(size
, unsigned(0));
612 if (currentSub
.isNull()) {
613 currentSub
= current
;
615 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
617 NodeManager
* nm
= NodeManager::currentNM();
618 Node test
= Rewriter::rewrite(other
.eqNode(nm
->mkConst
<BitVector
>(bv
)));
619 if (test
== nm
->mkConst
<bool>(false)) {
623 currentSub
= currentSub
.andNode(test
.notNode());
626 currentSub
= currentSub
.orNode(test
);
628 // Delay adding this substitution - see comment at end of function
629 delayQueueLeft
.push_back(current
);
630 delayQueueRight
.push_back(currentSub
);
637 // These should have been rewritten up front
638 case kind::BITVECTOR_REPEAT
:
639 case kind::BITVECTOR_ZERO_EXTEND
:
640 case kind::BITVECTOR_ROTATE_LEFT
:
641 case kind::BITVECTOR_ROTATE_RIGHT
:
646 case kind::BITVECTOR_SIGN_EXTEND
:
650 if (current
== parent
&& d_visited
[parent
] == 1) {
651 d_unconstrained
.insert(parent
);
655 if (!currentSub
.isNull()) {
656 Assert(currentSub
.isVar());
657 d_substitutions
.addSubstitution(current
, currentSub
, false);
659 if (workList
.empty()) {
662 current
= workList
.back();
668 // All substitutions except those arising from bitvector comparisons are
669 // substitutions t -> x where x is a variable. This allows us to build the
670 // substitution very quickly (never invalidating the substitution cache).
671 // Bitvector comparisons are more complicated and may require
672 // back-substitution and cache-invalidation. So we do these last.
673 while (!delayQueueLeft
.empty()) {
674 left
= delayQueueLeft
.back();
675 if (!d_substitutions
.hasSubstitution(left
)) {
676 right
= d_substitutions
.apply(delayQueueRight
.back());
677 d_substitutions
.addSubstitution(delayQueueLeft
.back(), right
);
679 delayQueueLeft
.pop_back();
680 delayQueueRight
.pop_back();
685 void UnconstrainedSimplifier::processAssertions(vector
<Node
>& assertions
)
689 vector
<Node
>::iterator it
= assertions
.begin(), iend
= assertions
.end();
690 for (; it
!= iend
; ++it
) {
694 if (!d_unconstrained
.empty()) {
695 processUnconstrained();
696 // d_substitutions.print(Message.getStream());
697 for (it
= assertions
.begin(); it
!= iend
; ++it
) {
698 (*it
) = Rewriter::rewrite(d_substitutions
.apply(*it
));
702 // to clear substitutions map
706 d_visitedOnce
.clear();
707 d_unconstrained
.clear();