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 "smt/smt_statistics_registry.h"
22 #include "theory/logic_info.h"
23 #include "theory/rewriter.h"
26 namespace preprocessing
{
29 using namespace CVC4::theory
;
31 UnconstrainedSimplifier::UnconstrainedSimplifier(
32 PreprocessingPassContext
* preprocContext
)
33 : PreprocessingPass(preprocContext
, "unconstrained-simplifier"),
34 d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
35 d_context(preprocContext
->getDecisionContext()),
36 d_substitutions(preprocContext
->getDecisionContext()),
37 d_logicInfo(preprocContext
->getLogicInfo())
39 smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim
);
42 UnconstrainedSimplifier::~UnconstrainedSimplifier()
44 smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim
);
47 struct unc_preprocess_stack_element
51 unc_preprocess_stack_element(TNode n
) : node(n
) {}
52 unc_preprocess_stack_element(TNode n
, TNode p
) : node(n
), parent(p
) {}
53 }; /* struct unc_preprocess_stack_element */
55 void UnconstrainedSimplifier::visitAll(TNode assertion
)
57 // Do a topological sort of the subexpressions and substitute them
58 vector
<unc_preprocess_stack_element
> toVisit
;
59 toVisit
.push_back(assertion
);
61 while (!toVisit
.empty())
63 // The current node we are processing
64 TNode current
= toVisit
.back().node
;
65 TNode parent
= toVisit
.back().parent
;
68 TNodeCountMap::iterator find
= d_visited
.find(current
);
69 if (find
!= d_visited
.end())
71 if (find
->second
== 1)
73 d_visitedOnce
.erase(current
);
76 d_unconstrained
.erase(current
);
80 // Also erase the children from the visited-once set when we visit a
81 // node a second time, otherwise variables in this node are not
82 // erased from the set of unconstrained variables.
83 for (TNode childNode
: current
)
85 toVisit
.push_back(unc_preprocess_stack_element(childNode
, current
));
93 d_visited
[current
] = 1;
94 d_visitedOnce
[current
] = parent
;
96 if (current
.getNumChildren() == 0)
98 if (current
.getKind() == kind::VARIABLE
99 || current
.getKind() == kind::SKOLEM
)
101 d_unconstrained
.insert(current
);
104 else if (current
.isClosure())
106 // Throw an exception. This should never happen in practice unless the
107 // user specifically enabled unconstrained simplification in an illegal
109 throw LogicException(
110 "Cannot use unconstrained simplification in this logic, due to "
111 "(possibly internally introduced) quantified formula.");
115 for (TNode childNode
: current
)
117 toVisit
.push_back(unc_preprocess_stack_element(childNode
, current
));
123 Node
UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t
, TNode var
)
125 Node n
= NodeManager::currentNM()->mkSkolem(
128 "a new var introduced because of unconstrained variable "
133 void UnconstrainedSimplifier::processUnconstrained()
135 NodeManager
* nm
= NodeManager::currentNM();
137 vector
<TNode
> workList(d_unconstrained
.begin(), d_unconstrained
.end());
143 vector
<TNode
> delayQueueLeft
;
144 vector
<Node
> delayQueueRight
;
146 TNode current
= workList
.back();
150 Assert(d_visitedOnce
.find(current
) != d_visitedOnce
.end());
151 parent
= d_visitedOnce
[current
];
152 if (!parent
.isNull())
154 swap
= isSigned
= strict
= false;
155 bool checkParent
= false;
156 switch (parent
.getKind())
158 // If-then-else operator - any two unconstrained children makes the
159 // parent unconstrained
162 Assert(parent
[0] == current
|| parent
[1] == current
163 || parent
[2] == current
);
166 || d_unconstrained
.find(parent
[0]) != d_unconstrained
.end();
169 || d_unconstrained
.find(parent
[1]) != d_unconstrained
.end();
172 || d_unconstrained
.find(parent
[2]) != d_unconstrained
.end();
173 if ((uCond
&& uThen
) || (uCond
&& uElse
) || (uThen
&& uElse
))
175 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
176 && !d_substitutions
.hasSubstitution(parent
))
178 ++d_numUnconstrainedElim
;
181 if (parent
[1] != current
)
183 if (parent
[1].isVar())
185 currentSub
= parent
[1];
189 Assert(d_substitutions
.hasSubstitution(parent
[1]));
190 currentSub
= d_substitutions
.apply(parent
[1]);
193 else if (currentSub
.isNull())
195 currentSub
= current
;
198 else if (parent
[2] != current
)
200 if (parent
[2].isVar())
202 currentSub
= parent
[2];
206 Assert(d_substitutions
.hasSubstitution(parent
[2]));
207 currentSub
= d_substitutions
.apply(parent
[2]);
210 else if (currentSub
.isNull())
212 currentSub
= current
;
223 Cardinality card
= parent
.getType().getCardinality();
224 if (card
.isFinite() && !card
.isLargeFinite()
225 && card
.getFiniteCardinality() == 2)
227 // Special case: condition is unconstrained, then and else are
228 // different, and total cardinality of the type is 2, then the
229 // result is unconstrained
230 Node test
= Rewriter::rewrite(parent
[1].eqNode(parent
[2]));
231 if (test
== nm
->mkConst
<bool>(false))
233 ++d_numUnconstrainedElim
;
234 if (currentSub
.isNull())
236 currentSub
= current
;
238 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
246 // Comparisons that return a different type - assuming domains are
247 // larger than 1, any unconstrained child makes parent unconstrained as
250 if (parent
[0].getType() != parent
[1].getType())
252 TNode other
= (parent
[0] == current
) ? parent
[1] : parent
[0];
253 if (current
.getType().isSubtypeOf(other
.getType()))
258 if (parent
[0].getType().getCardinality().isOne())
262 if (parent
[0].getType().isDatatype())
264 TypeNode tn
= parent
[0].getType();
265 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
266 if (dt
.isRecursiveSingleton(tn
.toType()))
268 // domain size may be 1
272 if (parent
[0].getType().isBoolean())
278 case kind::BITVECTOR_COMP
:
284 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
285 && !d_substitutions
.hasSubstitution(parent
))
287 ++d_numUnconstrainedElim
;
288 Assert(parent
[0] != parent
[1]
289 && (parent
[0] == current
|| parent
[1] == current
));
290 if (currentSub
.isNull())
292 currentSub
= current
;
294 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
304 // Unary operators that propagate unconstrainedness
306 case kind::BITVECTOR_NOT
:
307 case kind::BITVECTOR_NEG
:
309 ++d_numUnconstrainedElim
;
310 Assert(parent
[0] == current
);
311 if (currentSub
.isNull())
313 currentSub
= current
;
318 // Unary operators that propagate unconstrainedness and return a
320 case kind::BITVECTOR_EXTRACT
:
321 ++d_numUnconstrainedElim
;
322 Assert(parent
[0] == current
);
323 if (currentSub
.isNull())
325 currentSub
= current
;
327 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
331 // Operators returning same type requiring all children to be
336 case kind::BITVECTOR_AND
:
337 case kind::BITVECTOR_OR
:
338 case kind::BITVECTOR_NAND
:
339 case kind::BITVECTOR_NOR
:
341 bool allUnconstrained
= true;
342 for (TNode child
: parent
)
344 if (d_unconstrained
.find(child
) == d_unconstrained
.end())
346 allUnconstrained
= false;
350 if (allUnconstrained
)
357 // Require all children to be unconstrained and different
358 case kind::BITVECTOR_SHL
:
359 case kind::BITVECTOR_LSHR
:
360 case kind::BITVECTOR_ASHR
:
361 case kind::BITVECTOR_UDIV_TOTAL
:
362 case kind::BITVECTOR_UREM_TOTAL
:
363 case kind::BITVECTOR_SDIV
:
364 case kind::BITVECTOR_SREM
:
365 case kind::BITVECTOR_SMOD
:
367 bool allUnconstrained
= true;
368 bool allDifferent
= true;
369 for (TNode::iterator child_it
= parent
.begin();
370 child_it
!= parent
.end();
373 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end())
375 allUnconstrained
= false;
378 for (TNode::iterator child_it2
= child_it
+ 1;
379 child_it2
!= parent
.end();
382 if (*child_it
== *child_it2
)
384 allDifferent
= false;
389 if (allUnconstrained
&& allDifferent
)
396 // Requires all children to be unconstrained and different, and returns
398 case kind::BITVECTOR_CONCAT
:
400 bool allUnconstrained
= true;
401 bool allDifferent
= true;
402 for (TNode::iterator child_it
= parent
.begin();
403 child_it
!= parent
.end();
406 if (d_unconstrained
.find(*child_it
) == d_unconstrained
.end())
408 allUnconstrained
= false;
411 for (TNode::iterator child_it2
= child_it
+ 1;
412 child_it2
!= parent
.end();
415 if (*child_it
== *child_it2
)
417 allDifferent
= false;
422 if (allUnconstrained
&& allDifferent
)
424 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
425 && !d_substitutions
.hasSubstitution(parent
))
427 ++d_numUnconstrainedElim
;
428 if (currentSub
.isNull())
430 currentSub
= current
;
432 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
443 // N-ary operators returning same type requiring at least one child to
447 if (current
.getType().isInteger() && !parent
.getType().isInteger())
453 case kind::BITVECTOR_XOR
:
454 case kind::BITVECTOR_XNOR
:
455 case kind::BITVECTOR_PLUS
:
456 case kind::BITVECTOR_SUB
: checkParent
= true; break;
458 // Multiplication/division: must be non-integer and other operand must
463 Assert(parent
.getNumChildren() == 2);
465 if (parent
[0] == current
)
471 Assert(parent
[1] == current
);
474 if (d_unconstrained
.find(other
) != d_unconstrained
.end())
476 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
477 && !d_substitutions
.hasSubstitution(parent
))
479 if (current
.getType().isInteger() && other
.getType().isInteger())
481 Assert(parent
.getKind() == kind::DIVISION
482 || parent
.getType().isInteger());
483 if (parent
.getKind() == kind::DIVISION
)
488 ++d_numUnconstrainedElim
;
489 if (currentSub
.isNull())
491 currentSub
= current
;
502 // if only the denominator of a division is unconstrained, can't
503 // set it to 0 so the result is not unconstrained
504 if (parent
.getKind() == kind::DIVISION
&& current
== parent
[1])
508 // if we are an integer, the only way we are unconstrained is if
509 // we are a MULT by -1
510 if (current
.getType().isInteger())
512 // div/mult by 1 should have been simplified
513 Assert(other
!= nm
->mkConst
<Rational
>(1));
514 // div by -1 should have been simplified
515 if (other
!= nm
->mkConst
<Rational
>(-1))
521 Assert(parent
.getKind() == kind::MULT
);
522 Assert(parent
.getType().isInteger());
527 // TODO(#2377): could build ITE here
528 Node test
= other
.eqNode(nm
->mkConst
<Rational
>(0));
529 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(false))
534 ++d_numUnconstrainedElim
;
535 if (currentSub
.isNull())
537 currentSub
= current
;
544 // Bitvector MULT - current must only appear once in the children:
545 // all other children must be unconstrained or odd
546 case kind::BITVECTOR_MULT
:
551 for (TNode child
: parent
)
553 if (child
== current
)
563 else if (d_unconstrained
.find(child
) == d_unconstrained
.end())
566 nm
->mkConst
<BitVectorExtract
>(BitVectorExtract(0, 0));
567 vector
<Node
> children
;
568 children
.push_back(child
);
569 Node test
= nm
->mkNode(extractOp
, children
);
570 BitVector
one(1, unsigned(1));
571 test
= test
.eqNode(nm
->mkConst
<BitVector
>(one
));
572 if (Rewriter::rewrite(test
) != nm
->mkConst
<bool>(true))
587 // Uninterpreted function - if domain is infinite, no quantifiers are
588 // used, and any child is unconstrained, result is unconstrained
590 if (d_logicInfo
.isQuantified()
591 || !current
.getType().getCardinality().isInfinite())
595 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
596 && !d_substitutions
.hasSubstitution(parent
))
598 ++d_numUnconstrainedElim
;
599 if (currentSub
.isNull())
601 currentSub
= current
;
603 // always introduce a new variable; it is unsound to try to reuse
604 // currentSub as the variable, see issue #4469.
605 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
614 // Array select - if array is unconstrained, so is result
616 if (parent
[0] == current
)
618 ++d_numUnconstrainedElim
;
619 Assert(current
.getType().isArray());
620 if (currentSub
.isNull())
622 currentSub
= current
;
624 currentSub
= newUnconstrainedVar(
625 current
.getType().getArrayConstituentType(), currentSub
);
630 // Array store - if both store and value are unconstrained, so is
633 if (((parent
[0] == current
634 && d_unconstrained
.find(parent
[2]) != d_unconstrained
.end())
635 || (parent
[2] == current
636 && d_unconstrained
.find(parent
[0])
637 != d_unconstrained
.end())))
639 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
640 && !d_substitutions
.hasSubstitution(parent
))
642 ++d_numUnconstrainedElim
;
643 if (parent
[0] != current
)
645 if (parent
[0].isVar())
647 currentSub
= parent
[0];
651 Assert(d_substitutions
.hasSubstitution(parent
[0]));
652 currentSub
= d_substitutions
.apply(parent
[0]);
655 else if (currentSub
.isNull())
657 currentSub
= current
;
668 // Bit-vector comparisons: replace with new Boolean variable, but have
669 // to also conjoin with a side condition as there is always one case
670 // when the comparison is forced to be false
671 case kind::BITVECTOR_ULT
:
672 case kind::BITVECTOR_UGE
:
673 case kind::BITVECTOR_UGT
:
674 case kind::BITVECTOR_ULE
:
675 case kind::BITVECTOR_SLT
:
676 case kind::BITVECTOR_SGE
:
677 case kind::BITVECTOR_SGT
:
678 case kind::BITVECTOR_SLE
:
680 // Tuples over (signed, swap, strict).
681 switch (parent
.getKind())
683 case kind::BITVECTOR_UGE
: break;
684 case kind::BITVECTOR_ULT
: strict
= true; break;
685 case kind::BITVECTOR_ULE
: swap
= true; break;
686 case kind::BITVECTOR_UGT
:
690 case kind::BITVECTOR_SGE
: isSigned
= true; break;
691 case kind::BITVECTOR_SLT
:
695 case kind::BITVECTOR_SLE
:
699 case kind::BITVECTOR_SGT
:
704 default: Unreachable();
708 if (parent
[0] == current
)
715 Assert(parent
[1] == current
);
718 if (d_unconstrained
.find(other
) != d_unconstrained
.end())
720 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
721 && !d_substitutions
.hasSubstitution(parent
))
723 ++d_numUnconstrainedElim
;
724 if (currentSub
.isNull())
726 currentSub
= current
;
728 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
738 unsigned size
= current
.getType().getBitVectorSize();
740 isSigned
? BitVector(size
, Integer(1).multiplyByPow2(size
- 1))
741 : BitVector(size
, unsigned(0));
746 if (currentSub
.isNull())
748 currentSub
= current
;
750 currentSub
= newUnconstrainedVar(parent
.getType(), currentSub
);
753 Rewriter::rewrite(other
.eqNode(nm
->mkConst
<BitVector
>(bv
)));
754 if (test
== nm
->mkConst
<bool>(false))
758 currentSub
= strict
? currentSub
.andNode(test
.notNode())
759 : currentSub
.orNode(test
);
760 // Delay adding this substitution - see comment at end of function
761 delayQueueLeft
.push_back(current
);
762 delayQueueRight
.push_back(currentSub
);
770 case kind::BITVECTOR_SIGN_EXTEND
:
771 case kind::BITVECTOR_ZERO_EXTEND
:
772 case kind::BITVECTOR_REPEAT
:
773 case kind::BITVECTOR_ROTATE_LEFT
:
774 case kind::BITVECTOR_ROTATE_RIGHT
:
780 // run for various cases from above
781 if (d_unconstrained
.find(parent
) == d_unconstrained
.end()
782 && !d_substitutions
.hasSubstitution(parent
))
784 ++d_numUnconstrainedElim
;
785 if (currentSub
.isNull())
787 currentSub
= current
;
796 if (current
== parent
&& d_visited
[parent
] == 1)
798 d_unconstrained
.insert(parent
);
802 if (!currentSub
.isNull())
805 << "UnconstrainedSimplifier::processUnconstrained: introduce "
806 << currentSub
<< " for " << current
<< ", parent " << parent
808 Assert(currentSub
.isVar());
809 d_substitutions
.addSubstitution(current
, currentSub
, false);
811 if (workList
.empty())
815 current
= workList
.back();
821 // All substitutions except those arising from bitvector comparisons are
822 // substitutions t -> x where x is a variable. This allows us to build the
823 // substitution very quickly (never invalidating the substitution cache).
824 // Bitvector comparisons are more complicated and may require
825 // back-substitution and cache-invalidation. So we do these last.
826 while (!delayQueueLeft
.empty())
828 left
= delayQueueLeft
.back();
829 if (!d_substitutions
.hasSubstitution(left
))
831 right
= d_substitutions
.apply(delayQueueRight
.back());
832 d_substitutions
.addSubstitution(delayQueueLeft
.back(), right
);
834 delayQueueLeft
.pop_back();
835 delayQueueRight
.pop_back();
839 PreprocessingPassResult
UnconstrainedSimplifier::applyInternal(
840 AssertionPipeline
* assertionsToPreprocess
)
842 d_preprocContext
->spendResource(ResourceManager::Resource::PreprocessStep
);
844 std::vector
<Node
>& assertions
= assertionsToPreprocess
->ref();
848 for (const Node
& assertion
: assertions
)
853 if (!d_unconstrained
.empty())
855 processUnconstrained();
856 // d_substitutions.print(Message.getStream());
857 for (Node
& assertion
: assertions
)
859 assertion
= Rewriter::rewrite(d_substitutions
.apply(assertion
));
863 // to clear substitutions map
867 d_visitedOnce
.clear();
868 d_unconstrained
.clear();
870 return PreprocessingPassResult::NO_CONFLICT
;
874 } // namespace passes
875 } // namespace preprocessing