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 abstract class RuleTable.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 #include "variable.hh"
35
36 // interface class definitions
37 #include "symbol.hh"
38 #include "dagNode.hh"
39 #include "term.hh"
40 #include "subproblem.hh"
41 #include "extensionInfo.hh"
42
43 // core class definitions
44 #include "substitution.hh"
45 #include "rewritingContext.hh"
46 #include "lhsAutomaton.hh"
47 #include "rhsAutomaton.hh"
48 #include "variableInfo.hh"
49 #include "preEquation.hh"
50 #include "sortConstraint.hh"
51 #include "sortConstraintTable.hh"
52
SortConstraintTable()53 SortConstraintTable::SortConstraintTable()
54 {
55 tableComplete = false;
56 }
57
58 local_inline bool
sortConstraintLt(SortConstraint * const & sc1,SortConstraint * const & sc2)59 SortConstraintTable::sortConstraintLt(SortConstraint* const& sc1,
60 SortConstraint* const& sc2)
61 {
62 //
63 // Sort constraints are sorted in the order: largest index (smallest sort) first
64 //
65 return sc2->getSort()->index() < sc1->getSort()->index(); // reverse order
66 // IDEA: might want to weaken comparison and do a stable_sort()
67 // BUT: stable_sort() requires a strict weak ordering - much stronger that
68 // the partial ordering we have on sorts.
69 }
70
71 void
orderSortConstraints()72 SortConstraintTable::orderSortConstraints()
73 {
74 //
75 // sortConstraints may contain sort constraints with variable lhs which have
76 // too low a sort to ever match our symbol. However the sort of our symbol
77 // is itself affected by sort constraints. So we "comb" out usable sort
78 // constraints in successive passes; this is inefficient but we expect the number
79 // of sort constraints to be very small so it's not worth doing anything smarter.
80 //
81 tableComplete = true; // not really complete until we've finished, but pretend it is
82 int nrSortConstraints = sortConstraints.length();
83 if (nrSortConstraints == 0)
84 return;
85 Vector<SortConstraint*> all;
86 all.swap(sortConstraints);
87 bool addedSortConstraint;
88 do
89 {
90 addedSortConstraint = false;
91 for (int i = 0; i < nrSortConstraints; i++)
92 {
93 SortConstraint* sc = all[i];
94 //
95 // Because we set tableComplete = true; acceptSortConstraint() may
96 // inspect the table of sortConstraints accepted so far and make
97 // a finer distinction than it could in offerSortConstraint().
98 //
99 if (sc != 0 && acceptSortConstraint(sc))
100 {
101 sortConstraints.append(sc);
102 all[i] = 0;
103 addedSortConstraint = true;
104 }
105 }
106 }
107 while (addedSortConstraint);
108 sort(sortConstraints.begin(), sortConstraints.end(), sortConstraintLt);
109 }
110
111 void
compileSortConstraints()112 SortConstraintTable::compileSortConstraints()
113 {
114 int nrConstraints = sortConstraints.length();
115 for (int i = 0; i < nrConstraints; i++)
116 sortConstraints[i]->compile(true);
117 }
118
119 void
constrainToSmallerSort2(DagNode * subject,RewritingContext & context)120 SortConstraintTable::constrainToSmallerSort2(DagNode* subject, RewritingContext& context)
121 {
122 int currentSortIndex = subject->getSortIndex();
123 Subproblem* sp;
124 //
125 // We try sort constraints, smallest sort first until one applies or
126 // all remaining sort constraints have sort >= than our current sort.
127 // Whenever we succeed in applying a sort constraint we start again
128 // with the new sort, because earlier sort constraints (via collapse
129 // or variable lhs patterns) may be able to test this new sort.
130 //
131 int nrConstraints = sortConstraints.length();
132 retry:
133 for (int i = 0; i < nrConstraints; i++)
134 {
135 SortConstraint* sc = sortConstraints[i];
136 Sort* s = sc->getSort();
137 if (leq(currentSortIndex, s))
138 break;
139 if (leq(s, currentSortIndex)) // not equal because of previous test
140 {
141 int nrVariables = sc->getNrProtectedVariables();
142 context.clear(nrVariables);
143 if (sc->getLhsAutomaton()->match(subject, context, sp, 0))
144 {
145 if (sp == 0 || sp->solve(true, context))
146 {
147 if (!(sc->hasCondition()) || sc->checkCondition(subject, context, sp))
148 {
149 delete sp;
150 if (RewritingContext::getTraceStatus())
151 {
152 context.tracePreScApplication(subject, sc);
153 if (context.traceAbort())
154 {
155 context.finished();
156 return;
157 }
158 }
159 context.incrementMbCount();
160 context.finished();
161 MemoryCell::okToCollectGarbage();
162 currentSortIndex = s->index();
163 subject->setSortIndex(currentSortIndex);
164 goto retry;
165 }
166 }
167 delete sp;
168 }
169 context.finished();
170 MemoryCell::okToCollectGarbage();
171 }
172 }
173 }
174