1 /********************* */
2 /*! \file unconstrained_simplifier.cpp
4 ** Top contributors (to current version):
5 ** Clark Barrett, Andres Noetzli, Andrew Reynolds
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 Simplifications based on unconstrained variables
14 ** This module implements a preprocessing phase which replaces certain
15 ** "unconstrained" expressions by variables. Based on Roberto
16 ** Bruttomesso's PhD thesis.
19 #include "preprocessing/passes/unconstrained_simplifier.h"
21 #include "expr/dtype.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/logic_info.h"
24 #include "theory/rewriter.h"
27 namespace preprocessing
{
30 using namespace CVC4::theory
;
32 UnconstrainedSimplifier::UnconstrainedSimplifier(
33 PreprocessingPassContext
* preprocContext
)
34 : PreprocessingPass(preprocContext
, "unconstrained-simplifier"),
35 d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
36 d_context(preprocContext
->getDecisionContext()),
37 d_substitutions(preprocContext
->getDecisionContext()),
38 d_logicInfo(preprocContext
->getLogicInfo())
40 smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim
);
43 UnconstrainedSimplifier::~UnconstrainedSimplifier()
45 smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim
);
48 struct unc_preprocess_stack_element
52 unc_preprocess_stack_element(TNode n
) : node(n
) {}
53 unc_preprocess_stack_element(TNode n
, TNode p
) : node(n
), parent(p
) {}
54 }; /* struct unc_preprocess_stack_element */
56 void UnconstrainedSimplifier::visitAll(TNode assertion
)
58 // Do a topological sort of the subexpressions and substitute them
59 vector
<unc_preprocess_stack_element
> toVisit
;
60 toVisit
.push_back(assertion
);
62 while (!toVisit
.empty())
64 // The current node we are processing
65 TNode current
= toVisit
.back().node
;
66 TNode parent
= toVisit
.back().parent
;
69 TNodeCountMap::iterator find
= d_visited
.find(current
);
70 if (find
!= d_visited
.end())
72 if (find
->second
== 1)
74 d_visitedOnce
.erase(current
);
77 d_unconstrained
.erase(current
);
81 // Also erase the children from the visited-once set when we visit a
82 // node a second time, otherwise variables in this node are not
83 // erased from the set of unconstrained variables.
84 for (TNode childNode
: current
)
86 toVisit
.push_back(unc_preprocess_stack_element(childNode
, current
));
94 d_visited
[current
] = 1;
95 d_visitedOnce
[current
] = parent
;
97 if (current
.getNumChildren() == 0)
99 if (current
.getKind() == kind::VARIABLE
100 || current
.getKind() == kind::SKOLEM
)
102 d_unconstrained
.insert(current
);
105 else if (current
.isClosure())
107 // Throw an exception. This should never happen in practice unless the
108 // user specifically enabled unconstrained simplification in an illegal
110 throw LogicException(
111 "Cannot use unconstrained simplification in this logic, due to "
112 "(possibly internally introduced) quantified formula.");
116 for (TNode childNode
: current
)
118 toVisit
.push_back(unc_preprocess_stack_element(childNode
, current
));
124 Node
UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t
, TNode var
)
126 Node n
= NodeManager::currentNM()->mkSkolem(
129 "a new var introduced because of unconstrained variable "
134 void UnconstrainedSimplifier::processUnconstrained()
136 NodeManager
* nm
= NodeManager::currentNM();
138 vector
<TNode
> workList(d_unconstrained
.begin(), d_unconstrained
.end());
144 vector
<TNode
> delayQueueLeft
;
145 vector
<Node
> delayQueueRight
;
147 TNode current
= workList
.back();
151 Assert(d_visitedOnce
.find(current
) != d_visitedOnce
.end());
152 parent
= d_visitedOnce
[current
];
153 if (!parent
.isNull())
155 swap
= isSigned
= strict
= false;
156 bool checkParent
= false;
157 switch (parent
.getKind())
159 // If-then-else operator - any two unconstrained children makes the
160 // parent unconstrained
163 Assert(parent
[0] == current
|| parent
[1] == current
164 || parent
[2] == current
);
167 || d_unconstrained
.find(parent
[0]) != d_unconstrained
.end();
170 || d_unconstrained
.find(parent
[1]) != d_unconstrained
.end();
173 || d_unconstrained
.find(parent
[2]) != d_unconstrained
.end();
174 if ((uCond
&& uThen
) || (uCond
&& uElse
) || (uThen
&& uElse
))
176 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
177 && !d_substitutions
.hasSubstitution(parent
))
179 ++d_numUnconstrainedElim
;
182 if (parent
[1] != current
)
184 if (parent
[1].isVar())
186 currentSub
= parent
[1];
190 Assert(d_substitutions
.hasSubstitution(parent
[1]));
191 currentSub
= d_substitutions
.apply(parent
[1]);
194 else if (currentSub
.isNull())
196 currentSub
= current
;
199 else if (parent
[2] != current
)
201 if (parent
[2].isVar())
203 currentSub
= parent
[2];
207 Assert(d_substitutions
.hasSubstitution(parent
[2]));
208 currentSub
= d_substitutions
.apply(parent
[2]);
211 else if (currentSub
.isNull())
213 currentSub
= current
;
224 Cardinality card
= parent
.getType().getCardinality();
225 if (card
.isFinite() && !card
.isLargeFinite()
226 && card
.getFiniteCardinality() == 2)
228 // Special case: condition is unconstrained, then and else are
229 // different, and total cardinality of the type is 2, then the
230 // result is unconstrained
231 Node test
= Rewriter::rewrite(parent
[1].eqNode(parent
[2]));
232 if (test
== nm
->mkConst
<bool>(false))
234 ++d_numUnconstrainedElim
;
235 if (currentSub
.isNull())
237 currentSub
= current
;
239 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
247 // Comparisons that return a different type - assuming domains are
248 // larger than 1, any unconstrained child makes parent unconstrained as
251 if (parent
[0].getType() != parent
[1].getType())
253 TNode other
= (parent
[0] == current
) ? parent
[1] : parent
[0];
254 if (current
.getType().isSubtypeOf(other
.getType()))
259 if (parent
[0].getType().getCardinality().isOne())
263 if (parent
[0].getType().isDatatype())
265 TypeNode tn
= parent
[0].getType();
266 const DType
& dt
= tn
.getDType();
267 if (dt
.isRecursiveSingleton(tn
))
269 // domain size may be 1
273 if (parent
[0].getType().isBoolean())
279 case kind::BITVECTOR_COMP
:
285 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
286 && !d_substitutions
.hasSubstitution(parent
))
288 ++d_numUnconstrainedElim
;
289 Assert(parent
[0] != parent
[1]
290 && (parent
[0] == current
|| parent
[1] == current
));
291 if (currentSub
.isNull())
293 currentSub
= current
;
295 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
305 // Unary operators that propagate unconstrainedness
307 case kind::BITVECTOR_NOT
:
308 case kind::BITVECTOR_NEG
:
310 ++d_numUnconstrainedElim
;
311 Assert(parent
[0] == current
);
312 if (currentSub
.isNull())
314 currentSub
= current
;
319 // Unary operators that propagate unconstrainedness and return a
321 case kind::BITVECTOR_EXTRACT
:
322 ++d_numUnconstrainedElim
;
323 Assert(parent
[0] == current
);
324 if (currentSub
.isNull())
326 currentSub
= current
;
328 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
332 // Operators returning same type requiring all children to be
337 case kind::BITVECTOR_AND
:
338 case kind::BITVECTOR_OR
:
339 case kind::BITVECTOR_NAND
:
340 case kind::BITVECTOR_NOR
:
342 bool allUnconstrained
= true;
343 for (TNode child
: parent
)
345 if (d_unconstrained
.find(child
) == d_unconstrained
.end())
347 allUnconstrained
= false;
351 if (allUnconstrained
)
358 // Require all children to be unconstrained and different
359 case kind::BITVECTOR_SHL
:
360 case kind::BITVECTOR_LSHR
:
361 case kind::BITVECTOR_ASHR
:
362 case kind::BITVECTOR_UDIV_TOTAL
:
363 case kind::BITVECTOR_UREM_TOTAL
:
364 case kind::BITVECTOR_SDIV
:
365 case kind::BITVECTOR_SREM
:
366 case kind::BITVECTOR_SMOD
:
368 bool allUnconstrained
= true;
369 bool allDifferent
= true;
370 for (TNode::iterator child_it
= parent
.begin();
371 child_it
!= parent
.end();
374 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end())
376 allUnconstrained
= false;
379 for (TNode::iterator child_it2
= child_it
+ 1;
380 child_it2
!= parent
.end();
383 if (*child_it
== *child_it2
)
385 allDifferent
= false;
390 if (allUnconstrained
&& allDifferent
)
397 // Requires all children to be unconstrained and different, and returns
399 case kind::BITVECTOR_CONCAT
:
401 bool allUnconstrained
= true;
402 bool allDifferent
= true;
403 for (TNode::iterator child_it
= parent
.begin();
404 child_it
!= parent
.end();
407 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end())
409 allUnconstrained
= false;
412 for (TNode::iterator child_it2
= child_it
+ 1;
413 child_it2
!= parent
.end();
416 if (*child_it
== *child_it2
)
418 allDifferent
= false;
423 if (allUnconstrained
&& allDifferent
)
425 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
426 && !d_substitutions
.hasSubstitution(parent
))
428 ++d_numUnconstrainedElim
;
429 if (currentSub
.isNull())
431 currentSub
= current
;
433 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
444 // N-ary operators returning same type requiring at least one child to
448 if (current
.getType().isInteger() && !parent
.getType().isInteger())
454 case kind::BITVECTOR_XOR
:
455 case kind::BITVECTOR_XNOR
:
456 case kind::BITVECTOR_PLUS
:
457 case kind::BITVECTOR_SUB
: checkParent
= true; break;
459 // Multiplication/division: must be non-integer and other operand must
464 Assert(parent
.getNumChildren() == 2);
466 if (parent
[0] == current
)
472 Assert(parent
[1] == current
);
475 if (d_unconstrained
.find(other
) != d_unconstrained
.end())
477 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
478 && !d_substitutions
.hasSubstitution(parent
))
480 if (current
.getType().isInteger() && other
.getType().isInteger())
482 Assert(parent
.getKind() == kind::DIVISION
483 || parent
.getType().isInteger());
484 if (parent
.getKind() == kind::DIVISION
)
489 ++d_numUnconstrainedElim
;
490 if (currentSub
.isNull())
492 currentSub
= current
;
503 // if only the denominator of a division is unconstrained, can't
504 // set it to 0 so the result is not unconstrained
505 if (parent
.getKind() == kind::DIVISION
&& current
== parent
[1])
509 // if we are an integer, the only way we are unconstrained is if
510 // we are a MULT by -1
511 if (current
.getType().isInteger())
513 // div/mult by 1 should have been simplified
514 Assert(other
!= nm
->mkConst
<Rational
>(1));
515 // div by -1 should have been simplified
516 if (other
!= nm
->mkConst
<Rational
>(-1))
522 Assert(parent
.getKind() == kind::MULT
);
523 Assert(parent
.getType().isInteger());
528 // TODO(#2377): could build ITE here
529 Node test
= other
.eqNode(nm
->mkConst
<Rational
>(0));
530 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(false))
535 ++d_numUnconstrainedElim
;
536 if (currentSub
.isNull())
538 currentSub
= current
;
545 // Bitvector MULT - current must only appear once in the children:
546 // all other children must be unconstrained or odd
547 case kind::BITVECTOR_MULT
:
552 for (TNode child
: parent
)
554 if (child
== current
)
564 else if (d_unconstrained
.find(child
) == d_unconstrained
.end())
567 nm
->mkConst
<BitVectorExtract
>(BitVectorExtract(0, 0));
568 vector
<Node
> children
;
569 children
.push_back(child
);
570 Node test
= nm
->mkNode(extractOp
, children
);
571 BitVector
one(1, unsigned(1));
572 test
= test
.eqNode(nm
->mkConst
<BitVector
>(one
));
573 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(true))
588 // Uninterpreted function - if domain is infinite, no quantifiers are
589 // used, and any child is unconstrained, result is unconstrained
591 if (d_logicInfo
.isQuantified()
592 || !current
.getType().getCardinality().isInfinite())
596 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
597 && !d_substitutions
.hasSubstitution(parent
))
599 ++d_numUnconstrainedElim
;
600 if (currentSub
.isNull())
602 currentSub
= current
;
604 // always introduce a new variable; it is unsound to try to reuse
605 // currentSub as the variable, see issue #4469.
606 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
615 // Array select - if array is unconstrained, so is result
617 if (parent
[0] == current
)
619 ++d_numUnconstrainedElim
;
620 Assert(current
.getType().isArray());
621 if (currentSub
.isNull())
623 currentSub
= current
;
625 currentSub
= newUnconstrainedVar(
626 current
.getType().getArrayConstituentType(), currentSub
);
631 // Array store - if both store and value are unconstrained, so is
634 if (((parent
[0] == current
635 && d_unconstrained
.find(parent
[2]) != d_unconstrained
.end())
636 || (parent
[2] == current
637 && d_unconstrained
.find(parent
[0])
638 != d_unconstrained
.end())))
640 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
641 && !d_substitutions
.hasSubstitution(parent
))
643 ++d_numUnconstrainedElim
;
644 if (parent
[0] != current
)
646 if (parent
[0].isVar())
648 currentSub
= parent
[0];
652 Assert(d_substitutions
.hasSubstitution(parent
[0]));
653 currentSub
= d_substitutions
.apply(parent
[0]);
656 else if (currentSub
.isNull())
658 currentSub
= current
;
669 // Bit-vector comparisons: replace with new Boolean variable, but have
670 // to also conjoin with a side condition as there is always one case
671 // when the comparison is forced to be false
672 case kind::BITVECTOR_ULT
:
673 case kind::BITVECTOR_UGE
:
674 case kind::BITVECTOR_UGT
:
675 case kind::BITVECTOR_ULE
:
676 case kind::BITVECTOR_SLT
:
677 case kind::BITVECTOR_SGE
:
678 case kind::BITVECTOR_SGT
:
679 case kind::BITVECTOR_SLE
:
681 // Tuples over (signed, swap, strict).
682 switch (parent
.getKind())
684 case kind::BITVECTOR_UGE
: break;
685 case kind::BITVECTOR_ULT
: strict
= true; break;
686 case kind::BITVECTOR_ULE
: swap
= true; break;
687 case kind::BITVECTOR_UGT
:
691 case kind::BITVECTOR_SGE
: isSigned
= true; break;
692 case kind::BITVECTOR_SLT
:
696 case kind::BITVECTOR_SLE
:
700 case kind::BITVECTOR_SGT
:
705 default: Unreachable();
709 if (parent
[0] == current
)
716 Assert(parent
[1] == current
);
719 if (d_unconstrained
.find(other
) != d_unconstrained
.end())
721 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
722 && !d_substitutions
.hasSubstitution(parent
))
724 ++d_numUnconstrainedElim
;
725 if (currentSub
.isNull())
727 currentSub
= current
;
729 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
739 unsigned size
= current
.getType().getBitVectorSize();
741 isSigned
? BitVector(size
, Integer(1).multiplyByPow2(size
- 1))
742 : BitVector(size
, unsigned(0));
747 if (currentSub
.isNull())
749 currentSub
= current
;
751 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
754 Rewriter::rewrite(other
.eqNode(nm
->mkConst
<BitVector
>(bv
)));
755 if (test
== nm
->mkConst
<bool>(false))
759 currentSub
= strict
? currentSub
.andNode(test
.notNode())
760 : currentSub
.orNode(test
);
761 // Delay adding this substitution - see comment at end of function
762 delayQueueLeft
.push_back(current
);
763 delayQueueRight
.push_back(currentSub
);
771 case kind::BITVECTOR_SIGN_EXTEND
:
772 case kind::BITVECTOR_ZERO_EXTEND
:
773 case kind::BITVECTOR_REPEAT
:
774 case kind::BITVECTOR_ROTATE_LEFT
:
775 case kind::BITVECTOR_ROTATE_RIGHT
:
781 // run for various cases from above
782 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
783 && !d_substitutions
.hasSubstitution(parent
))
785 ++d_numUnconstrainedElim
;
786 if (currentSub
.isNull())
788 currentSub
= current
;
797 if (current
== parent
&& d_visited
[parent
] == 1)
799 d_unconstrained
.insert(parent
);
803 if (!currentSub
.isNull())
806 << "UnconstrainedSimplifier::processUnconstrained: introduce "
807 << currentSub
<< " for " << current
<< ", parent " << parent
809 Assert(currentSub
.isVar());
810 d_substitutions
.addSubstitution(current
, currentSub
, false);
812 if (workList
.empty())
816 current
= workList
.back();
822 // All substitutions except those arising from bitvector comparisons are
823 // substitutions t -> x where x is a variable. This allows us to build the
824 // substitution very quickly (never invalidating the substitution cache).
825 // Bitvector comparisons are more complicated and may require
826 // back-substitution and cache-invalidation. So we do these last.
827 while (!delayQueueLeft
.empty())
829 left
= delayQueueLeft
.back();
830 if (!d_substitutions
.hasSubstitution(left
))
832 right
= d_substitutions
.apply(delayQueueRight
.back());
833 d_substitutions
.addSubstitution(delayQueueLeft
.back(), right
);
835 delayQueueLeft
.pop_back();
836 delayQueueRight
.pop_back();
840 PreprocessingPassResult
UnconstrainedSimplifier::applyInternal(
841 AssertionPipeline
* assertionsToPreprocess
)
843 d_preprocContext
->spendResource(ResourceManager::Resource::PreprocessStep
);
845 const std::vector
<Node
>& assertions
= assertionsToPreprocess
->ref();
849 for (const Node
& assertion
: assertions
)
854 if (!d_unconstrained
.empty())
856 processUnconstrained();
857 // d_substitutions.print(Message.getStream());
858 for (size_t i
= 0, asize
= assertions
.size(); i
< asize
; ++i
)
860 Node a
= assertions
[i
];
861 Node as
= Rewriter::rewrite(d_substitutions
.apply(a
));
862 // replace the assertion
863 assertionsToPreprocess
->replace(i
, as
);
867 // to clear substitutions map
871 d_visitedOnce
.clear();
872 d_unconstrained
.clear();
874 return PreprocessingPassResult::NO_CONFLICT
;
878 } // namespace passes
879 } // namespace preprocessing