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