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 class ACU_LhsAutomaton.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "indent.hh"
30 #include "vector.hh"
31
32 // forward declarations
33 #include "interface.hh"
34 #include "core.hh"
35 #include "ACU_Persistent.hh"
36 #include "ACU_Theory.hh"
37
38 // interface class definitions
39 #include "argVec.hh"
40 #include "associativeSymbol.hh"
41 #include "dagNode.hh"
42 #include "term.hh"
43 #include "subproblem.hh"
44 #include "lhsAutomaton.hh"
45 #include "rhsAutomaton.hh"
46
47 // core class definitions
48 #include "variableInfo.hh"
49 #include "subproblemSequence.hh"
50 #include "subproblemDisjunction.hh"
51 #include "subproblemAccumulator.hh"
52 #include "disjunctiveSubproblemAccumulator.hh"
53 #include "substitution.hh"
54 #include "localBinding.hh"
55 #include "variableAbstractionSubproblem.hh"
56 #include "equalitySubproblem.hh"
57
58 // variable class definitions
59 #include "variableSymbol.hh"
60 #include "variableTerm.hh"
61
62 // ACU Red-Black class definitions
63 #include "ACU_SlowIter.hh"
64
65 // ACU theory class definitions
66 #include "ACU_Symbol.hh"
67 #include "ACU_DagNode.hh"
68 #include "ACU_TreeDagNode.hh"
69 #include "ACU_LhsAutomaton.hh"
70 #include "ACU_Subproblem.hh"
71 #include "ACU_LazySubproblem.hh"
72 #include "ACU_ExtensionInfo.hh"
73
74 // our stuff
75 #include "ACU_TreeMatcher.cc"
76 #include "ACU_CollapseMatcher.cc"
77 #include "ACU_Matcher.cc"
78 #include "ACU_GreedyMatcher.cc"
79
ACU_LhsAutomaton(ACU_Symbol * symbol,bool matchAtTop,bool collapsePossible,int nrVariables)80 ACU_LhsAutomaton::ACU_LhsAutomaton(ACU_Symbol* symbol,
81 bool matchAtTop,
82 bool collapsePossible,
83 int nrVariables)
84 : topSymbol(symbol),
85 matchAtTop(matchAtTop),
86 collapsePossible(collapsePossible),
87 local(nrVariables),
88 scratch(nrVariables)
89 {
90 totalLowerBound = 0;
91 totalUpperBound = matchAtTop ? UNBOUNDED : 0;
92 maxPatternMultiplicity = 0;
93 totalNonGroundAliensMultiplicity = 0;
94 uniqueCollapseAutomaton = 0;
95 treeMatchOK = true;
96 collectorSeen = matchAtTop;
97 nrExpectedUnboundVariables = 0;
98 }
99
~ACU_LhsAutomaton()100 ACU_LhsAutomaton::~ACU_LhsAutomaton()
101 {
102 delete uniqueCollapseAutomaton;
103 int nrTopVariables = topVariables.length();
104 for (int i = 0; i < nrTopVariables; i++)
105 delete topVariables[i].abstracted;
106 int nrGroundedOutAliens = groundedOutAliens.length();
107 for (int i = 0; i < nrGroundedOutAliens; i++)
108 delete groundedOutAliens[i].automaton;
109 int nrGroundAliens = nonGroundAliens.length();
110 for (int i = 0; i < nrGroundAliens; i++)
111 delete nonGroundAliens[i].automaton;
112 }
113
114 void
updateTotals(int min,int max)115 ACU_LhsAutomaton::updateTotals(int min, int max)
116 {
117 totalLowerBound += min;
118 if (min > maxPatternMultiplicity)
119 maxPatternMultiplicity = min;
120 if (totalUpperBound != UNBOUNDED && max != UNBOUNDED)
121 totalUpperBound += max;
122 else
123 totalUpperBound = UNBOUNDED;
124 }
125
126 void
addTopVariable(const VariableTerm * variable,int multiplicity,bool willBeBound)127 ACU_LhsAutomaton::addTopVariable(const VariableTerm* variable,
128 int multiplicity,
129 bool willBeBound)
130 {
131 Sort* s = variable->getSort();
132 int bound = topSymbol->sortBound(s);
133 collectorSeen = collectorSeen ||
134 (!willBeBound && bound == UNBOUNDED && multiplicity == 1);
135 if (!willBeBound)
136 ++nrExpectedUnboundVariables;
137 bool takeIdentity = topSymbol->takeIdentity(s);
138 int nrTopVariables = topVariables.length();
139 topVariables.expandBy(1);
140 TopVariable& tv = topVariables[nrTopVariables];
141 tv.index = variable->getIndex();
142 tv.multiplicity = multiplicity;
143 tv.sort = s;
144 tv.upperBound = bound;
145 tv.structure = topSymbol->sortStructure(s);
146 tv.takeIdentity = takeIdentity;
147 tv.abstracted = 0;
148 updateTotals(takeIdentity ? 0 : multiplicity,
149 (bound == UNBOUNDED) ? UNBOUNDED : (bound * multiplicity));
150 }
151
152 void
addAbstractionVariable(int index,Sort * sort,int upperBound,bool takeIdentity,LhsAutomaton * abstracted,int multiplicity)153 ACU_LhsAutomaton::addAbstractionVariable(int index,
154 Sort* sort,
155 int upperBound,
156 bool takeIdentity,
157 LhsAutomaton* abstracted,
158 int multiplicity)
159 {
160 int nrTopVariables = topVariables.length();
161 topVariables.expandBy(1);
162 TopVariable& tv = topVariables[nrTopVariables];
163 tv.index = index;
164 tv.multiplicity = multiplicity;
165 tv.sort = sort;
166 tv.upperBound = upperBound;
167 tv.structure = AssociativeSymbol::UNSTRUCTURED;
168 tv.takeIdentity = takeIdentity;
169 tv.abstracted = abstracted;
170 updateTotals(takeIdentity ? 0 : multiplicity,
171 (upperBound == UNBOUNDED) ? UNBOUNDED : (upperBound * multiplicity));
172 treeMatchOK = false;
173 }
174
175 void
addGroundAlien(Term * alien,int multiplicity)176 ACU_LhsAutomaton::addGroundAlien(Term* alien, int multiplicity)
177 {
178 updateTotals(multiplicity, multiplicity);
179 int nrGroundAliens = groundAliens.length();
180 groundAliens.expandBy(1);
181 groundAliens[nrGroundAliens].term = alien;
182 groundAliens[nrGroundAliens].multiplicity = multiplicity;
183 }
184
185 void
addGroundedOutAlien(Term * alien,LhsAutomaton * automaton,int multiplicity)186 ACU_LhsAutomaton::addGroundedOutAlien(Term* alien, LhsAutomaton* automaton, int multiplicity)
187 {
188 updateTotals(multiplicity, multiplicity);
189 int nrGroundedOutAliens = groundedOutAliens.length();
190 groundedOutAliens.expandBy(1);
191 groundedOutAliens[nrGroundedOutAliens].term = alien->stable() ? alien : 0;
192 groundedOutAliens[nrGroundedOutAliens].automaton = automaton;
193 groundedOutAliens[nrGroundedOutAliens].multiplicity = multiplicity;
194 treeMatchOK = treeMatchOK && alien->stable();
195 }
196
197 void
addNonGroundAlien(Term * alien,LhsAutomaton * automaton,int multiplicity)198 ACU_LhsAutomaton::addNonGroundAlien(Term* alien, LhsAutomaton* automaton, int multiplicity)
199 {
200 updateTotals(multiplicity, multiplicity);
201 totalNonGroundAliensMultiplicity += multiplicity;
202 int nrNonGroundAliens = nonGroundAliens.length();
203 nonGroundAliens.expandBy(1);
204 nonGroundAliens[nrNonGroundAliens].term = alien->stable() ? alien : 0;
205 nonGroundAliens[nrNonGroundAliens].automaton = automaton;
206 nonGroundAliens[nrNonGroundAliens].multiplicity = multiplicity;
207 treeMatchOK = treeMatchOK && alien->stable();
208 }
209
210 local_inline bool
topVariableLt(const TopVariable & t1,const TopVariable & t2)211 ACU_LhsAutomaton::topVariableLt(const TopVariable& t1, const TopVariable& t2)
212 {
213 //
214 // Variables with high multiplicity go to the begining of the vector.
215 // Between variables of equal multiplicity, variables of high sort
216 // index (low sort) come first.
217 //
218 int r = t2.multiplicity - t1.multiplicity;
219 return (r != 0) ? (r < 0) : (t2.sort->index() < t1.sort->index());
220 }
221
222 void
complete(MatchStrategy strategy,int nrIndependent)223 ACU_LhsAutomaton::complete(MatchStrategy strategy,
224 int nrIndependent)
225 {
226 //
227 // For red-black greedy matching to be correct we require that
228 // (1) unbound top variables are quasi-linear and don't occur in the
229 // condition;
230 // (2) unbound variables in a nonground alien don't occur in other
231 // aliens, in our context or in the condition;
232 // (3) there are no abstraction variables;
233 // (4) all groundout aliens and nonground aliens are stable; and
234 // (5) - obsolete - (was SAT_MULT related)
235 //
236 // For red-black greedy matching to be a win we require that
237 // (6) subproblems must be unlikely; and
238 // (7) there is a unbound variable or extension that can take almost
239 // everything.
240 //
241 // (1) and (2) are satisfied if strategy is LONE_VARIABLE or GREEDY.
242 // (6) is satisfied if strategy is GREEDY or strategy is LONE_VARIABLE
243 // and (3) holds.
244 // treeMatchOK will have already been falsified if (3) or (4) fail to
245 // hold. (7) is recorded by the collectorSeen flag.
246 //
247 if (treeMatchOK)
248 {
249 if (strategy == LONE_VARIABLE || strategy == GREEDY)
250 treeMatchOK = collectorSeen;
251 else if (strategy == FULL)
252 {
253 //
254 // We now allow non-greedy tree matching if there is a single
255 // NGA with multiplicity 1, a single unbound variable with
256 // multiplicity 1 and no extension.
257 //
258 treeMatchOK = collectorSeen &&
259 !matchAtTop &&
260 nrExpectedUnboundVariables == 1 &&
261 nonGroundAliens.length() == 1 &&
262 nonGroundAliens[0].multiplicity == 1;
263 }
264 else
265 treeMatchOK = false;
266 }
267
268 matchStrategy = strategy;
269 Assert(nrIndependent <= nonGroundAliens.length(), "too many independent");
270 nrIndependentAliens = nrIndependent;
271 sort(topVariables.begin(), topVariables.end(), topVariableLt);
272 }
273
274 #ifdef DUMP
275 void
dump(ostream & s,const VariableInfo & variableInfo,int indentLevel)276 ACU_LhsAutomaton::dump(ostream& s, const VariableInfo& variableInfo, int indentLevel)
277 {
278 s << Indent(indentLevel) << "Begin{ACU_LhsAutomaton}\n";
279 ++indentLevel;
280 s << Indent(indentLevel) << "topSymbol = \"" << topSymbol <<
281 "\"\tmatchAtTop = " << static_cast<bool>(matchAtTop) <<
282 "\tcollapsePossible = " << static_cast<bool>(collapsePossible) << '\n';
283 s << Indent(indentLevel) << "treeMatchOK = " << static_cast<bool>(treeMatchOK) <<
284 "\tcollectorSeen = " << static_cast<bool>(collectorSeen) <<
285 "\tmatchStrategy = " << static_cast<MatchStrategy>(matchStrategy) << '\n';
286 if (uniqueCollapseAutomaton != 0)
287 {
288 s << Indent(indentLevel) << "uniqueCollapseAutomaton =\n";
289 uniqueCollapseAutomaton->dump(s, variableInfo, indentLevel + 1);
290 }
291 s << Indent(indentLevel) << "totalLowerBound = " << totalLowerBound <<
292 "\tmaxPatternMultiplicity = " << maxPatternMultiplicity <<
293 "\ttotalUpperBound = " << totalUpperBound << '\n';
294 s << Indent(indentLevel) <<
295 "totalNonGroundAliensMultiplicity = " << totalNonGroundAliensMultiplicity <<
296 "\tnrIndependentAliens = " << nrIndependentAliens << '\n';
297
298 s << Indent(indentLevel) << "topVariables:\n";
299 ++indentLevel;
300 for (int i = 0; i < topVariables.length(); i++)
301 {
302 TopVariable& tv = topVariables[i];
303 s << Indent(indentLevel) << "index = " << tv.index;
304 if (tv.abstracted == 0)
305 s << " \"" << variableInfo.index2Variable(tv.index) << '"';
306 s << "\tmultiplicity = " << tv.multiplicity <<
307 "\tsort = \"" << tv.sort <<
308 "\"\tupperBound = " << tv.upperBound <<
309 "\tstructure = " << tv.structure <<
310 "\ttakeIdentity = " << tv.takeIdentity << '\n';
311 if (tv.abstracted != 0)
312 {
313 s << Indent(indentLevel) << "abstracted = " << '\n';
314 tv.abstracted->dump(s, variableInfo, indentLevel + 1);
315 }
316 }
317
318 s << Indent(indentLevel - 1) << "groundAliens:\n";
319 for (int i = 0; i < groundAliens.length(); i++)
320 {
321 s << Indent(indentLevel) << "term = \"" << groundAliens[i].term <<
322 "\"\tmultiplicity = " << groundAliens[i].multiplicity << '\n';
323 }
324
325 s << Indent(indentLevel - 1) << "groundedOutAliens:\n";
326 for (int i = 0; i < groundedOutAliens.length(); i++)
327 {
328 s << Indent(indentLevel) << "multiplicity = " << groundedOutAliens[i].multiplicity <<
329 "\tautomaton =\n";
330 groundedOutAliens[i].automaton->dump(s, variableInfo, indentLevel + 1);
331 }
332
333 s << Indent(indentLevel - 1) << "nonGroundAliens:\n";
334 for (int i = 0; i < nonGroundAliens.length(); i++)
335 {
336 s << Indent(indentLevel) << "multiplicity = " << nonGroundAliens[i].multiplicity <<
337 "\tautomaton =\n";
338 nonGroundAliens[i].automaton->dump(s, variableInfo, indentLevel + 1);
339 }
340
341 s << Indent(indentLevel - 2) << "End{ACU_LhsAutomaton}\n";
342 }
343
344
operator <<(ostream & s,ACU_LhsAutomaton::MatchStrategy strategy)345 ostream& operator<<(ostream& s, ACU_LhsAutomaton::MatchStrategy strategy)
346 {
347 static const char* const names[] = {"GROUND_OUT",
348 "LONE_VARIABLE",
349 "ALIENS_ONLY",
350 "GREEDY",
351 "FULL"};
352 s << names[strategy];
353 return s;
354 }
355 #endif
356