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-2019 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 /** Whether to keep substitutions in solved form */ 70 bool d_solvedForm; 71 72 /** Internal method that performs substitution */ 73 Node internalSubstitute(TNode t, NodeCache& cache); 74 75 /** Helper class to invalidate cache on user pop */ 76 class CacheInvalidator : public context::ContextNotifyObj { 77 bool& d_cacheInvalidated; 78 protected: contextNotifyPop()79 void contextNotifyPop() override { d_cacheInvalidated = true; } 80 81 public: CacheInvalidator(context::Context * context,bool & cacheInvalidated)82 CacheInvalidator(context::Context* context, bool& cacheInvalidated) : 83 context::ContextNotifyObj(context), 84 d_cacheInvalidated(cacheInvalidated) { 85 } 86 87 };/* class SubstitutionMap::CacheInvalidator */ 88 89 /** 90 * This object is notified on user pop and marks the SubstitutionMap's 91 * cache as invalidated. 92 */ 93 CacheInvalidator d_cacheInvalidator; 94 95 public: 96 97 SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : d_substitutions(context)98 d_substitutions(context), 99 d_substitutionCache(), 100 d_substituteUnderQuantifiers(substituteUnderQuantifiers), 101 d_cacheInvalidated(false), 102 d_solvedForm(solvedForm), 103 d_cacheInvalidator(context, d_cacheInvalidated) 104 { 105 } 106 107 /** 108 * Adds a substitution from x to t. 109 */ 110 void addSubstitution(TNode x, TNode t, bool invalidateCache = true); 111 112 /** 113 * Merge subMap into current set of substitutions 114 */ 115 void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true); 116 117 /** 118 * Returns true iff x is in the substitution map 119 */ hasSubstitution(TNode x)120 bool hasSubstitution(TNode x) const { 121 return d_substitutions.find(x) != d_substitutions.end(); 122 } 123 124 /** 125 * Returns the substitution mapping that was given for x via 126 * addSubstitution(). Note that the returned value might itself 127 * be in the map; for the actual substitution that would be 128 * performed for x, use .apply(x). This getSubstitution() function 129 * is mainly intended for constructing assertions about what has 130 * already been put in the map. 131 */ getSubstitution(TNode x)132 TNode getSubstitution(TNode x) const { 133 AssertArgument(hasSubstitution(x), x, "element not in this substitution map"); 134 return (*d_substitutions.find(x)).second; 135 } 136 137 /** 138 * Apply the substitutions to the node. 139 */ 140 Node apply(TNode t); 141 142 /** 143 * Apply the substitutions to the node. 144 */ apply(TNode t)145 Node apply(TNode t) const { 146 return const_cast<SubstitutionMap*>(this)->apply(t); 147 } 148 begin()149 iterator begin() { 150 return d_substitutions.begin(); 151 } 152 end()153 iterator end() { 154 return d_substitutions.end(); 155 } 156 begin()157 const_iterator begin() const { 158 return d_substitutions.begin(); 159 } 160 end()161 const_iterator end() const { 162 return d_substitutions.end(); 163 } 164 empty()165 bool empty() const { 166 return d_substitutions.empty(); 167 } 168 169 // NOTE [MGD]: removed clear() and swap() from the interface 170 // when this data structure became context-dependent 171 // because they weren't used---and it's not clear how they 172 // should best interact with cache invalidation on context 173 // pops. 174 175 // Simplify right-hand sides of current map using the given substitutions 176 void simplifyRHS(const SubstitutionMap& subMap); 177 178 // Simplify right-hand sides of current map with lhs -> rhs 179 void simplifyRHS(TNode lhs, TNode rhs); 180 isSolvedForm()181 bool isSolvedForm() const { return d_solvedForm; } 182 183 /** 184 * Print to the output stream 185 */ 186 void print(std::ostream& out) const; 187 void debugPrint() const; 188 189 };/* class SubstitutionMap */ 190 191 inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) { 192 subst.print(out); 193 return out; 194 } 195 196 }/* CVC4::theory namespace */ 197 198 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i); 199 200 }/* CVC4 namespace */ 201 202 #endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ 203