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 // Code for commands that do rewriting.
25 //
26 #ifdef QUANTIFY_REWRITING
27 #include "quantify.h"
28 #endif
29
30 void
clearContinueInfo()31 Interpreter::clearContinueInfo()
32 {
33 delete savedContext;
34 delete savedMatchSearchState;
35 delete savedUnificationProblem;
36 delete savedRewriteSequenceSearch;
37 delete savedStrategicSearch;
38 savedContext = 0;
39 savedMatchSearchState = 0;
40 savedUnificationProblem = 0;
41 savedRewriteSequenceSearch = 0;
42 savedStrategicSearch = 0;
43 continueFunc = 0;
44 if (savedModule != 0)
45 {
46 (void) savedModule->unprotect();
47 savedModule = 0;
48 }
49 }
50
51 DagNode*
makeDag(Term * subjectTerm)52 Interpreter::makeDag(Term* subjectTerm)
53 {
54 subjectTerm = subjectTerm->normalize(false);
55 NatSet eagerVariables;
56 Vector<int> problemVariables;
57 subjectTerm->markEager(0, eagerVariables, problemVariables);
58 DagNode* d = subjectTerm->term2Dag();
59 subjectTerm->deepSelfDestruct();
60 return d;
61 }
62
63 DagNode*
makeDag(const Vector<Token> & subject)64 Interpreter::makeDag(const Vector<Token>& subject)
65 {
66 if (Term* s = currentModule->getFlatModule()->parseTerm(subject))
67 return makeDag(s);
68 return 0;
69 }
70
71 void
startUsingModule(VisibleModule * module)72 Interpreter::startUsingModule(VisibleModule* module)
73 {
74 clearContinueInfo();
75 UserLevelRewritingContext::clearTrialCount();
76 if (getFlag(AUTO_CLEAR_MEMO))
77 module->clearMemo();
78 if (getFlag(AUTO_CLEAR_PROFILE))
79 module->clearProfile();
80 module->protect();
81 }
82
83 void
beginRewriting(bool debug)84 Interpreter::beginRewriting(bool debug)
85 {
86 if (debug)
87 UserLevelRewritingContext::setDebug();
88 #ifdef QUANTIFY_REWRITING
89 quantify_start_recording_data();
90 #endif
91 }
92
93 void
printModifiers(Int64 number,Int64 number2)94 Interpreter::printModifiers(Int64 number, Int64 number2)
95 {
96 if (number != NONE || number2 != NONE)
97 {
98 cout << '[';
99 if (number != NONE)
100 cout << number;
101 if (number2 != NONE)
102 cout << ", " << number2;
103 cout << "] ";
104 }
105 cout << "in " << currentModule << " : ";
106 }
107
108 void
printTiming(Int64 nrRewrites,Int64 cpu,Int64 real)109 Interpreter::printTiming(Int64 nrRewrites, Int64 cpu, Int64 real)
110 {
111 cout << " in " << cpu / 1000 << "ms cpu (" << real / 1000 << "ms real) (";
112 if (cpu > 0)
113 cout << (1000000 * nrRewrites) / cpu;
114 else
115 cout << '~';
116 cout << " rewrites/second)";
117 }
118
119 void
printStats(const Timer & timer,RewritingContext & context,bool timingFlag)120 Interpreter::printStats(const Timer& timer, RewritingContext& context, bool timingFlag)
121 {
122 Int64 nrRewrites = context.getTotalCount();
123 cout << "rewrites: " << nrRewrites;
124 Int64 real;
125 Int64 virt;
126 Int64 prof;
127 if (timingFlag && timer.getTimes(real, virt, prof))
128 printTiming(nrRewrites, prof, real);
129 cout << '\n';
130 if (getFlag(SHOW_BREAKDOWN))
131 {
132 cout << "mb applications: " << context.getMbCount() <<
133 " equational rewrites: " << context.getEqCount() <<
134 " rule rewrites: " << context.getRlCount() <<
135 " variant narrowing steps: " << context.getVariantNarrowingCount() <<
136 " narrowing steps: " << context.getNarrowingCount() << '\n';
137 }
138 }
139
140 void
endRewriting(Timer & timer,UserLevelRewritingContext * context,VisibleModule * module,ContinueFuncPtr cf)141 Interpreter::endRewriting(Timer& timer,
142 UserLevelRewritingContext* context,
143 VisibleModule* module,
144 ContinueFuncPtr cf)
145 {
146 timer.stop();
147 #ifdef QUANTIFY_REWRITING
148 quantify_stop_recording_data();
149 #endif
150 clearContinueInfo(); // just in case debugger left info
151 if (UserLevelRewritingContext::aborted())
152 {
153 delete context;
154 (void) module->unprotect();
155 }
156 else
157 {
158 if (getFlag(SHOW_STATS))
159 printStats(timer, *context, getFlag(SHOW_TIMING));
160 DagNode* r = context->root();
161 cout << "result " << r->getSort() << ": " << r << '\n';
162 cout.flush();
163 if (xmlBuffer != 0)
164 {
165 xmlBuffer->generateResult(*context,
166 timer,
167 getFlag(SHOW_STATS),
168 getFlag(SHOW_TIMING),
169 getFlag(SHOW_BREAKDOWN));
170 }
171
172 if (cf == 0)
173 {
174 delete context;
175 (void) module->unprotect();
176 }
177 else
178 {
179 savedContext = context;
180 savedModule = module;
181 continueFunc = cf;
182 }
183 }
184 UserLevelRewritingContext::clearDebug(); // even if we didn't start in debug mode
185 }
186
187 #if 1
188 //int CONVERT_THRESHOLD = 8;
189 //int MERGE_THRESHOLD = 16;
190
191 void
reduce(const Vector<Token> & subject,bool debug)192 Interpreter::reduce(const Vector<Token>& subject, bool debug)
193 {
194 if (DagNode* d = makeDag(subject))
195 {
196 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
197 if (getFlag(SHOW_COMMAND))
198 {
199 UserLevelRewritingContext::beginCommand();
200 cout << "reduce in " << currentModule << " : " << d << " ." << endl;
201 if (xmlBuffer != 0)
202 xmlBuffer->generateReduce(d);
203 }
204 VisibleModule* fm = currentModule->getFlatModule();
205 startUsingModule(fm);
206 beginRewriting(debug);
207 Timer timer(getFlag(SHOW_TIMING));
208 context->reduce();
209 endRewriting(timer, context, fm);
210 }
211 }
212 #else
213 int CONVERT_THRESHOLD;
214 int MERGE_THRESHOLD;
215
216 void
reduce(const Vector<Token> & subject,bool debug)217 Interpreter::reduce(const Vector<Token>& subject, bool debug)
218 {
219 if (DagNode* d = makeDag(subject))
220 {
221 for (int i = 0; i < 2; ++i)
222 {
223 for (CONVERT_THRESHOLD = 0; CONVERT_THRESHOLD <= 20; CONVERT_THRESHOLD += 1)
224 {
225 for (MERGE_THRESHOLD = 0; MERGE_THRESHOLD <= 20; MERGE_THRESHOLD += 1)
226 {
227 cout << "CONVERT_THRESHOLD = " << CONVERT_THRESHOLD <<
228 "\tMERGE_THRESHOLD = " << MERGE_THRESHOLD << endl;
229 DagNode* d = makeDag(subject);
230 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
231 VisibleModule* fm = currentModule->getFlatModule();
232 startUsingModule(fm);
233 beginRewriting(debug);
234 Timer timer(getFlag(SHOW_TIMING));
235 context->reduce();
236 endRewriting(timer, context, fm);
237 }
238 }
239 }
240 }
241 }
242 #endif
243
244 void
rewrite(const Vector<Token> & subject,Int64 limit,bool debug)245 Interpreter::rewrite(const Vector<Token>& subject, Int64 limit, bool debug)
246 {
247 if (DagNode* d = makeDag(subject))
248 {
249 if (getFlag(SHOW_COMMAND))
250 {
251 UserLevelRewritingContext::beginCommand();
252 cout << "rewrite ";
253 if (limit != NONE)
254 cout << '[' << limit << "] ";
255 cout << "in " << currentModule << " : " << d << " ." << endl;
256 if (xmlBuffer != 0)
257 xmlBuffer->generateRewrite(d, limit);
258 }
259
260 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
261 VisibleModule* fm = currentModule->getFlatModule();
262
263 startUsingModule(fm);
264 if (getFlag(AUTO_CLEAR_RULES))
265 fm->resetRules();
266 beginRewriting(debug);
267 Timer timer(getFlag(SHOW_TIMING));
268 context->ruleRewrite(limit);
269 endRewriting(timer, context, fm, &Interpreter::rewriteCont);
270 }
271 }
272
273 void
rewriteCont(Int64 limit,bool debug)274 Interpreter::rewriteCont(Int64 limit, bool debug)
275 {
276 UserLevelRewritingContext* context = savedContext;
277 VisibleModule* fm = savedModule;
278 savedContext = 0;
279 savedModule = 0;
280 continueFunc = 0;
281 if (xmlBuffer != 0 && getFlag(SHOW_COMMAND))
282 xmlBuffer->generateContinue("rewrite", fm, limit);
283 context->clearCount();
284 beginRewriting(debug);
285 Timer timer(getFlag(SHOW_TIMING));
286 context->ruleRewrite(limit);
287 endRewriting(timer, context, fm, &Interpreter::rewriteCont);
288 }
289
290 void
fRewrite(const Vector<Token> & subject,Int64 limit,Int64 gas,bool debug)291 Interpreter::fRewrite(const Vector<Token>& subject, Int64 limit, Int64 gas, bool debug)
292 {
293 if (DagNode* d = makeDag(subject))
294 {
295 if (getFlag(SHOW_COMMAND))
296 {
297 UserLevelRewritingContext::beginCommand();
298 cout << "frewrite ";
299 printModifiers(limit, gas);
300 cout << d << " ." << endl;
301 if (xmlBuffer != 0)
302 xmlBuffer->generateFrewrite(d, limit, gas);
303 }
304 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
305 context->setObjectMode(ObjectSystemRewritingContext::FAIR);
306 VisibleModule* fm = currentModule->getFlatModule();
307
308 startUsingModule(fm);
309 if (getFlag(AUTO_CLEAR_RULES))
310 fm->resetRules();
311 beginRewriting(debug);
312 Timer timer(getFlag(SHOW_TIMING));
313 context->fairRewrite(limit, (gas == NONE) ? 1 : gas);
314 endRewriting(timer, context, fm, &Interpreter::fRewriteCont);
315 }
316 }
317
318 void
fRewriteCont(Int64 limit,bool debug)319 Interpreter::fRewriteCont(Int64 limit, bool debug)
320 {
321 UserLevelRewritingContext* context = savedContext;
322 VisibleModule* fm = savedModule;
323 savedContext = 0;
324 savedModule = 0;
325 continueFunc = 0;
326 if (xmlBuffer != 0 && getFlag(SHOW_COMMAND))
327 xmlBuffer->generateContinue("frewrite", fm, limit);
328 context->clearCount();
329 beginRewriting(debug);
330 Timer timer(getFlag(SHOW_TIMING));
331 context->fairContinue(limit);
332 endRewriting(timer, context, fm, &Interpreter::fRewriteCont);
333 }
334
335 void
cont(Int64 limit,bool debug)336 Interpreter::cont(Int64 limit, bool debug)
337 {
338 if (limit != 0)
339 {
340 if (continueFunc != 0)
341 (this->*continueFunc)(limit, debug);
342 else
343 IssueWarning("can't continue.");
344 }
345 }
346
347 void
creduce(const Vector<Token> & subject)348 Interpreter::creduce(const Vector<Token>& subject)
349 {
350 #ifdef COMPILER
351 if (DagNode* d = makeDag(subject))
352 {
353 if (makeExecutable(currentModule, getFlag(COMPILE_COUNT)))
354 {
355 if (getFlag(SHOW_COMMAND))
356 {
357 UserLevelRewritingContext::beginCommand();
358 cout << "creduce in " << currentModule << " : " << d << " ." << endl;
359 }
360 //
361 // Write dag to file, run executable and read result from file.
362 //
363 outputGraph(d);
364 runExecutable();
365 Int64 nrRewrites;
366 Int64 cpu;
367 Int64 real;
368 DagNode* r = inputGraph(nrRewrites, cpu, real);
369 //
370 // Print number of rewrites, timing and result.
371 //
372 if (getFlag(SHOW_STATS))
373 {
374 cout << "rewrites: " << nrRewrites;
375 if (getFlag(SHOW_TIMING))
376 printTiming(nrRewrites, cpu, real);
377 cout << '\n';
378 }
379 cout << "result " << r->getSort() << ": " << r << '\n';
380 cout.flush();
381 }
382 }
383 #endif
384 }
385
386 #include "stackMachine.hh"
387 #include "stackMachineRhsCompiler.hh"
388 #include "frame.hh"
389
390 void
sreduce(const Vector<Token> & subject)391 Interpreter::sreduce(const Vector<Token>& subject)
392 {
393 if (Term* t = currentModule->getFlatModule()->parseTerm(subject))
394 {
395 //
396 // Partly normalize term (don't flatten).
397 //
398 t = t->normalize(false);
399 //
400 // Set EAGER flag in eager terms since term2InstructionSequence() needs this
401 // to determine subterm sharability.
402 //
403 NatSet eagerVariables;
404 Vector<int> problemVariables;
405 t->markEager(0, eagerVariables, problemVariables);
406 //
407 // Now compile a sequence of instructions to build the term, evaluating alond the way.
408 //
409 Instruction* instructionSequence = t->term2InstructionSequence();
410 //
411 // If some function symbol didn't generate an instruction we get the null sequence to
412 // flag unsupported feature.
413 //
414 if (instructionSequence == 0)
415 {
416 IssueWarning("sreduce unsupported operator (Maude VM compiler).");
417 return;
418 }
419 //
420 // Now run the sequence in a stack machine.
421 //
422 VisibleModule* fm = currentModule->getFlatModule();
423 fm->stackMachineCompile();
424
425 startUsingModule(fm);
426 Timer timer(getFlag(SHOW_TIMING));
427
428 if (getFlag(SHOW_COMMAND))
429 {
430 UserLevelRewritingContext::beginCommand();
431 cout << "sreduce in " << currentModule << " : " << t << " ." << endl;
432 }
433
434 t->deepSelfDestruct();
435 StackMachine sm;
436 DagNode* r = sm.execute(instructionSequence);
437 Int64 nrRewrites = sm.getEqCount();
438 //
439 // End of stack based reduction.
440 //
441 if (getFlag(SHOW_STATS))
442 {
443 cout << "rewrites: " << nrRewrites;
444 Int64 real;
445 Int64 virt;
446 Int64 prof;
447 if (getFlag(SHOW_TIMING) && timer.getTimes(real, virt, prof))
448 printTiming(nrRewrites, prof, real);
449 cout << '\n';
450 }
451 cout << "result " << r->getSort() << ": " << r << '\n';
452 cout.flush();
453 delete instructionSequence;
454 (void) fm->unprotect();
455 }
456 }
457
458 #include "SMT_Info.hh"
459 #include "variableGenerator.hh"
460
461 void
check(const Vector<Token> & subject)462 Interpreter::check(const Vector<Token>& subject)
463 {
464 if (Term* term = currentModule->getFlatModule()->parseTerm(subject))
465 {
466 term = term->normalize(false);
467 DagNode* d = term->term2Dag();
468
469 if (getFlag(SHOW_COMMAND))
470 {
471 UserLevelRewritingContext::beginCommand();
472 cout << "check in " << currentModule << " : " << d << " ." << endl;
473 }
474
475 VisibleModule* fm = currentModule->getFlatModule();
476 startUsingModule(fm);
477
478 const SMT_Info& smtInfo = fm->getSMT_Info();
479 VariableGenerator vg(smtInfo);
480 VariableGenerator::Result result = vg.checkDag(d);
481 if (result == VariableGenerator::BAD_DAG)
482 IssueWarning (*term << ": term " << QUOTE(term) << " is not a valid SMT Boolean expression.");
483 else
484 {
485 cout << "Result from sat solver is: " <<
486 ((result == VariableGenerator::SAT) ? "sat" :
487 ((result == VariableGenerator::UNSAT) ? "unsat" : "undecided")) << endl;
488 }
489
490 term->deepSelfDestruct();
491 fm->unprotect();
492 }
493 }
494
495 void
test(const Vector<Token> & subject)496 Interpreter::test(const Vector<Token>& subject)
497 {
498 }
499