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