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 search command.
25 //
26
27 #include "equalityConditionFragment.hh"
28 #include "SMT_RewriteSequenceSearch.hh"
29
30 void
printSearchTiming(const Timer & timer,RewriteSequenceSearch * state)31 Interpreter::printSearchTiming(const Timer& timer, RewriteSequenceSearch* state)
32 {
33 if (getFlag(SHOW_STATS))
34 {
35 cout << "states: " << state->getNrStates() << " ";
36 printStats(timer, *(state->getContext()), getFlag(SHOW_TIMING));
37 }
38 }
39
40 void
search(const Vector<Token> & bubble,Int64 limit,Int64 depth,SearchKind searchKind)41 Interpreter::search(const Vector<Token>& bubble, Int64 limit, Int64 depth, SearchKind searchKind)
42 {
43 VisibleModule* fm = currentModule->getFlatModule();
44 Term* initial;
45 int searchType;
46 Term* target;
47 Vector<ConditionFragment*> condition;
48 if (!(fm->parseSearchCommand(bubble, initial, searchType, target, condition)))
49 return;
50 //
51 // Narrowing does not support conditions.
52 //
53 if ((searchKind == NARROW || searchKind == XG_NARROW) && !condition.empty())
54 {
55 IssueWarning(*target << ": conditions are not currently supported for narrowing.");
56 return; // FIXME we should probably deep self destruct initial and condition here.
57 }
58 //
59 // SMT search does not support =>! mode since states are symbolic.
60 // Only equational condition fragments are supported since they need to pushed in to the SMT solver.
61 //
62 Pattern* pattern;
63 if (searchKind == SMT_SEARCH)
64 {
65 if (searchType == SequenceSearch::NORMAL_FORM)
66 {
67 IssueWarning(*target << ": =>! mode is not supported for searching modulo SMT.");
68 return; // FIXME clean up
69 }
70 if (!(fm->validForSMT_Rewriting()))
71 return;
72 }
73 else
74 pattern = new Pattern(target, false, condition);
75
76 //
77 // Regular seach cannot have unbound variables.
78 //
79 if (searchKind == SEARCH && !(pattern->getUnboundVariables().empty()))
80 {
81 IssueWarning(*target << ": variable " <<
82 QUOTE(pattern->index2Variable(pattern->getUnboundVariables().min())) <<
83 " is used before it is bound in the condition of a search command.\n");
84 initial->deepSelfDestruct();
85 delete pattern;
86 return;
87 }
88
89 DagNode* subjectDag = makeDag(initial);
90
91 static const char* searchTypeSymbol[] = { "=>1", "=>+", "=>*", "=>!" };
92 if (getFlag(SHOW_COMMAND))
93 {
94 static const char* searchKindName[] = { "search", "narrow", "xg-narrow", "smt-search" };
95
96 UserLevelRewritingContext::beginCommand();
97 cout << searchKindName[searchKind] << ' ';
98 printModifiers(limit, depth);
99 cout << subjectDag << ' ' << searchTypeSymbol[searchType] << ' ' << target;
100 if (!condition.empty())
101 {
102 cout << " such that ";
103 MixfixModule::printCondition(cout, condition);
104 }
105 cout << " ." << endl;
106
107 if (xmlBuffer != 0)
108 xmlBuffer->generateSearch(subjectDag, pattern, searchTypeSymbol[searchType], limit, depth); // does this work for narrowing?
109 }
110
111 startUsingModule(fm);
112
113 #ifdef QUANTIFY_REWRITING
114 quantify_start_recording_data();
115 #endif
116
117 if (searchKind == SEARCH)
118 {
119 RewriteSequenceSearch* state =
120 new RewriteSequenceSearch(new UserLevelRewritingContext(subjectDag),
121 static_cast<RewriteSequenceSearch::SearchType>(searchType),
122 pattern,
123 depth);
124 Timer timer(getFlag(SHOW_TIMING));
125 doSearching(timer, fm, state, 0, limit);
126 }
127 else if (searchKind == SMT_SEARCH)
128 {
129 const SMT_Info& smtInfo = fm->getSMT_Info();
130 VariableGenerator* vg = new VariableGenerator(smtInfo);
131 RewritingContext* initial = new UserLevelRewritingContext(subjectDag);
132
133 SMT_RewriteSequenceSearch* smtSearch =
134 new SMT_RewriteSequenceSearch(initial,
135 static_cast<RewriteSequenceSearch::SearchType>(searchType),
136 target,
137 condition,
138 smtInfo,
139 vg,
140 depth,
141 0);
142 int solutionNr = 0;
143 while (solutionNr != limit)
144 {
145 if (!(smtSearch->findNextMatch()))
146 break;
147 cout << "\nSolution " << ++solutionNr << endl;
148 UserLevelRewritingContext::printSubstitution(*(smtSearch->getSubstitution()), *smtSearch, smtSearch->getSMT_VarIndices());
149 cout << "where " << smtSearch->getFinalConstraint() << endl;
150 DebugAdvisory("variable number = " << smtSearch->getMaxVariableNumber());
151 /*
152 int stateNr = smtSearch->getCurrentStateNumber();
153 cout << "state number = " << stateNr << endl;
154 cout << "state = " << smtSearch->getState(stateNr) << endl;
155 cout << "constraint = " << smtSearch->getConstraint(stateNr) << endl;
156 cout << "final constraint = " << smtSearch->getFinalConstraint() << endl;
157 cout << "substitution =\n";
158 UserLevelRewritingContext::printSubstitution(*(smtSearch->getSubstitution()), *smtSearch);
159 */
160 }
161 delete smtSearch; // will take initial and vg with it
162 UserLevelRewritingContext::clearDebug();
163 }
164 else
165 {
166 NarrowingSequenceSearch* state = new NarrowingSequenceSearch(new UserLevelRewritingContext(subjectDag),
167 static_cast<NarrowingSequenceSearch::SearchType>(searchType), // HACK
168 pattern,
169 depth,
170 (searchKind == XG_NARROW ?
171 NarrowingSearchState::ALLOW_NONEXEC | NarrowingSearchState::SINGLE_POSITION :
172 NarrowingSearchState::ALLOW_NONEXEC),
173 new FreshVariableSource(fm));
174 Timer timer(getFlag(SHOW_TIMING));
175 doNarrowing(timer, fm, state, 0, limit);
176 }
177 }
178
179 void
doNarrowing(Timer & timer,VisibleModule * module,NarrowingSequenceSearch * state,int solutionCount,int limit)180 Interpreter::doNarrowing(Timer& timer,
181 VisibleModule* module,
182 NarrowingSequenceSearch* state,
183 int solutionCount,
184 int limit)
185 {
186 const VariableInfo* variableInfo = state->getGoal();
187 int i = 0;
188 for (; i != limit; i++)
189 {
190 bool result = state->findNextMatch();
191 if (UserLevelRewritingContext::aborted())
192 break; // HACK: Is this safe - shouldn't we destroy context?
193 if (!result)
194 {
195 cout << ((solutionCount == 0) ? "\nNo solution.\n" : "\nNo more solutions.\n");
196 //printSearchTiming(timer, state);
197 break;
198 }
199
200 ++solutionCount;
201 cout << "\nSolution " << solutionCount << "\n";
202 //printSearchTiming(timer, state);
203 UserLevelRewritingContext::printSubstitution(*(state->getSubstitution()), *variableInfo);
204 if (UserLevelRewritingContext::interrupted())
205 break;
206 }
207
208 #ifdef QUANTIFY_REWRITING
209 quantify_stop_recording_data();
210 #endif
211
212 clearContinueInfo(); // just in case debugger left info
213 //state->getContext()->clearCount();
214 //savedRewriteSequenceSearch = state;
215 //savedSolutionCount = solutionCount;
216 //savedModule = module;
217 //if (i == limit) // possible to continue
218 // continueFunc = &Interpreter::searchCont;
219 UserLevelRewritingContext::clearDebug();
220 }
221
222 void
doSearching(Timer & timer,VisibleModule * module,RewriteSequenceSearch * state,int solutionCount,int limit)223 Interpreter::doSearching(Timer& timer,
224 VisibleModule* module,
225 RewriteSequenceSearch* state,
226 int solutionCount,
227 int limit)
228 {
229 const VariableInfo* variableInfo = state->getGoal();
230 int i = 0;
231 for (; i != limit; i++)
232 {
233 bool result = state->findNextMatch();
234 if (UserLevelRewritingContext::aborted())
235 break; // HACK: Is this safe - shouldn't we destroy context?
236 if (!result)
237 {
238 cout << ((solutionCount == 0) ? "\nNo solution.\n" : "\nNo more solutions.\n");
239 printSearchTiming(timer, state);
240 if (xmlBuffer != 0)
241 {
242 xmlBuffer->generateSearchResult(NONE,
243 state,
244 timer,
245 getFlag(SHOW_STATS),
246 getFlag(SHOW_TIMING),
247 getFlag(SHOW_BREAKDOWN));
248 }
249 break;
250 }
251
252 ++solutionCount;
253 cout << "\nSolution " << solutionCount <<
254 " (state " << state->getStateNr() << ")\n";
255 printSearchTiming(timer, state);
256 UserLevelRewritingContext::printSubstitution(*(state->getSubstitution()), *variableInfo);
257 if (UserLevelRewritingContext::interrupted())
258 break;
259 if (xmlBuffer != 0)
260 {
261 xmlBuffer->generateSearchResult(solutionCount,
262 state,
263 timer,
264 getFlag(SHOW_STATS),
265 getFlag(SHOW_TIMING),
266 getFlag(SHOW_BREAKDOWN));
267 }
268 }
269
270 #ifdef QUANTIFY_REWRITING
271 quantify_stop_recording_data();
272 #endif
273
274 clearContinueInfo(); // just in case debugger left info
275 state->getContext()->clearCount();
276 savedRewriteSequenceSearch = state;
277 savedSolutionCount = solutionCount;
278 savedModule = module;
279 if (i == limit) // possible to continue
280 continueFunc = &Interpreter::searchCont;
281 UserLevelRewritingContext::clearDebug();
282 }
283
284 void
searchCont(Int64 limit,bool)285 Interpreter::searchCont(Int64 limit, bool /* debug */)
286 {
287 RewriteSequenceSearch* state = savedRewriteSequenceSearch;
288 VisibleModule* fm = savedModule;
289 savedRewriteSequenceSearch = 0;
290 savedModule = 0;
291 continueFunc = 0;
292 if (xmlBuffer != 0 && getFlag(SHOW_COMMAND))
293 xmlBuffer->generateContinue("search", fm, limit);
294
295 #ifdef QUANTIFY_REWRITING
296 quantify_start_recording_data();
297 #endif
298
299 Timer timer(getFlag(SHOW_TIMING));
300 doSearching(timer, fm, state, savedSolutionCount, limit);
301 }
302
303 void
showSearchPath(int stateNr)304 Interpreter::showSearchPath(int stateNr)
305 {
306 if (savedRewriteSequenceSearch == 0)
307 {
308 IssueWarning("no state graph.");
309 return;
310 }
311 if (stateNr < 0 || stateNr >= savedRewriteSequenceSearch->getNrStates())
312 {
313 IssueWarning("bad state number.");
314 return;
315 }
316 if (xmlBuffer != 0 && getFlag(SHOW_COMMAND))
317 xmlBuffer->generateShowSearchPath(stateNr);
318 Vector<int> steps;
319 for (int i = stateNr; i != NONE; i = savedRewriteSequenceSearch->getStateParent(i))
320 steps.append(i);
321
322 for (int i = steps.length() - 1; i >= 0; i--)
323 {
324 int sn = steps[i];
325 if (sn != 0)
326 cout << "===[ " << savedRewriteSequenceSearch->getStateRule(sn) << " ]===>\n";
327 DagNode* d = savedRewriteSequenceSearch->getStateDag(sn);
328 cout << "state " << sn << ", " << d->getSort() << ": " << d << '\n';
329 }
330 if (xmlBuffer != 0)
331 xmlBuffer->generateSearchPath(savedRewriteSequenceSearch, stateNr);
332 }
333
334 void
showSearchPathLabels(int stateNr)335 Interpreter::showSearchPathLabels(int stateNr)
336 {
337 if (savedRewriteSequenceSearch == 0)
338 {
339 IssueWarning("no state graph.");
340 return;
341 }
342 if (stateNr < 0 || stateNr >= savedRewriteSequenceSearch->getNrStates())
343 {
344 IssueWarning("bad state number.");
345 return;
346 }
347 Vector<int> steps;
348 for (int i = stateNr; i != NONE; i = savedRewriteSequenceSearch->getStateParent(i))
349 steps.append(i);
350
351 int i = steps.length() - 2;
352 if (i < 0)
353 cout << "Empty path.\n";
354 else
355 {
356 for (; i >= 0; i--)
357 {
358 const Label& label = savedRewriteSequenceSearch->getStateRule(steps[i])->getLabel();
359 if (label.id() == NONE)
360 cout << "(unlabeled rule)\n";
361 else
362 cout << &label << '\n';
363 }
364 }
365 }
366
367 void
showSearchGraph()368 Interpreter::showSearchGraph()
369 {
370 if (savedRewriteSequenceSearch == 0)
371 {
372 IssueWarning("no state graph.");
373 return;
374 }
375 if (xmlBuffer != 0 && getFlag(SHOW_COMMAND))
376 xmlBuffer->generateShowSearchGraph();
377 int nrStates = savedRewriteSequenceSearch->getNrStates();
378 for (int i = 0; i < nrStates; i++)
379 {
380 if (i > 0)
381 cout << '\n';
382 DagNode* d = savedRewriteSequenceSearch->getStateDag(i);
383 cout << "state " << i << ", " << d->getSort() << ": " << d << '\n';
384 const RewriteSequenceSearch::ArcMap& fwdArcs =
385 savedRewriteSequenceSearch->getStateFwdArcs(i);
386 int arcNr = 0;
387 for (RewriteSequenceSearch::ArcMap::const_iterator j = fwdArcs.begin();
388 j != fwdArcs.end(); j++, arcNr++)
389 {
390 cout << "arc " << arcNr << " ===> state " << (*j).first;
391 const set<Rule*>& r = (*j).second;
392 for (set<Rule*>::const_iterator k = r.begin(); k != r.end(); k++)
393 cout << " (" << *k << ')';
394 cout << '\n';
395 }
396 }
397 if (xmlBuffer != 0)
398 xmlBuffer->generateSearchGraph(savedRewriteSequenceSearch);
399 }
400
401 void
getVariants(const Vector<Token> & bubble,Int64 limit,bool irredundant,bool debug)402 Interpreter::getVariants(const Vector<Token>& bubble, Int64 limit, bool irredundant, bool debug)
403 {
404 VisibleModule* fm = currentModule->getFlatModule();
405 Term* initial;
406 Vector<Term*> constraint;
407
408 if (!(fm->parseGetVariantsCommand(bubble, initial, constraint)))
409 return;
410
411 DagNode* d = makeDag(initial);
412 if (getFlag(SHOW_COMMAND))
413 {
414 UserLevelRewritingContext::beginCommand();
415 cout << "get " << (irredundant ? "irredundant variants " : "variants ");
416 if (limit != NONE)
417 cout << '[' << limit << "] ";
418 cout << "in " << currentModule << " : " << d;
419 if (constraint.empty())
420 cout << " ." << endl;
421 else
422 {
423 cout << " such that ";
424 const char* sep = "";
425 FOR_EACH_CONST(i, Vector<Term*>, constraint)
426 {
427 cout << sep << *i;
428 sep = ", ";
429 }
430 cout << " irreducible ." << endl;
431 }
432 }
433
434 startUsingModule(fm);
435 Timer timer(getFlag(SHOW_TIMING));
436
437 FreshVariableGenerator* freshVariableGenerator = new FreshVariableSource(fm);
438 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
439 if (debug)
440 UserLevelRewritingContext::setDebug();
441
442 Vector<DagNode*> blockerDags;
443 FOR_EACH_CONST(i, Vector<Term*>, constraint)
444 {
445 Term* t = *i;
446 t = t->normalize(true); // we don't really need to normalize but we do need to set hash values
447 blockerDags.append(t->term2Dag());
448 t->deepSelfDestruct();
449 }
450 //
451 // Responsibility for deleting context and freshVariableGenerator is passed to ~VariantSearch().
452 //
453 VariantSearch vs(context, blockerDags, freshVariableGenerator, false, irredundant);
454
455 if (!(context->traceAbort()))
456 {
457 const NarrowingVariableInfo& variableInfo = vs.getVariableInfo();
458 if (irredundant)
459 printStats(timer, *context, getFlag(SHOW_TIMING));
460 cout << endl;
461
462 int counter = 0;
463 const Vector<DagNode*>* variant;
464 int nrFreeVariables;
465 int parentIndex;
466 bool moreInLayer;
467 while (counter != limit && (variant = vs.getNextVariant(nrFreeVariables, parentIndex, moreInLayer)))
468 {
469 ++counter;
470 cout << "Variant #" << counter << endl;
471 if (!irredundant)
472 printStats(timer, *context, getFlag(SHOW_TIMING));
473
474 int nrVariables = variant->size() - 1;
475 DagNode* d = (*variant)[nrVariables];
476 cout << d->getSort() << ": " << d << '\n';
477 for (int i = 0; i < nrVariables; ++i)
478 {
479 DagNode* v = variableInfo.index2Variable(i);
480 cout << v << " --> " << (*variant)[i] << endl;
481 }
482 cout << endl;
483 }
484 if (counter != limit)
485 {
486 cout << ((counter == 0) ? "No variants.\n" : "No more variants.\n");
487 if (vs.isIncomplete())
488 IssueWarning("Some variants may have been missed due to incomplete unification algorithm(s).");
489 if (!irredundant)
490 printStats(timer, *context, getFlag(SHOW_TIMING));
491 }
492 }
493 (void) fm->unprotect();
494 UserLevelRewritingContext::clearDebug();
495 }
496
497 void
variantUnify(const Vector<Token> & bubble,Int64 limit,bool debug)498 Interpreter::variantUnify(const Vector<Token>& bubble, Int64 limit, bool debug)
499 {
500 VisibleModule* fm = currentModule->getFlatModule();
501 Vector<Term*> lhs;
502 Vector<Term*> rhs;
503 Vector<Term*> constraint;
504
505 if (!(fm->parseVariantUnifyCommand(bubble, lhs, rhs, constraint)))
506 return;
507
508 if (getFlag(SHOW_COMMAND))
509 {
510 UserLevelRewritingContext::beginCommand();
511 cout << "variant unify ";
512 if (limit != NONE)
513 cout << '[' << limit << "] ";
514 cout << "in " << currentModule << " : ";
515 int nrPairs = lhs.size();
516 for (int i = 0; i < nrPairs; ++i)
517 cout << lhs[i] << " =? " << rhs[i] << ((i == nrPairs - 1) ? " " : " /\\ ");
518 if (constraint.empty())
519 cout << " ." << endl;
520 else
521 {
522 cout << " such that ";
523 const char* sep = "";
524 FOR_EACH_CONST(i, Vector<Term*>, constraint)
525 {
526 cout << sep << *i;
527 sep = ", ";
528 }
529 cout << " irreducible ." << endl;
530 }
531 }
532
533 startUsingModule(fm);
534 Timer timer(getFlag(SHOW_TIMING));
535 FreshVariableGenerator* freshVariableGenerator = new FreshVariableSource(fm);
536 if (debug)
537 UserLevelRewritingContext::setDebug();
538
539 DagNode* d = fm->makeUnificationProblemDag(lhs, rhs);
540 UserLevelRewritingContext* context = new UserLevelRewritingContext(d);
541
542 Vector<DagNode*> blockerDags;
543 FOR_EACH_CONST(i, Vector<Term*>, constraint)
544 {
545 Term* t = *i;
546 t = t->normalize(true); // we don't really need to normalize but we do need to set hash values
547 blockerDags.append(t->term2Dag());
548 t->deepSelfDestruct();
549 }
550
551 //
552 // Responsibility for deleting context and freshVariableGenerator is passed to ~VariantSearch().
553 //
554 VariantSearch vs(context, blockerDags, freshVariableGenerator, true, false);
555
556 if (!(context->traceAbort()))
557 {
558 const NarrowingVariableInfo& variableInfo = vs.getVariableInfo();
559 cout << endl;
560
561 int counter = 0;
562 const Vector<DagNode*>* unifier;
563 int nrFreeVariables;
564 while (counter != limit && (unifier = vs.getNextUnifier(nrFreeVariables)))
565 {
566 ++counter;
567 cout << "Unifier #" << counter << endl;
568 printStats(timer, *context, getFlag(SHOW_TIMING));
569
570 int nrVariables = unifier->size();
571
572 for (int i = 0; i < nrVariables; ++i)
573 {
574 DagNode* v = variableInfo.index2Variable(i);
575 cout << v << " --> " << (*unifier)[i] << endl;
576 }
577 cout << endl;
578 }
579 if (counter != limit)
580 {
581 cout << ((counter == 0) ? "No unifiers.\n" : "No more unifiers.\n");
582 if (vs.isIncomplete())
583 IssueWarning("Some unifiers may have been missed due to incomplete unification algorithm(s).");
584 printStats(timer, *context, getFlag(SHOW_TIMING));
585 }
586 }
587 (void) fm->unprotect();
588 UserLevelRewritingContext::clearDebug();
589 }
590