src/theory/ite_utilities.h

   1 /*********************                                                        */
   2 /*! \file ite_utilities.h
   3  ** \verbatim
   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
  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 '96
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef __CVC4__ITE_UTILITIES_H
  23 #define __CVC4__ITE_UTILITIES_H
  24
  25 #include <unordered_map>
  26 #include <vector>
  27
  28 #include "expr/node.h"
  29 #include "util/hash.h"
  30 #include "util/statistics_registry.h"
  31
  32 namespace CVC4 {
  33 namespace theory {
  34
  35 class IncomingArcCounter;
  36 class TermITEHeightCounter;
  37 class ITECompressor;
  38 class ITESimplifier;
  39 class ITECareSimplifier;
  40
  41 /**
  42  * A caching visitor that computes whether a node contains a term ite.
  43  */
  44 class ContainsTermITEVisitor {
  45 public:
  46   ContainsTermITEVisitor();
  47   ~ContainsTermITEVisitor();
  48
  49   /** returns true if a node contains a term ite. */
  50   bool containsTermITE(TNode n);
  51
  52   /** Garbage collects the cache. */
  53   void garbageCollect();
  54
  55   /** returns the size of the cache. */
  56   size_t cache_size() const { return d_cache.size(); }
  57
  58 private:
  59   typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
  60   NodeBoolMap d_cache;
  61 };
  62
  63 class ITEUtilities
  64 {
  65  public:
  66   ITEUtilities();
  67   ~ITEUtilities();
  68
  69   Node simpITE(TNode assertion);
  70
  71   bool simpIteDidALotOfWorkHeuristic() const;
  72
  73   /* returns false if an assertion is discovered to be equal to false. */
  74   bool compress(std::vector<Node>& assertions);
  75
  76   Node simplifyWithCare(TNode e);
  77
  78   void clear();
  79
  80   ContainsTermITEVisitor* getContainsVisitor()
  81   {
  82     return d_containsVisitor.get();
  83   }
  84
  85   bool containsTermITE(TNode n)
  86   {
  87     return d_containsVisitor->containsTermITE(n);
  88   }
  89
  90  private:
  91   std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
  92   ITECompressor* d_compressor;
  93   ITESimplifier* d_simplifier;
  94   ITECareSimplifier* d_careSimp;
  95 };
  96
  97 class IncomingArcCounter {
  98 public:
  99   IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
 100   ~IncomingArcCounter();
 101   void computeReachability(const std::vector<Node>& assertions);
 102
 103   inline uint32_t lookupIncoming(Node n) const {
 104     NodeCountMap::const_iterator it = d_reachCount.find(n);
 105     if(it == d_reachCount.end()){
 106       return 0;
 107     }else{
 108       return (*it).second;
 109     }
 110   }
 111   void clear();
 112 private:
 113   typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
 114   NodeCountMap d_reachCount;
 115
 116   bool d_skipVariables;
 117   bool d_skipConstants;
 118 };
 119
 120 class TermITEHeightCounter {
 121 public:
 122   TermITEHeightCounter();
 123   ~TermITEHeightCounter();
 124
 125   /**
 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.
 129    * Inductively:
 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))
 134    */
 135   uint32_t termITEHeight(TNode e);
 136
 137   /** Clear the cache. */
 138   void clear();
 139
 140   /** Size of the cache. */
 141   size_t cache_size() const;
 142
 143 private:
 144   typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
 145   NodeCountMap d_termITEHeight;
 146 }; /* class TermITEHeightCounter */
 147
 148 /**
 149  * A routine designed to undo the potentially large blow up
 150  * due to expansion caused by the ite simplifier.
 151  */
 152 class ITECompressor {
 153 public:
 154   ITECompressor(ContainsTermITEVisitor* contains);
 155   ~ITECompressor();
 156
 157   /* returns false if an assertion is discovered to be equal to false. */
 158   bool compress(std::vector<Node>& assertions);
 159
 160   /* garbage Collects the compressor. */
 161   void garbageCollect();
 162
 163 private:
 164
 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;
 170
 171   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 172   NodeMap d_compressed;
 173
 174   void reset();
 175
 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);
 181
 182   class Statistics {
 183   public:
 184     IntStat d_compressCalls;
 185     IntStat d_skolemsAdded;
 186     Statistics();
 187     ~Statistics();
 188   };
 189   Statistics d_statistics;
 190 }; /* class ITECompressor */
 191
 192 class ITESimplifier {
 193 public:
 194   ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
 195   ~ITESimplifier();
 196
 197   Node simpITE(TNode assertion);
 198
 199   bool doneALotOfWorkHeuristic() const;
 200   void clearSimpITECaches();
 201
 202 private:
 203   Node d_true;
 204   Node d_false;
 205
 206   ContainsTermITEVisitor* d_containsVisitor;
 207   inline bool containsTermITE(TNode n) {
 208     return d_containsVisitor->containsTermITE(n);
 209   }
 210   TermITEHeightCounter d_termITEHeight;
 211   inline uint32_t termITEHeight(TNode e) {
 212     return d_termITEHeight.termITEHeight(e);
 213   }
 214
 215   // ConstantIte is a small inductive sublanguage:
 216   //     constant
 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;
 221
 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);
 229
 230   /** If its not a constant and containsTermITE(ite),
 231    * returns a sorted NodeVec of the leaves. */
 232   NodeVec* computeConstantLeaves(TNode ite);
 233
 234   // Lists all of the vectors in d_constantLeaves for fast deletion.
 235   std::vector<NodeVec*> d_allocatedConstantLeaves;
 236
 237
 238   /* transforms */
 239   Node transformAtom(TNode atom);
 240   Node attemptConstantRemoval(TNode atom);
 241   Node attemptLiftEquality(TNode atom);
 242   Node attemptEagerRemoval(TNode atom);
 243
 244   // Given ConstantIte trees lcite and rcite,
 245   // return a boolean expression equivalent to (= lcite rcite)
 246   Node intersectConstantIte(TNode lcite, TNode rcite);
 247
 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;
 252
 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);
 262
 263   std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
 264   bool leavesAreConst(TNode e, theory::TheoryId tid);
 265   bool leavesAreConst(TNode e);
 266
 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);
 271
 272   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 273   NodeMap d_simpContextCache;
 274   Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
 275
 276   NodeMap d_simpITECache;
 277   Node simpITEAtom(TNode atom);
 278
 279
 280 private:
 281   class Statistics {
 282   public:
 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;
 290
 291     HistogramStat<uint32_t> d_inSmaller;
 292
 293     Statistics();
 294     ~Statistics();
 295   };
 296
 297   Statistics d_statistics;
 298 };
 299
 300 class ITECareSimplifier {
 301 public:
 302   ITECareSimplifier();
 303   ~ITECareSimplifier();
 304
 305   Node simplifyWithCare(TNode e);
 306
 307   void clear();
 308 private:
 309
 310   /**
 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().
 315    */
 316   unsigned d_careSetsOutstanding;
 317
 318   Node d_true;
 319   Node d_false;
 320
 321   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 322
 323   class CareSetPtr;
 324   class CareSetPtrVal {
 325    public:
 326     bool safeToGarbageCollect() const { return d_refCount == 0; }
 327    private:
 328     friend class ITECareSimplifier::CareSetPtr;
 329     ITECareSimplifier& d_iteSimplifier;
 330     unsigned d_refCount;
 331     std::set<Node> d_careSet;
 332     CareSetPtrVal(ITECareSimplifier& simp)
 333         : d_iteSimplifier(simp), d_refCount(1) {}
 334   }; /* class ITECareSimplifier::CareSetPtrVal */
 335
 336   std::vector<CareSetPtrVal*> d_usedSets;
 337   void careSetPtrGC(CareSetPtrVal* val) {
 338     d_usedSets.push_back(val);
 339   }
 340
 341   class CareSetPtr {
 342     CareSetPtrVal* d_val;
 343     CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
 344   public:
 345     CareSetPtr() : d_val(NULL) {}
 346     CareSetPtr(const CareSetPtr& cs) {
 347       d_val = cs.d_val;
 348       if (d_val != NULL) {
 349         ++(d_val->d_refCount);
 350       }
 351     }
 352     ~CareSetPtr() {
 353       if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
 354         d_val->d_iteSimplifier.careSetPtrGC(d_val);
 355       }
 356     }
 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);
 361         }
 362         d_val = cs.d_val;
 363         if (d_val != NULL) {
 364           ++(d_val->d_refCount);
 365         }
 366       }
 367       return *this;
 368     }
 369     std::set<Node>& getCareSet() { return d_val->d_careSet; }
 370
 371     static CareSetPtr mkNew(ITECareSimplifier& simp);
 372     static CareSetPtr recycle(CareSetPtrVal* val) {
 373       Assert(val != NULL && val->d_refCount == 0);
 374       val->d_refCount = 1;
 375       return CareSetPtr(val);
 376     }
 377   }; /* class ITECareSimplifier::CareSetPtr */
 378
 379   CareSetPtr getNewSet();
 380
 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);
 384 };
 385
 386 }/* CVC4::theory namespace */
 387 }/* CVC4 namespace */
 388
 389 #endif