GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/util/ite_utilities.h Lines: 8 43 18.6 %
Date: 2021-03-23 Branches: 4 44 9.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ite_utilities.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Aina Niemetz, Clark Barrett
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief Simplifications for ITE expressions
13
 **
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
18
 *'96
19
 **/
20
21
#include "cvc4_private.h"
22
23
#ifndef CVC4__ITE_UTILITIES_H
24
#define CVC4__ITE_UTILITIES_H
25
26
#include <unordered_map>
27
#include <vector>
28
29
#include "expr/node.h"
30
#include "util/hash.h"
31
#include "util/statistics_registry.h"
32
#include "util/stats_histogram.h"
33
34
namespace CVC4 {
35
namespace preprocessing {
36
37
class AssertionPipeline;
38
39
namespace util {
40
41
class ITECompressor;
42
class ITESimplifier;
43
class ITECareSimplifier;
44
45
/**
46
 * A caching visitor that computes whether a node contains a term ite.
47
 */
48
class ContainsTermITEVisitor
49
{
50
 public:
51
  ContainsTermITEVisitor();
52
  ~ContainsTermITEVisitor();
53
54
  /** returns true if a node contains a term ite. */
55
  bool containsTermITE(TNode n);
56
57
  /** Garbage collects the cache. */
58
  void garbageCollect();
59
60
  /** returns the size of the cache. */
61
  size_t cache_size() const { return d_cache.size(); }
62
63
 private:
64
  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
65
  NodeBoolMap d_cache;
66
};
67
68
class ITEUtilities
69
{
70
 public:
71
  ITEUtilities();
72
  ~ITEUtilities();
73
74
  Node simpITE(TNode assertion);
75
76
  bool simpIteDidALotOfWorkHeuristic() const;
77
78
  /* returns false if an assertion is discovered to be equal to false. */
79
  bool compress(AssertionPipeline* assertionsToPreprocess);
80
81
  Node simplifyWithCare(TNode e);
82
83
  void clear();
84
85
  ContainsTermITEVisitor* getContainsVisitor()
86
  {
87
    return d_containsVisitor.get();
88
  }
89
90
2
  bool containsTermITE(TNode n)
91
  {
92
2
    return d_containsVisitor->containsTermITE(n);
93
  }
94
95
 private:
96
  std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
97
  ITECompressor* d_compressor;
98
  ITESimplifier* d_simplifier;
99
  ITECareSimplifier* d_careSimp;
100
};
101
102
class IncomingArcCounter
103
{
104
 public:
105
  IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
106
  ~IncomingArcCounter();
107
  void computeReachability(const std::vector<Node>& assertions);
108
109
7109
  inline uint32_t lookupIncoming(Node n) const
110
  {
111
7109
    NodeCountMap::const_iterator it = d_reachCount.find(n);
112
7109
    if (it == d_reachCount.end())
113
    {
114
      return 0;
115
    }
116
    else
117
    {
118
7109
      return (*it).second;
119
    }
120
  }
121
  void clear();
122
123
 private:
124
  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
125
  NodeCountMap d_reachCount;
126
127
  bool d_skipVariables;
128
  bool d_skipConstants;
129
};
130
131
class TermITEHeightCounter
132
{
133
 public:
134
  TermITEHeightCounter();
135
  ~TermITEHeightCounter();
136
137
  /**
138
   * Compute and [potentially] cache the termITEHeight() of e.
139
   * The term ite height equals the maximum number of term ites
140
   * encountered on any path from e to a leaf.
141
   * Inductively:
142
   *  - termITEHeight(leaves) = 0
143
   *  - termITEHeight(e: term-ite(c, t, e) ) =
144
   *     1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
145
   *  - termITEHeight(e not term ite) = max_{c in children(e))
146
   * (termITEHeight(c))
147
   */
148
  uint32_t termITEHeight(TNode e);
149
150
  /** Clear the cache. */
151
  void clear();
152
153
  /** Size of the cache. */
154
  size_t cache_size() const;
155
156
 private:
157
  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
158
  NodeCountMap d_termITEHeight;
159
}; /* class TermITEHeightCounter */
160
161
/**
162
 * A routine designed to undo the potentially large blow up
163
 * due to expansion caused by the ite simplifier.
164
 */
165
class ITECompressor
166
{
167
 public:
168
  ITECompressor(ContainsTermITEVisitor* contains);
169
  ~ITECompressor();
170
171
  /* returns false if an assertion is discovered to be equal to false. */
172
  bool compress(AssertionPipeline* assertionsToPreprocess);
173
174
  /* garbage Collects the compressor. */
175
  void garbageCollect();
176
177
 private:
178
  Node d_true;  /* Copy of true. */
179
  Node d_false; /* Copy of false. */
180
  ContainsTermITEVisitor* d_contains;
181
  AssertionPipeline* d_assertions;
182
  IncomingArcCounter d_incoming;
183
184
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
185
  NodeMap d_compressed;
186
187
  void reset();
188
189
  Node push_back_boolean(Node original, Node compressed);
190
  bool multipleParents(TNode c);
191
  Node compressBooleanITEs(Node toCompress);
192
  Node compressTerm(Node toCompress);
193
  Node compressBoolean(Node toCompress);
194
195
  class Statistics
196
  {
197
   public:
198
    IntStat d_compressCalls;
199
    IntStat d_skolemsAdded;
200
    Statistics();
201
    ~Statistics();
202
  };
203
  Statistics d_statistics;
204
}; /* class ITECompressor */
205
206
class ITESimplifier
207
{
208
 public:
209
  ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
210
  ~ITESimplifier();
211
212
  Node simpITE(TNode assertion);
213
214
  bool doneALotOfWorkHeuristic() const;
215
  void clearSimpITECaches();
216
217
 private:
218
  Node d_true;
219
  Node d_false;
220
221
  ContainsTermITEVisitor* d_containsVisitor;
222
2043
  inline bool containsTermITE(TNode n)
223
  {
224
2043
    return d_containsVisitor->containsTermITE(n);
225
  }
226
  TermITEHeightCounter d_termITEHeight;
227
  inline uint32_t termITEHeight(TNode e)
228
  {
229
    return d_termITEHeight.termITEHeight(e);
230
  }
231
232
  // ConstantIte is a small inductive sublanguage:
233
  //     constant
234
  // or  termITE(cnd, ConstantIte, ConstantIte)
235
  typedef std::vector<Node> NodeVec;
236
  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction>
237
      ConstantLeavesMap;
238
  ConstantLeavesMap d_constantLeaves;
239
240
  // d_constantLeaves satisfies the following invariants:
241
  // not containsTermITE(x) then !isKey(x)
242
  // containsTermITE(x):
243
  // - not isKey(x) then this value is uncomputed
244
  // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
245
  // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant
246
  // leaf
247
  bool isConstantIte(TNode e);
248
249
  /** If its not a constant and containsTermITE(ite),
250
   * returns a sorted NodeVec of the leaves. */
251
  NodeVec* computeConstantLeaves(TNode ite);
252
253
  // Lists all of the vectors in d_constantLeaves for fast deletion.
254
  std::vector<NodeVec*> d_allocatedConstantLeaves;
255
256
  /* transforms */
257
  Node transformAtom(TNode atom);
258
  Node attemptConstantRemoval(TNode atom);
259
  Node attemptLiftEquality(TNode atom);
260
  Node attemptEagerRemoval(TNode atom);
261
262
  // Given ConstantIte trees lcite and rcite,
263
  // return a boolean expression equivalent to (= lcite rcite)
264
  Node intersectConstantIte(TNode lcite, TNode rcite);
265
266
  // Given ConstantIte tree cite and a constant c,
267
  // return a boolean expression equivalent to (= lcite c)
268
  Node constantIteEqualsConstant(TNode cite, TNode c);
269
  uint32_t d_citeEqConstApplications;
270
271
  typedef std::pair<Node, Node> NodePair;
272
  using NodePairHashFunction =
273
      PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>;
274
  typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
275
  NodePairMap d_constantIteEqualsConstantCache;
276
  NodePairMap d_replaceOverCache;
277
  NodePairMap d_replaceOverTermIteCache;
278
  Node replaceOver(Node n, Node replaceWith, Node simpVar);
279
  Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
280
281
  std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
282
  bool leavesAreConst(TNode e, theory::TheoryId tid);
283
  bool leavesAreConst(TNode e);
284
285
  NodePairMap d_simpConstCache;
286
  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
287
  std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
288
  Node getSimpVar(TypeNode t);
289
290
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
291
  NodeMap d_simpContextCache;
292
  Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
293
294
  NodeMap d_simpITECache;
295
  Node simpITEAtom(TNode atom);
296
297
 private:
298
  class Statistics
299
  {
300
   public:
301
    IntStat d_maxNonConstantsFolded;
302
    IntStat d_unexpected;
303
    IntStat d_unsimplified;
304
    IntStat d_exactMatchFold;
305
    IntStat d_binaryPredFold;
306
    IntStat d_specialEqualityFolds;
307
    IntStat d_simpITEVisits;
308
309
    IntegralHistogramStat<uint32_t> d_inSmaller;
310
311
    Statistics();
312
    ~Statistics();
313
  };
314
315
  Statistics d_statistics;
316
};
317
318
class ITECareSimplifier
319
{
320
 public:
321
  ITECareSimplifier();
322
  ~ITECareSimplifier();
323
324
  Node simplifyWithCare(TNode e);
325
326
  void clear();
327
328
 private:
329
  /**
330
   * This should always equal the number of care sets allocated by
331
   * this object - the number of these that have been deleted. This is
332
   * initially 0 and should always be 0 at the *start* of
333
   * ~ITECareSimplifier().
334
   */
335
  unsigned d_careSetsOutstanding;
336
337
  Node d_true;
338
  Node d_false;
339
340
  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
341
342
  class CareSetPtr;
343
  class CareSetPtrVal
344
  {
345
   public:
346
    bool safeToGarbageCollect() const { return d_refCount == 0; }
347
348
   private:
349
    friend class ITECareSimplifier::CareSetPtr;
350
    ITECareSimplifier& d_iteSimplifier;
351
    unsigned d_refCount;
352
    std::set<Node> d_careSet;
353
    CareSetPtrVal(ITECareSimplifier& simp)
354
        : d_iteSimplifier(simp), d_refCount(1)
355
    {
356
    }
357
  }; /* class ITECareSimplifier::CareSetPtrVal */
358
359
  std::vector<CareSetPtrVal*> d_usedSets;
360
  void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); }
361
362
  class CareSetPtr
363
  {
364
    CareSetPtrVal* d_val;
365
    CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
366
367
   public:
368
    CareSetPtr() : d_val(NULL) {}
369
    CareSetPtr(const CareSetPtr& cs)
370
    {
371
      d_val = cs.d_val;
372
      if (d_val != NULL)
373
      {
374
        ++(d_val->d_refCount);
375
      }
376
    }
377
    ~CareSetPtr()
378
    {
379
      if (d_val != NULL && (--(d_val->d_refCount) == 0))
380
      {
381
        d_val->d_iteSimplifier.careSetPtrGC(d_val);
382
      }
383
    }
384
    CareSetPtr& operator=(const CareSetPtr& cs)
385
    {
386
      if (d_val != cs.d_val)
387
      {
388
        if (d_val != NULL && (--(d_val->d_refCount) == 0))
389
        {
390
          d_val->d_iteSimplifier.careSetPtrGC(d_val);
391
        }
392
        d_val = cs.d_val;
393
        if (d_val != NULL)
394
        {
395
          ++(d_val->d_refCount);
396
        }
397
      }
398
      return *this;
399
    }
400
    std::set<Node>& getCareSet() { return d_val->d_careSet; }
401
402
    static CareSetPtr mkNew(ITECareSimplifier& simp);
403
    static CareSetPtr recycle(CareSetPtrVal* val)
404
    {
405
      Assert(val != NULL && val->d_refCount == 0);
406
      val->d_refCount = 1;
407
      return CareSetPtr(val);
408
    }
409
  }; /* class ITECareSimplifier::CareSetPtr */
410
411
  CareSetPtr getNewSet();
412
413
  typedef std::map<TNode, CareSetPtr> CareMap;
414
  void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
415
  Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
416
};
417
418
}  // namespace util
419
}  // namespace preprocessing
420
}  // namespace CVC4
421
422
#endif