src/theory/substitutions.h

   1 /*********************                                                        */
   2 /*! \file substitutions.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Dejan Jovanovic, Clark Barrett
   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
  11  **
  12  ** \brief A substitution mapping for theory simplification
  13  **
  14  ** A substitution mapping for theory simplification.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__SUBSTITUTIONS_H
  20 #define CVC4__THEORY__SUBSTITUTIONS_H
  21
  22 //#include <algorithm>
  23 #include <utility>
  24 #include <vector>
  25 #include <unordered_map>
  26
  27 #include "expr/node.h"
  28 #include "context/context.h"
  29 #include "context/cdo.h"
  30 #include "context/cdhashmap.h"
  31 #include "util/hash.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35
  36 /**
  37  * The type for the Substitutions mapping output by
  38  * Theory::simplify(), TheoryEngine::simplify(), and
  39  * Valuation::simplify().  This is in its own header to
  40  * avoid circular dependences between those three.
  41  *
  42  * This map is context-dependent.
  43  */
  44 class SubstitutionMap {
  45
  46 public:
  47
  48   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
  49
  50   typedef NodeMap::iterator iterator;
  51   typedef NodeMap::const_iterator const_iterator;
  52
  53 private:
  54
  55   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
  56
  57   /** The variables, in order of addition */
  58   NodeMap d_substitutions;
  59
  60   /** Cache of the already performed substitutions */
  61   NodeCache d_substitutionCache;
  62
  63   /** Whether or not to substitute under quantifiers */
  64   bool d_substituteUnderQuantifiers;
  65
  66   /** Has the cache been invalidated? */
  67   bool d_cacheInvalidated;
  68
  69   /** Internal method that performs substitution */
  70   Node internalSubstitute(TNode t, NodeCache& cache);
  71
  72   /** Helper class to invalidate cache on user pop */
  73   class CacheInvalidator : public context::ContextNotifyObj {
  74     bool& d_cacheInvalidated;
  75   protected:
  76    void contextNotifyPop() override { d_cacheInvalidated = true; }
  77
  78   public:
  79     CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
  80       context::ContextNotifyObj(context),
  81       d_cacheInvalidated(cacheInvalidated) {
  82     }
  83
  84   };/* class SubstitutionMap::CacheInvalidator */
  85
  86   /**
  87    * This object is notified on user pop and marks the SubstitutionMap's
  88    * cache as invalidated.
  89    */
  90   CacheInvalidator d_cacheInvalidator;
  91
  92 public:
  93  SubstitutionMap(context::Context* context,
  94                  bool substituteUnderQuantifiers = true)
  95      : d_substitutions(context),
  96        d_substitutionCache(),
  97        d_substituteUnderQuantifiers(substituteUnderQuantifiers),
  98        d_cacheInvalidated(false),
  99        d_cacheInvalidator(context, d_cacheInvalidated)
 100  {
 101   }
 102
 103   /**
 104    * Adds a substitution from x to t.
 105    */
 106   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 107
 108   /**
 109    * Merge subMap into current set of substitutions
 110    */
 111   void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
 112
 113   /**
 114    * Returns true iff x is in the substitution map
 115    */
 116   bool hasSubstitution(TNode x) const {
 117     return d_substitutions.find(x) != d_substitutions.end();
 118   }
 119
 120   /**
 121    * Returns the substitution mapping that was given for x via
 122    * addSubstitution().  Note that the returned value might itself
 123    * be in the map; for the actual substitution that would be
 124    * performed for x, use .apply(x).  This getSubstitution() function
 125    * is mainly intended for constructing assertions about what has
 126    * already been put in the map.
 127    */
 128   TNode getSubstitution(TNode x) const {
 129     AssertArgument(hasSubstitution(x), x, "element not in this substitution map");
 130     return (*d_substitutions.find(x)).second;
 131   }
 132
 133   /**
 134    * Apply the substitutions to the node.
 135    */
 136   Node apply(TNode t);
 137
 138   /**
 139    * Apply the substitutions to the node.
 140    */
 141   Node apply(TNode t) const {
 142     return const_cast<SubstitutionMap*>(this)->apply(t);
 143   }
 144
 145   iterator begin() {
 146     return d_substitutions.begin();
 147   }
 148
 149   iterator end() {
 150     return d_substitutions.end();
 151   }
 152
 153   const_iterator begin() const {
 154     return d_substitutions.begin();
 155   }
 156
 157   const_iterator end() const {
 158     return d_substitutions.end();
 159   }
 160
 161   bool empty() const {
 162     return d_substitutions.empty();
 163   }
 164
 165   /**
 166    * Print to the output stream
 167    */
 168   void print(std::ostream& out) const;
 169   void debugPrint() const;
 170
 171 };/* class SubstitutionMap */
 172
 173 inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
 174   subst.print(out);
 175   return out;
 176 }
 177
 178 }/* CVC4::theory namespace */
 179
 180 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
 181
 182 }/* CVC4 namespace */
 183
 184 #endif /* CVC4__THEORY__SUBSTITUTIONS_H */