1 /********************* */
2 /*! \file ite_utilities.h
4 ** Top contributors (to current version):
5 ** Tim King, Paul Meng, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 for ITE expressions
14 ** This module implements preprocessing phases designed to simplify ITE
15 ** expressions. Based on:
16 ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
17 ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
20 #include "cvc4_private.h"
22 #ifndef __CVC4__ITE_UTILITIES_H
23 #define __CVC4__ITE_UTILITIES_H
25 #include <unordered_map>
28 #include "expr/node.h"
29 #include "util/hash.h"
30 #include "util/statistics_registry.h"
35 class IncomingArcCounter
;
36 class TermITEHeightCounter
;
39 class ITECareSimplifier
;
42 * A caching visitor that computes whether a node contains a term ite.
44 class ContainsTermITEVisitor
{
46 ContainsTermITEVisitor();
47 ~ContainsTermITEVisitor();
49 /** returns true if a node contains a term ite. */
50 bool containsTermITE(TNode n
);
52 /** Garbage collects the cache. */
53 void garbageCollect();
55 /** returns the size of the cache. */
56 size_t cache_size() const { return d_cache
.size(); }
59 typedef std::unordered_map
<Node
, bool, NodeHashFunction
> NodeBoolMap
;
69 Node
simpITE(TNode assertion
);
71 bool simpIteDidALotOfWorkHeuristic() const;
73 /* returns false if an assertion is discovered to be equal to false. */
74 bool compress(std::vector
<Node
>& assertions
);
76 Node
simplifyWithCare(TNode e
);
80 ContainsTermITEVisitor
* getContainsVisitor()
82 return d_containsVisitor
.get();
85 bool containsTermITE(TNode n
)
87 return d_containsVisitor
->containsTermITE(n
);
91 std::unique_ptr
<ContainsTermITEVisitor
> d_containsVisitor
;
92 ITECompressor
* d_compressor
;
93 ITESimplifier
* d_simplifier
;
94 ITECareSimplifier
* d_careSimp
;
97 class IncomingArcCounter
{
99 IncomingArcCounter(bool skipVars
= false, bool skipConstants
= false);
100 ~IncomingArcCounter();
101 void computeReachability(const std::vector
<Node
>& assertions
);
103 inline uint32_t lookupIncoming(Node n
) const {
104 NodeCountMap::const_iterator it
= d_reachCount
.find(n
);
105 if(it
== d_reachCount
.end()){
113 typedef std::unordered_map
<Node
, uint32_t, NodeHashFunction
> NodeCountMap
;
114 NodeCountMap d_reachCount
;
116 bool d_skipVariables
;
117 bool d_skipConstants
;
120 class TermITEHeightCounter
{
122 TermITEHeightCounter();
123 ~TermITEHeightCounter();
126 * Compute and [potentially] cache the termITEHeight() of e.
127 * The term ite height equals the maximum number of term ites
128 * encountered on any path from e to a leaf.
130 * - termITEHeight(leaves) = 0
131 * - termITEHeight(e: term-ite(c, t, e) ) =
132 * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
133 * - termITEHeight(e not term ite) = max_{c in children(e)) (termITEHeight(c))
135 uint32_t termITEHeight(TNode e
);
137 /** Clear the cache. */
140 /** Size of the cache. */
141 size_t cache_size() const;
144 typedef std::unordered_map
<Node
, uint32_t, NodeHashFunction
> NodeCountMap
;
145 NodeCountMap d_termITEHeight
;
146 }; /* class TermITEHeightCounter */
149 * A routine designed to undo the potentially large blow up
150 * due to expansion caused by the ite simplifier.
152 class ITECompressor
{
154 ITECompressor(ContainsTermITEVisitor
* contains
);
157 /* returns false if an assertion is discovered to be equal to false. */
158 bool compress(std::vector
<Node
>& assertions
);
160 /* garbage Collects the compressor. */
161 void garbageCollect();
165 Node d_true
; /* Copy of true. */
166 Node d_false
; /* Copy of false. */
167 ContainsTermITEVisitor
* d_contains
;
168 std::vector
<Node
>* d_assertions
;
169 IncomingArcCounter d_incoming
;
171 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
172 NodeMap d_compressed
;
176 Node
push_back_boolean(Node original
, Node compressed
);
177 bool multipleParents(TNode c
);
178 Node
compressBooleanITEs(Node toCompress
);
179 Node
compressTerm(Node toCompress
);
180 Node
compressBoolean(Node toCompress
);
184 IntStat d_compressCalls
;
185 IntStat d_skolemsAdded
;
189 Statistics d_statistics
;
190 }; /* class ITECompressor */
192 class ITESimplifier
{
194 ITESimplifier(ContainsTermITEVisitor
* d_containsVisitor
);
197 Node
simpITE(TNode assertion
);
199 bool doneALotOfWorkHeuristic() const;
200 void clearSimpITECaches();
206 ContainsTermITEVisitor
* d_containsVisitor
;
207 inline bool containsTermITE(TNode n
) {
208 return d_containsVisitor
->containsTermITE(n
);
210 TermITEHeightCounter d_termITEHeight
;
211 inline uint32_t termITEHeight(TNode e
) {
212 return d_termITEHeight
.termITEHeight(e
);
215 // ConstantIte is a small inductive sublanguage:
217 // or termITE(cnd, ConstantIte, ConstantIte)
218 typedef std::vector
<Node
> NodeVec
;
219 typedef std::unordered_map
<Node
, NodeVec
*, NodeHashFunction
> ConstantLeavesMap
;
220 ConstantLeavesMap d_constantLeaves
;
222 // d_constantLeaves satisfies the following invariants:
223 // not containsTermITE(x) then !isKey(x)
224 // containsTermITE(x):
225 // - not isKey(x) then this value is uncomputed
226 // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
227 // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant leaf
228 bool isConstantIte(TNode e
);
230 /** If its not a constant and containsTermITE(ite),
231 * returns a sorted NodeVec of the leaves. */
232 NodeVec
* computeConstantLeaves(TNode ite
);
234 // Lists all of the vectors in d_constantLeaves for fast deletion.
235 std::vector
<NodeVec
*> d_allocatedConstantLeaves
;
239 Node
transformAtom(TNode atom
);
240 Node
attemptConstantRemoval(TNode atom
);
241 Node
attemptLiftEquality(TNode atom
);
242 Node
attemptEagerRemoval(TNode atom
);
244 // Given ConstantIte trees lcite and rcite,
245 // return a boolean expression equivalent to (= lcite rcite)
246 Node
intersectConstantIte(TNode lcite
, TNode rcite
);
248 // Given ConstantIte tree cite and a constant c,
249 // return a boolean expression equivalent to (= lcite c)
250 Node
constantIteEqualsConstant(TNode cite
, TNode c
);
251 uint32_t d_citeEqConstApplications
;
253 typedef std::pair
<Node
, Node
> NodePair
;
254 using NodePairHashFunction
=
255 PairHashFunction
<Node
, Node
, NodeHashFunction
, NodeHashFunction
>;
256 typedef std::unordered_map
<NodePair
, Node
, NodePairHashFunction
> NodePairMap
;
257 NodePairMap d_constantIteEqualsConstantCache
;
258 NodePairMap d_replaceOverCache
;
259 NodePairMap d_replaceOverTermIteCache
;
260 Node
replaceOver(Node n
, Node replaceWith
, Node simpVar
);
261 Node
replaceOverTermIte(Node term
, Node simpAtom
, Node simpVar
);
263 std::unordered_map
<Node
, bool, NodeHashFunction
> d_leavesConstCache
;
264 bool leavesAreConst(TNode e
, theory::TheoryId tid
);
265 bool leavesAreConst(TNode e
);
267 NodePairMap d_simpConstCache
;
268 Node
simpConstants(TNode simpContext
, TNode iteNode
, TNode simpVar
);
269 std::unordered_map
<TypeNode
, Node
, TypeNode::HashFunction
> d_simpVars
;
270 Node
getSimpVar(TypeNode t
);
272 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
273 NodeMap d_simpContextCache
;
274 Node
createSimpContext(TNode c
, Node
& iteNode
, Node
& simpVar
);
276 NodeMap d_simpITECache
;
277 Node
simpITEAtom(TNode atom
);
283 IntStat d_maxNonConstantsFolded
;
284 IntStat d_unexpected
;
285 IntStat d_unsimplified
;
286 IntStat d_exactMatchFold
;
287 IntStat d_binaryPredFold
;
288 IntStat d_specialEqualityFolds
;
289 IntStat d_simpITEVisits
;
291 HistogramStat
<uint32_t> d_inSmaller
;
297 Statistics d_statistics
;
300 class ITECareSimplifier
{
303 ~ITECareSimplifier();
305 Node
simplifyWithCare(TNode e
);
311 * This should always equal the number of care sets allocated by
312 * this object - the number of these that have been deleted. This is
313 * initially 0 and should always be 0 at the *start* of
314 * ~ITECareSimplifier().
316 unsigned d_careSetsOutstanding
;
321 typedef std::unordered_map
<TNode
, Node
, TNodeHashFunction
> TNodeMap
;
324 class CareSetPtrVal
{
326 bool safeToGarbageCollect() const { return d_refCount
== 0; }
328 friend class ITECareSimplifier::CareSetPtr
;
329 ITECareSimplifier
& d_iteSimplifier
;
331 std::set
<Node
> d_careSet
;
332 CareSetPtrVal(ITECareSimplifier
& simp
)
333 : d_iteSimplifier(simp
), d_refCount(1) {}
334 }; /* class ITECareSimplifier::CareSetPtrVal */
336 std::vector
<CareSetPtrVal
*> d_usedSets
;
337 void careSetPtrGC(CareSetPtrVal
* val
) {
338 d_usedSets
.push_back(val
);
342 CareSetPtrVal
* d_val
;
343 CareSetPtr(CareSetPtrVal
* val
) : d_val(val
) {}
345 CareSetPtr() : d_val(NULL
) {}
346 CareSetPtr(const CareSetPtr
& cs
) {
349 ++(d_val
->d_refCount
);
353 if (d_val
!= NULL
&& (--(d_val
->d_refCount
) == 0)) {
354 d_val
->d_iteSimplifier
.careSetPtrGC(d_val
);
357 CareSetPtr
& operator=(const CareSetPtr
& cs
) {
358 if (d_val
!= cs
.d_val
) {
359 if (d_val
!= NULL
&& (--(d_val
->d_refCount
) == 0)) {
360 d_val
->d_iteSimplifier
.careSetPtrGC(d_val
);
364 ++(d_val
->d_refCount
);
369 std::set
<Node
>& getCareSet() { return d_val
->d_careSet
; }
371 static CareSetPtr
mkNew(ITECareSimplifier
& simp
);
372 static CareSetPtr
recycle(CareSetPtrVal
* val
) {
373 Assert(val
!= NULL
&& val
->d_refCount
== 0);
375 return CareSetPtr(val
);
377 }; /* class ITECareSimplifier::CareSetPtr */
379 CareSetPtr
getNewSet();
381 typedef std::map
<TNode
, CareSetPtr
> CareMap
;
382 void updateQueue(CareMap
& queue
, TNode e
, CareSetPtr
& careSet
);
383 Node
substitute(TNode e
, TNodeMap
& substTable
, TNodeMap
& cache
);
386 }/* CVC4::theory namespace */
387 }/* CVC4 namespace */