1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Class for rewriting contexts.
25 //
26 // A rewriting context keeps track of miscellaneous information needed
27 // while rewriting. An important perfomance trick is that we derive it
28 // from Substitution so that we can use the rewriting context to construct
29 // matching substitutions in. This avoids creating a new substitution at
30 // the start of each match attempt.
31 //
32 #ifndef _rewritingContext_hh_
33 #define _rewritingContext_hh_
34 #include "substitution.hh"
35 #include "simpleRootContainer.hh"
36 #include "dagNode.hh"
37 #include "module.hh"
38
39 class RewritingContext : public Substitution, private SimpleRootContainer
40 {
41 public:
42 enum Purpose
43 {
44 CONDITION_EVAL,
45 SORT_EVAL,
46 OTHER
47 };
48
49 enum RewriteType
50 {
51 NORMAL,
52 BUILTIN,
53 MEMOIZED
54 };
55
56 RewritingContext(DagNode* root);
57 RewritingContext(int substitutionSize); // limited use RewritingContext for matching
58 virtual ~RewritingContext();
59
60 static bool getTraceStatus();
61 static void setTraceStatus(bool state);
62
63 DagNode* root();
64 void incrementMbCount(Int64 i = 1);
65 void incrementEqCount(Int64 i = 1);
66 void incrementRlCount(Int64 i = 1);
67 void incrementNarrowingCount(Int64 i = 1);
68 void incrementVariantNarrowingCount(Int64 i = 1);
69
70 void clearCount();
71 void addInCount(const RewritingContext& other);
72 void transferCount(RewritingContext& other);
73 Int64 getTotalCount() const;
74 Int64 getMbCount() const;
75 Int64 getEqCount() const;
76 Int64 getRlCount() const;
77 Int64 getNarrowingCount() const;
78 Int64 getVariantNarrowingCount() const;
79 void reduce();
80 void ruleRewrite(Int64 limit = NONE);
81 void fairRewrite(Int64 limit = NONE, Int64 gas = 1);
82 void fairContinue(Int64 limit = NONE);
83 void fairStart(Int64 gas);
84 bool fairTraversal(Int64& limit);
85 bool builtInReplace(DagNode* old, DagNode* replacement);
86
87 virtual RewritingContext* makeSubcontext(DagNode* root, int purpose = OTHER);
88 virtual int traceBeginEqTrial(DagNode* subject, const Equation* equation);
89 virtual int traceBeginRuleTrial(DagNode* subject, const Rule* rule);
90 virtual int traceBeginScTrial(DagNode* subject, const SortConstraint* sc);
91 virtual void traceEndTrial(int trialRef, bool success);
92 virtual void traceExhausted(int trialRef);
93
94 virtual void tracePreEqRewrite(DagNode* redex,
95 const Equation* equation,
96 int type);
97 virtual void tracePostEqRewrite(DagNode* replacement);
98 virtual void tracePreRuleRewrite(DagNode* redex, const Rule* rule);
99 virtual void tracePostRuleRewrite(DagNode* replacement);
100 virtual void tracePreScApplication(DagNode* subject, const SortConstraint* sc);
101 virtual bool traceAbort();
102 virtual void traceBeginFragment(int trialRef,
103 const PreEquation* preEquation,
104 int fragmentIndex,
105 bool firstAttempt);
106 virtual void traceEndFragment(int trialRef,
107 const PreEquation* preEquation,
108 int fragmentIndex,
109 bool success);
110
111 virtual void traceNarrowingStep(Rule* rule,
112 DagNode* redex,
113 DagNode* replacement,
114 const NarrowingVariableInfo* variableInfo,
115 const Substitution* substitution,
116 DagNode* newState);
117
118 virtual void traceVariantNarrowingStep(Equation* equation,
119 const Vector<DagNode*>& oldVariantSubstitution,
120 DagNode* redex,
121 DagNode* replacement,
122 const NarrowingVariableInfo& variableInfo,
123 const Substitution* substitution,
124 DagNode* newState,
125 const Vector<DagNode*>& newVariantSubstitution,
126 const NarrowingVariableInfo& originalVariables);
127
128 #ifdef DUMP
129 static void dumpStack(ostream& s, const Vector<RedexPosition>& stack);
130 #endif
131
132 protected:
133 //
134 // We make this protected so that a derived class can override it and then call
135 // our version.
136 //
137 void markReachableNodes();
138
139 private:
140 enum Special
141 {
142 ROOT_OK = -2
143 };
144
145 void rebuildUptoRoot();
146 void remakeStaleDagNode(int staleIndex, int childIndex);
147 bool ascend();
148 void descend();
149 bool doRewriting(bool argsUnstackable);
150 bool fairTraversal();
151
152 static bool traceFlag;
153
154 DagNode* rootNode;
155
156 Int64 mbCount;
157 Int64 eqCount;
158 Int64 rlCount;
159
160 Int64 narrowingCount;
161 Int64 variantNarrowingCount;
162 //
163 // For rule rewriting
164 //
165 Vector<RedexPosition> redexStack;
166 int currentIndex;
167 int staleMarker;
168 bool progress;
169 Int64 rewriteLimit;
170 Int64 gasPerNode;
171 Int64 currentGas;
172 int lazyMarker;
173 };
174
175 inline
RewritingContext(DagNode * root)176 RewritingContext::RewritingContext(DagNode* root)
177 : Substitution(root->symbol()->getModule()->getMinimumSubstitutionSize(), 0),
178 rootNode(root)
179 {
180 //cout << "sub size is " << root->symbol()->getModule()->getMinimumSubstitutionSize() << endl;
181 Assert(root != 0, "null root");
182 mbCount = 0;
183 eqCount = 0;
184 rlCount = 0;
185
186 narrowingCount = 0;
187 variantNarrowingCount = 0;
188 staleMarker = ROOT_OK;
189 }
190
191 inline
RewritingContext(int substitutionSize)192 RewritingContext::RewritingContext(int substitutionSize)
193 : Substitution(substitutionSize),
194 rootNode(0)
195 {
196 //
197 // This constructor exists so we can build RewritingContexts for use in the solve() phase of matching where
198 // we don't otherwise have a RewritingContext to hand.
199 //
200 }
201
202 inline
~RewritingContext()203 RewritingContext::~RewritingContext()
204 {
205 }
206
207 inline DagNode*
root()208 RewritingContext::root()
209 {
210 if (staleMarker != ROOT_OK)
211 rebuildUptoRoot();
212 return rootNode;
213 }
214
215 inline bool
getTraceStatus()216 RewritingContext::getTraceStatus()
217 {
218 return traceFlag;
219 }
220
221 inline void
setTraceStatus(bool state)222 RewritingContext::setTraceStatus(bool state)
223 {
224 traceFlag = state;
225 }
226
227 inline Int64
getTotalCount() const228 RewritingContext::getTotalCount() const
229 {
230 return mbCount + eqCount + rlCount + narrowingCount + variantNarrowingCount;
231 }
232 inline Int64
getMbCount() const233 RewritingContext::getMbCount() const
234 {
235 return mbCount;
236 }
237 inline Int64
getEqCount() const238 RewritingContext::getEqCount() const
239 {
240 return eqCount;
241 }
242
243 inline Int64
getRlCount() const244 RewritingContext::getRlCount() const
245 {
246 return rlCount;
247 }
248
249 inline Int64
getNarrowingCount() const250 RewritingContext::getNarrowingCount() const
251 {
252 return narrowingCount;
253 }
254
255 inline Int64
getVariantNarrowingCount() const256 RewritingContext::getVariantNarrowingCount() const
257 {
258 return variantNarrowingCount;
259 }
260
261 inline void
incrementMbCount(Int64 i)262 RewritingContext::incrementMbCount(Int64 i)
263 {
264 mbCount += i;
265 }
266
267 inline void
incrementEqCount(Int64 i)268 RewritingContext::incrementEqCount(Int64 i)
269 {
270 eqCount += i;
271 }
272
273 inline void
incrementRlCount(Int64 i)274 RewritingContext::incrementRlCount(Int64 i)
275 {
276 rlCount += i;
277 }
278
279 inline void
incrementNarrowingCount(Int64 i)280 RewritingContext::incrementNarrowingCount(Int64 i)
281 {
282 narrowingCount += i;
283 }
284
285 inline void
incrementVariantNarrowingCount(Int64 i)286 RewritingContext::incrementVariantNarrowingCount(Int64 i)
287 {
288 variantNarrowingCount += i;
289 }
290
291
292 inline void
clearCount()293 RewritingContext::clearCount()
294 {
295 mbCount = 0;
296 eqCount = 0;
297 rlCount = 0;
298 }
299
300 inline void
addInCount(const RewritingContext & other)301 RewritingContext::addInCount(const RewritingContext& other)
302 {
303 mbCount += other.mbCount;
304 eqCount += other.eqCount;
305 rlCount += other.rlCount;
306
307 narrowingCount += other.narrowingCount;
308 variantNarrowingCount += other.variantNarrowingCount;
309 }
310
311 inline void
transferCount(RewritingContext & other)312 RewritingContext::transferCount(RewritingContext& other)
313 {
314 mbCount += other.mbCount;
315 other.mbCount = 0;
316 eqCount += other.eqCount;
317 other.eqCount = 0;
318 rlCount += other.rlCount;
319 other.rlCount = 0;
320
321 narrowingCount += other.narrowingCount;
322 other.narrowingCount = 0;
323 variantNarrowingCount += other.variantNarrowingCount;
324 other.variantNarrowingCount = 0;
325 }
326
327 inline bool
builtInReplace(DagNode * old,DagNode * replacement)328 RewritingContext::builtInReplace(DagNode* old, DagNode* replacement)
329 {
330 bool trace = traceFlag;
331 if (trace)
332 {
333 tracePreEqRewrite(old, 0, BUILTIN);
334 if (traceAbort())
335 return false;
336 }
337 replacement->overwriteWithClone(old);
338 ++eqCount;
339 if (trace)
340 tracePostEqRewrite(old);
341 return true;
342 }
343
344 #endif
345