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 // Implementation for AC/ACU matcher that works on red-black trees.
25 //
26
27 local_inline int
eliminateBoundVariables(Substitution & solution)28 ACU_LhsAutomaton::eliminateBoundVariables(Substitution& solution)
29 {
30 nrUnboundVariables = 0;
31 Term* identity = topSymbol->getIdentity();
32 FOR_EACH_CONST(i, Vector<TopVariable>, topVariables)
33 {
34 DagNode* d = solution.value(i->index);
35 if (d != 0)
36 {
37 if (d->symbol() == topSymbol)
38 return UNDECIDED;
39 if (identity == 0 || !(identity->equal(d)))
40 {
41 ACU_SlowIter j;
42 if (current.getSize() == 0 || !(current.find(d, j)))
43 return false;
44 int multiplicity = i->multiplicity;
45 if (j.getMultiplicity() < multiplicity)
46 return false;
47 current.deleteMult(j, multiplicity);
48 matchedMultiplicity += multiplicity;
49 }
50 }
51 else
52 ++nrUnboundVariables;
53 }
54 return true;
55 }
56
57 local_inline bool
eliminateGroundAliens()58 ACU_LhsAutomaton::eliminateGroundAliens()
59 {
60 FOR_EACH_CONST(i, Vector<GroundAlien>, groundAliens)
61 {
62 ACU_SlowIter j;
63 if (current.getSize() == 0 || !(current.find(i->term, j)))
64 return false;
65 int multiplicity = i->multiplicity;
66 if (j.getMultiplicity() < multiplicity)
67 return false;
68 current.deleteMult(j, multiplicity);
69 matchedMultiplicity += multiplicity;
70 }
71 return true;
72 }
73
74 local_inline bool
eliminateGroundedOutAliens(Substitution & solution)75 ACU_LhsAutomaton::eliminateGroundedOutAliens(Substitution& solution)
76 {
77 FOR_EACH_CONST(i, Vector<NonGroundAlien>, groundedOutAliens)
78 {
79 Term* t = i->term;
80 Assert(t != 0, "shouldn't be running on unstable terms");
81 ACU_SlowIter j;
82 if (current.getSize() != 0 &&
83 current.findFirstPotentialMatch(t, solution, j))
84 {
85 LhsAutomaton* a = i->automaton;
86 DagNode* d = j.getDagNode();
87 do
88 {
89 Subproblem* sp;
90 if (a->match(d, solution, sp))
91 {
92 Assert(sp == 0, "grounded out alien gave rise to subproblem!");
93 int multiplicity = i->multiplicity;
94 if (j.getMultiplicity() < multiplicity)
95 return false;
96 current.deleteMult(j, multiplicity);
97 matchedMultiplicity += multiplicity;
98 goto nextGroundedOutAlien;
99 }
100 j.next();
101 if (!j.valid())
102 break;
103 d = j.getDagNode();
104 }
105 while (t->partialCompare(solution, d) != Term::GREATER);
106 }
107 return false;
108 nextGroundedOutAlien:
109 ;
110 }
111 return true;
112 }
113
114 int
greedyMatch(ACU_TreeDagNode * subject,Substitution & solution,ACU_ExtensionInfo * extensionInfo)115 ACU_LhsAutomaton::greedyMatch(ACU_TreeDagNode* subject,
116 Substitution& solution,
117 ACU_ExtensionInfo* extensionInfo)
118 {
119 local.copy(solution); // greedy matching is speculative so make a copy
120 scratch.copy(solution); // keep a scratch copy as well
121 FOR_EACH_CONST(i, Vector<NonGroundAlien>, nonGroundAliens)
122 {
123 Term* t = i->term;
124 Assert(t != 0, "shouldn't be running on unstable terms");
125 ACU_SlowIter j;
126 if (current.getSize() != 0 &&
127 current.findFirstPotentialMatch(t, solution, j))
128 {
129 int multiplicity = i->multiplicity;
130 LhsAutomaton* a = i->automaton;
131 DagNode* d = j.getDagNode();
132 do
133 {
134 if (j.getMultiplicity() >= multiplicity)
135 {
136 Subproblem* sp;
137 if (a->match(d, scratch, sp))
138 {
139 if (sp != 0)
140 {
141 //
142 // On a hiding to nothing so pack up and go home.
143 //
144 delete sp;
145 return UNDECIDED;
146 }
147 local.copy(scratch); // preserve any new bindings
148 current.deleteMult(j, multiplicity);
149 matchedMultiplicity += multiplicity;
150 goto nextNonGroundAlien;
151 }
152 scratch.copy(local); // restore scratch copy
153 }
154 j.next();
155 if (!j.valid())
156 break;
157 d = j.getDagNode();
158 }
159 while (t->partialCompare(solution, d) != Term::GREATER);
160 }
161 return ((i - nonGroundAliens.begin()) < nrIndependentAliens) ?
162 false : UNDECIDED;
163 nextNonGroundAlien:
164 ;
165 }
166 if (greedyPureMatch(subject, local, extensionInfo))
167 {
168 solution.copy(local);
169 return true;
170 }
171 //
172 // When the pure matching step fails we always treat it as
173 // UNDECIDED for safety.
174 //
175 return UNDECIDED;
176 }
177
178 local_inline bool
tryToBindVariable(const TopVariable & tv,Substitution & solution)179 ACU_LhsAutomaton::tryToBindVariable(const TopVariable& tv,
180 Substitution& solution)
181 {
182 //
183 // Try to assign one thing to variable.
184 //
185 int multiplicity = tv.multiplicity;
186 if (multiplicity == 1)
187 {
188 //
189 // Choose first subject with low enough sort.
190 //
191 ACU_SlowIter j(current);
192 do
193 {
194 DagNode* d = j.getDagNode();
195 if (d->leq(tv.sort))
196 {
197 solution.bind(tv.index, d);
198 current.deleteMult(j, 1);
199 ++matchedMultiplicity;
200 return true;
201 }
202 j.next();
203 }
204 while (j.valid());
205 }
206 else
207 {
208 //
209 // Try first subject with high enough
210 // multiplicity and give up if sort too big.
211 //
212 ACU_SlowIter j;
213 if (current.findGeqMult(multiplicity, j))
214 {
215 DagNode* d = j.getDagNode();
216 if (d->leq(tv.sort))
217 {
218 solution.bind(tv.index, d);
219 current.deleteMult(j, multiplicity);
220 matchedMultiplicity += multiplicity;
221 return true;
222 }
223 }
224 }
225 //
226 // If we weren't able to assign a subject we can still
227 // try the identity element.
228 //
229 if (tv.takeIdentity)
230 {
231 solution.bind(tv.index, topSymbol->getIdentityDag());
232 return true;
233 }
234 return false;
235 }
236
237 DagNode*
makeHighMultiplicityAssignment(int multiplicity,Sort * sort,ACU_Tree & tree)238 ACU_LhsAutomaton::makeHighMultiplicityAssignment(int multiplicity,
239 Sort* sort,
240 ACU_Tree& tree)
241 {
242 ACU_SlowIter i;
243 if (!(tree.findGeqMult(multiplicity, i)))
244 return 0;
245 DagNode* d = i.getDagNode();
246 int currentSortIndex = d->getSortIndex();
247 if (!leq(currentSortIndex, sort))
248 return 0;
249 //
250 // We have a legal assignment; now try to find a "better" one.
251 //
252 int m = i.getMultiplicity();
253 int a = m / multiplicity;
254 Assert(a > 0, "multiplicity error");
255 if (a > 1)
256 {
257 currentSortIndex = topSymbol->computeMultSortIndex(currentSortIndex,
258 currentSortIndex,
259 a - 1);
260 if (!leq(currentSortIndex, sort))
261 {
262 tree.deleteMult(i, multiplicity);
263 return d; // quit trying to improve substitution
264 }
265 }
266 //
267 // We build the details in the reusable matched vector.
268 //
269 matched.clear();
270 do
271 {
272 matched.append(ACU_DagNode::Pair(d, a));
273 tree.deleteMult(i, a * multiplicity);
274 if (tree.getSize() == 0 ||
275 !(tree.findGeqMult(multiplicity, i)))
276 break;
277 d = i.getDagNode();
278 m = i.getMultiplicity();
279 a = m / multiplicity;
280 Assert(a > 0, "multiplicity error");
281 currentSortIndex = topSymbol->computeMultSortIndex(currentSortIndex,
282 d->getSortIndex(),
283 a);
284 }
285 while (leq(currentSortIndex, sort));
286 //
287 // Now make the assignment.
288 //
289 int nrMatched = matched.length();
290 if (nrMatched == 1 && matched[0].multiplicity == 1)
291 return matched[0].dagNode;
292
293 ACU_DagNode* d2 = new ACU_DagNode(topSymbol, nrMatched, ACU_DagNode::ASSIGNMENT);
294 ArgVec<ACU_DagNode::Pair>::iterator dest = d2->argArray.begin();
295 FOR_EACH_CONST(i, Vector<ACU_DagNode::Pair>, matched)
296 *dest++ = *i;
297 return d2;
298 }
299
300 local_inline bool
tryToBindLastVariable(ACU_TreeDagNode * subject,const TopVariable & tv,Substitution & solution)301 ACU_LhsAutomaton::tryToBindLastVariable(ACU_TreeDagNode* subject,
302 const TopVariable& tv,
303 Substitution& solution)
304 {
305 int multiplicity = tv.multiplicity;
306 if (multiplicity == 1)
307 {
308 if (current.getSize() == 1 && current.getMaxMult() == 1)
309 {
310 //
311 // Just one subject left so try to assign it.
312 //
313 DagNode* d = current.getSoleDagNode();
314 if (d->leq(tv.sort))
315 {
316 solution.bind(tv.index, d);
317 current.clear(); // no need to update matchedMultiplicity
318 return true;
319 }
320 }
321 else
322 {
323 {
324 //
325 // First see if we can give it everything.
326 //
327 ACU_TreeDagNode* t = new ACU_TreeDagNode(topSymbol, current);
328 int index = current.computeBaseSort(topSymbol);
329 if (leq(index, tv.sort))
330 {
331 if (subject->isReduced() && topSymbol->sortConstraintFree())
332 {
333 t->setSortIndex(index);
334 t->setReduced();
335 }
336 solution.bind(tv.index, t);
337 current.clear(); // no need to update matchedMultiplicity
338 return true;
339 }
340 }
341 if (matchAtTop && matchedMultiplicity >= 1)
342 {
343 //
344 // Plan B: We must have extension so try assigning
345 // just one subject.
346 //
347 ACU_SlowIter j(current);
348 do
349 {
350 DagNode* d = j.getDagNode();
351 if (d->leq(tv.sort))
352 {
353 solution.bind(tv.index, d);
354 current.deleteMult(j, 1);
355 ++matchedMultiplicity;
356 return true;
357 }
358 j.next();
359 }
360 while (j.valid());
361 }
362 }
363 }
364 else
365 {
366 //
367 // Last unbound variable has multiplicity >= 2.
368 //
369 if (matchAtTop)
370 {
371 DagNode* d = makeHighMultiplicityAssignment(multiplicity,
372 tv.sort,
373 current);
374 if (d != 0)
375 {
376 solution.bind(tv.index, d);
377 matchedMultiplicity = 2; // wrong but good enough
378 return true;
379 }
380 }
381 else
382 {
383 int size = current.getSize();
384 if (size == 1 && current.getSoleMultiplicity() == multiplicity)
385 {
386 DagNode* d = current.getSoleDagNode();
387 if (d->leq(tv.sort))
388 {
389 solution.bind(tv.index, d);
390 current.clear(); // no need to update matchedMultiplicity
391 return true;
392 }
393 return false;
394 }
395
396 ACU_DagNode* d =
397 new ACU_DagNode(topSymbol,current.getSize(), ACU_DagNode::ASSIGNMENT);
398 ArgVec<ACU_DagNode::Pair>::iterator dest = d->argArray.begin();
399 ACU_SlowIter i(current);
400 do
401 {
402 int m = i.getMultiplicity();
403 if (m % multiplicity != 0)
404 return false;
405 dest->dagNode = i.getDagNode();
406 dest->multiplicity = m / multiplicity;
407 ++dest;
408 i.next();
409 }
410 while (i.valid());
411 int index = d->argVecComputeBaseSort();
412 if (!leq(index, tv.sort))
413 return false;
414 if (subject->isReduced() && topSymbol->sortConstraintFree())
415 {
416 d->setSortIndex(index);
417 d->setReduced();
418 }
419 solution.bind(tv.index, d);
420 current.clear(); // no need to update matchedMultiplicity
421 return true;
422 }
423 }
424 //
425 // Last hope: see if we can assign the identity.
426 //
427 if (matchAtTop && matchedMultiplicity >= 2 && tv.takeIdentity)
428 {
429 solution.bind(tv.index, topSymbol->getIdentityDag());
430 return true;
431 }
432 return false;
433 }
434
435 bool
greedyPureMatch(ACU_TreeDagNode * subject,Substitution & solution,ACU_ExtensionInfo * extensionInfo)436 ACU_LhsAutomaton::greedyPureMatch(ACU_TreeDagNode* subject,
437 Substitution& solution,
438 ACU_ExtensionInfo* extensionInfo)
439 {
440 //
441 // Greedy pure matching can fail for so many reasons
442 // in the red-black case, we don't bother trying to
443 // detect true failure: false always means UNDECIDED.
444 //
445 FOR_EACH_CONST(i, Vector<TopVariable>, topVariables)
446 {
447 if (solution.value(i->index) == 0)
448 {
449 --nrUnboundVariables;
450 if (current.getSize() == 0)
451 {
452 if (!(i->takeIdentity))
453 return false;
454 solution.bind(i->index, topSymbol->getIdentityDag());
455 if (nrUnboundVariables == 0)
456 break;
457 }
458 else
459 {
460 if (nrUnboundVariables == 0)
461 {
462 if (!tryToBindLastVariable(subject, *i, solution))
463 return false;
464 break;
465 }
466 else
467 {
468 if (!tryToBindVariable(*i, solution))
469 return false;
470 }
471 }
472 }
473 }
474
475 if (current.getSize() == 0)
476 {
477 //
478 // Everything matched; fill out empty extension if needed.
479 //
480 if (extensionInfo != 0)
481 {
482 extensionInfo->setValidAfterMatch(true);
483 extensionInfo->setMatchedWhole(true);
484 }
485 }
486 else
487 {
488 //
489 // Stuff left over; see if we can put it in the extension.
490 //
491 if (extensionInfo != 0 && matchedMultiplicity >= 2)
492 {
493 extensionInfo->setValidAfterMatch(true);
494 extensionInfo->setMatchedWhole(false);
495 if (current.getSize() == 1 && current.getMaxMult() == 1)
496 extensionInfo->setUnmatched(current.getSoleDagNode());
497 else
498 extensionInfo->setUnmatched(new ACU_TreeDagNode(topSymbol, current));
499 }
500 else
501 return false;
502 }
503 return true;
504 }
505
506 int
treeMatch(ACU_TreeDagNode * subject,Substitution & solution,Subproblem * & returnedSubproblem,ACU_ExtensionInfo * extensionInfo)507 ACU_LhsAutomaton::treeMatch(ACU_TreeDagNode* subject,
508 Substitution& solution,
509 Subproblem*& returnedSubproblem,
510 ACU_ExtensionInfo* extensionInfo)
511 {
512 current = subject->getTree(); // deep copy
513 if (current.getMaxMult() < maxPatternMultiplicity)
514 return false;
515 //
516 // Eliminate subpatterns that must match a specific subterm
517 // in the subject.
518 //
519 matchedMultiplicity = 0; // so we know when we've matched at least 2 subjects
520 int r = eliminateBoundVariables(solution);
521 if (r != true)
522 return r;
523 if (!eliminateGroundAliens() || !eliminateGroundedOutAliens(solution))
524 return false;
525 if (extensionInfo == 0 && nrUnboundVariables == 1 && nonGroundAliens.empty())
526 {
527 //
528 // Forced lone variable case.
529 //
530 FOR_EACH_CONST(i, Vector<TopVariable>, topVariables)
531 {
532 if (solution.value(i->index) == 0)
533 return forcedLoneVariableCase(subject, *i, solution, returnedSubproblem);
534 }
535 CantHappen("didn't find unbound variable");
536 }
537 if (matchStrategy == FULL)
538 {
539 Assert(nrUnboundVariables <= 1, "nrUnboundVariables = " << nrUnboundVariables);
540 if (nrUnboundVariables != 1)
541 return UNDECIDED; // should be smarter
542 if (current.getSize() == 0)
543 return UNDECIDED; // should be smarter
544 if (current.getSize() == 1 && current.getMaxMult() == 1)
545 return UNDECIDED; // should be smarter
546 //
547 // The only way we can be here is if we have a nonground alien
548 // and a collector variable, and no extension.
549 //
550 Assert(nonGroundAliens.length() == 1,
551 "wrong number of nonGroundAliens" << nonGroundAliens.length());
552 Assert(extensionInfo == 0, "should not have extension");
553
554 FOR_EACH_CONST(i, Vector<TopVariable>, topVariables)
555 {
556 if (solution.value(i->index) == 0)
557 {
558 Assert(i->multiplicity == 1, "collector multiplicity = " << i->multiplicity);
559 returnedSubproblem =
560 new ACU_LazySubproblem(subject,
561 current,
562 solution,
563 nonGroundAliens[0].automaton,
564 nonGroundAliens[0].term,
565 i->index,
566 i->sort);
567 return true;
568 }
569 }
570 CantHappen("didn't find unbound variable");
571 }
572 //
573 // Match everything else using greedy algorithms.
574 //
575 return greedyMatch(subject, solution, extensionInfo);
576 }
577
578 bool
forcedLoneVariableCase(ACU_TreeDagNode * subject,const TopVariable & tv,Substitution & solution,Subproblem * & returnedSubproblem)579 ACU_LhsAutomaton::forcedLoneVariableCase(ACU_TreeDagNode* subject,
580 const TopVariable& tv,
581 Substitution& solution,
582 Subproblem*& returnedSubproblem)
583 {
584 if (current.getSize() == 0)
585 {
586 //
587 // Special case: assign identity.
588 //
589 if (tv.takeIdentity)
590 {
591 solution.bind(tv.index, topSymbol->getIdentityDag());
592 return true;
593 }
594 return false;
595 }
596
597 int multiplicity = tv.multiplicity;
598 if (current.getSize() == 1 && current.getSoleMultiplicity() == multiplicity)
599 {
600 //
601 // Special case: assign one subject.
602 //
603 DagNode* d = current.getSoleDagNode();
604 if (d->leq(tv.sort))
605 {
606 solution.bind(tv.index, d);
607 return true;
608 }
609 return false;
610 }
611 //
612 // General case: need to assign everything.
613 //
614 ACU_BaseDagNode* b;
615 if (multiplicity == 1)
616 b = new ACU_TreeDagNode(topSymbol, current);
617 else
618 {
619 ACU_DagNode* d = new ACU_DagNode(topSymbol, current.getSize(), ACU_DagNode::ASSIGNMENT);
620 ArgVec<ACU_DagNode::Pair>::iterator dest = d->argArray.begin();
621 ACU_SlowIter i(current);
622 do
623 {
624 int m = i.getMultiplicity();
625 if (m % multiplicity != 0)
626 return false;
627 dest->dagNode = i.getDagNode();
628 dest->multiplicity = m / multiplicity;
629 ++dest;
630 i.next();
631 }
632 while (i.valid());
633 b = d;
634 }
635 if (b->checkSort(tv.sort, returnedSubproblem))
636 {
637 solution.bind(tv.index, b);
638 if (subject->isReduced() && b->getSortIndex() != Sort::SORT_UNKNOWN)
639 b->setReduced();
640 return true;
641 }
642 return false;
643 }
644