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 BinarySymbol.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30 #include "pointerSet.hh"
31
32 // forward declarations
33 #include "interface.hh"
34 #include "core.hh"
35 #include "variable.hh"
36
37 // interface class definitions
38 #include "binarySymbol.hh"
39 #include "dagNode.hh"
40 #include "term.hh"
41
42 // core class definitions
43 #include "sortConstraint.hh"
44 #include "argumentIterator.hh"
45
46 // variable class definitions
47 #include "variableSymbol.hh"
48
BinarySymbol(int id,bool memoFlag,Term * identity)49 BinarySymbol::BinarySymbol(int id, bool memoFlag, Term* identity)
50 : Symbol(id, 2, memoFlag),
51 identityTerm(identity)
52 {
53 cyclicIdentity = (identity == 0) ? 0 : UNDECIDED;
54 }
55
56 bool
interSymbolPass()57 BinarySymbol::interSymbolPass()
58 {
59 return identityTerm.getTerm() == 0 ? false : identityTerm.normalize();
60 }
61
62 void
reset()63 BinarySymbol::reset()
64 {
65 identityTerm.reset(); // so identity dag can be garbage collected
66 Symbol::reset(); // default reset() tasks
67 }
68
69 void
setPermuteStrategy(const Vector<int> & userStrategy)70 BinarySymbol::setPermuteStrategy(const Vector<int>& userStrategy)
71 {
72 int stratLen = userStrategy.length();
73 if (stratLen == 0)
74 {
75 permuteStrategy = EAGER;
76 setStrategy(userStrategy, 2, isMemoized());
77 return;
78 }
79 permuteStrategy = LAZY;
80 Vector<int> modifiedStrategy;
81 bool seenZero = false;
82 for (int i = 0; i < stratLen; i++)
83 {
84 int a = userStrategy[i];
85 if (a == 0)
86 seenZero = true;
87 else
88 {
89 if (seenZero)
90 {
91 permuteStrategy = SEMI_EAGER;
92 modifiedStrategy.append(0);
93 }
94 else
95 permuteStrategy = EAGER;
96 modifiedStrategy.append(1);
97 modifiedStrategy.append(2);
98 break;
99 }
100 }
101 modifiedStrategy.append(0);
102 setStrategy(modifiedStrategy, 2, isMemoized());
103 }
104
105 void
setPermuteFrozen(const NatSet & frozen)106 BinarySymbol::setPermuteFrozen(const NatSet& frozen)
107 {
108 //
109 // Must freeze both arguments or neither for permutative operator.
110 //
111 if (frozen.contains(0) == frozen.contains(1))
112 Symbol::setFrozen(frozen);
113 else
114 {
115 NatSet newFrozen;
116 newFrozen.insert(0);
117 newFrozen.insert(1);
118 Symbol::setFrozen(newFrozen);
119 }
120 }
121
122 bool
isStable() const123 BinarySymbol::isStable() const
124 {
125 return identityTerm.getTerm() == 0;
126 }
127
128 void
commutativeSortCompletion()129 BinarySymbol::commutativeSortCompletion()
130 {
131 Assert(domainComponent(0) == domainComponent(1),
132 "Commutative operator " << this <<
133 " has its arguments in different sort components");
134 Vector<Sort*> newDecl(3);
135 const Vector<OpDeclaration>& opDecls = getOpDeclarations();
136 int nrOpDecls = opDecls.length();
137 for (int i = 0; i < nrOpDecls; i++)
138 {
139 const Vector<Sort*>& iDecl = opDecls[i].getDomainAndRange();
140 bool iCtor = opDecls[i].isConstructor();
141 for (int j = opDecls.length() - 1; j >= 0; j--)
142 {
143 const Vector<Sort*>& jDecl = opDecls[j].getDomainAndRange();
144 if (iDecl[0] == jDecl[1] &&
145 iDecl[1] == jDecl[0] &&
146 iDecl[2] == jDecl[2] &&
147 (!iCtor || opDecls[j].isConstructor()))
148 goto nextOpDecl;
149 }
150 newDecl[0] = iDecl[1];
151 newDecl[1] = iDecl[0];
152 newDecl[2] = iDecl[2];
153 addOpDeclaration(newDecl, iCtor);
154 nextOpDecl:
155 ;
156 }
157 }
158
159 void
processIdentity()160 BinarySymbol::processIdentity()
161 {
162 Term* id = identityTerm.getTerm();
163 if (id == 0)
164 return;
165
166 VariableInfo vi;
167 id->indexVariables(vi);
168 WarningCheck(id->occursBelow().empty(),
169 *id << ": identity element " << QUOTE(id) <<
170 " for operator " << QUOTE(this) << " contains variables.");
171 id->symbol()->fillInSortInfo(id);
172 int index = id->getSortIndex(); // is this valid?
173 Assert(index != Sort::SORT_UNKNOWN, "unknown sort for identity element");
174 WarningCheck(index != Sort::ERROR_SORT,
175 *id << ": identity element " << QUOTE(id) <<
176 " for operator " << QUOTE(this) << " has error sort.");
177 identityTerm.prepare();
178 }
179
180 bool
mightMatchOurIdentity(const Term * subterm) const181 BinarySymbol::mightMatchOurIdentity(const Term* subterm) const
182 {
183 Term* id = identityTerm.getTerm();
184 if (id == 0)
185 return false;
186 if (id->equal(subterm))
187 return true; // this can happen if we only have left (right) identity
188 Symbol* idTopSymbol = id->symbol();
189 //
190 // First examine subterm.
191 //
192 Symbol* s = subterm->symbol();
193 if (s == idTopSymbol && !(subterm->ground()))
194 return true;
195 VariableSymbol* vs = dynamic_cast<VariableSymbol*>(s);
196 if (vs != 0 && id->leq(vs->getSort()))
197 return true;
198 //
199 // Second examine what it might collapse to.
200 //
201 const PointerSet& cs = subterm->collapseSymbols();
202 int nrSymbols = cs.cardinality();
203 for (int i = 0; i < nrSymbols; i++)
204 {
205 Symbol* s2 = static_cast<Symbol*>(cs.index2Pointer(i));
206 if (s2 == idTopSymbol)
207 return true;
208 VariableSymbol* vs2 = dynamic_cast<VariableSymbol*>(s2);
209 if (vs2 != 0 && id->leq(vs2->getSort()))
210 return true;
211 }
212 return false;
213 }
214
215 void
leftIdentitySortCheck()216 BinarySymbol::leftIdentitySortCheck()
217 {
218 Term* id = identityTerm.getTerm();
219 const ConnectedComponent* component = rangeComponent();
220 Assert(component == domainComponent(1),
221 "operator with left identity " << this <<
222 " has right argument and range in different sort components");
223 Assert(id->getComponent() == domainComponent(0),
224 "operator " << this <<
225 " has left identity and left argument is different sort components");
226 int nrSorts = component->nrSorts();
227 //
228 // Check that all collapses are to less or equal sorts.
229 //
230 int step = traverse(0, id->getSortIndex());
231 for (int i = 1; i < nrSorts; i++)
232 {
233 const Sort* resultSort = component->sort(traverse(step, i));
234 unequalLeftIdCollapse = (resultSort->index() != i);
235 WarningCheck(leq(i, resultSort),
236 "sort declarations for operator " << QUOTE(this) <<
237 " with left identity " << QUOTE(id) <<
238 " can cause collapse from sort " << QUOTE(resultSort) <<
239 " to " << QUOTE(component->sort(i)) <<
240 " (collapsing to a larger or incomparable sort is illegal).");
241 }
242 }
243
244 void
rightIdentitySortCheck()245 BinarySymbol::rightIdentitySortCheck()
246 {
247 Term* id = identityTerm.getTerm();
248 const ConnectedComponent* component = rangeComponent();
249 Assert(component == domainComponent(0),
250 "operator with right identity " << this <<
251 " has left argument and range in different sort components");
252 Assert(id->getComponent() == domainComponent(1),
253 "operator " << this <<
254 " has right identity and right argument is different sort components");
255 int nrSorts = component->nrSorts();
256 //
257 // Check all collapses are to less or equal sorts.
258 //
259 int idIndex = id->getSortIndex();
260 for (int i = 1; i < nrSorts; i++)
261 {
262 const Sort* resultSort = component->sort(traverse(traverse(0, i), idIndex));
263 unequalRightIdCollapse = (resultSort->index() != i);
264 WarningCheck(leq(i, resultSort),
265 "sort declarations for operator " << QUOTE(this) <<
266 " with right identity " << QUOTE(id) <<
267 " can cause collapse from sort " << QUOTE(resultSort) <<
268 " to sort " << QUOTE(component->sort(i)) <<
269 " (collapsing to a larger or incomparable sort is illegal).");
270 }
271 }
272
273 void
idempotentSortCheck()274 BinarySymbol::idempotentSortCheck()
275 {
276 const ConnectedComponent* component = rangeComponent();
277 Assert(domainComponent(0) == component && domainComponent(1) == component,
278 "Idempotent operator " << this <<
279 " has a domain sort in a different connected component from its range sort");
280 int nrSorts = component->nrSorts();
281 for (int i = 1; i < nrSorts; i++)
282 {
283 const Sort* resultSort = component->sort(traverse(traverse(0, i), i));
284 WarningCheck(leq(i, resultSort),
285 "sort declarations for idempotent operator " << QUOTE(this) <<
286 " can cause collapse from sort " << QUOTE(resultSort) <<
287 " to sort " << QUOTE(component->sort(i)) <<
288 " (collapsing to a larger or incomparable sort is illegal).");
289 }
290 }
291
292 bool
lookForCycle(Term * term,NatSet & examinedIds) const293 BinarySymbol::lookForCycle(Term* term, NatSet& examinedIds) const
294 {
295 DebugAdvisory("BinarySymbol::lookForCycle() looking at " << term);
296 //
297 // Check if we've cycled back.
298 //
299 Symbol* s = term->symbol();
300 if (s == this)
301 return true;
302
303 //
304 // If we've reached symbol which has an identity we haven't explored, see
305 // if we can reach a cycle through it.
306 //
307 if (BinarySymbol* bs = dynamic_cast<BinarySymbol*>(s))
308 {
309 if (Term* id = bs->getIdentity())
310 {
311 int index = bs->getIndexWithinModule();
312 if (!examinedIds.contains(index))
313 {
314 examinedIds.insert(index);
315 if (lookForCycle(id, examinedIds))
316 return true;
317 }
318 }
319 }
320 //
321 // Finally explore the arguments.
322 //
323 for (ArgumentIterator a(*term); a.valid(); a.next())
324 {
325 if (lookForCycle(a.argument(), examinedIds))
326 return true;
327 }
328 return false;
329 }
330