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 // Abstract base class for terms.
25 //
26 #ifndef _term_hh_
27 #define _term_hh_
28 #include "lineNumber.hh"
29 #include "sort.hh"
30 #include "symbol.hh"
31 #include "dagNode.hh"
32 #include "natSet.hh"
33 #include "pointerSet.hh"
34 #include "termSet.hh"
35 #include "variableSymbol.hh"
36
37 class Term : public LineNumber
38 {
39 NO_COPYING(Term);
40
41 static bool discard;
42
43 public:
44 enum ReturnValues
45 {
46 GREATER = 1,
47 LESS = -2,
48 EQUAL = 0,
49 UNKNOWN = -1
50 };
51
52 Term(Symbol* symbol);
~Term()53 virtual ~Term() {}
54 //
55 // These member functions should not be overridden
56 //
57 Symbol* symbol() const;
58 bool ground() const;
59 bool stable() const;
60 const NatSet& occursBelow() const;
61 const NatSet& occursInContext() const;
62 const PointerSet& collapseSymbols() const;
63 unsigned int getHashValue() const;
64 int computeSize();
65 Term* deepCopy(SymbolMap* translation = 0) const;
66 Term* instantiate(const Vector<Term*>& varBindings, SymbolMap* translation);
67 int compare(const Term* other) const;
68 int compare(const DagNode* other) const;
69 bool equal(const Term* other) const;
70 bool equal(const DagNode* other) const;
71 bool leq(const Sort* sort) const;
72 DagNode* term2Dag(bool setSortInfo = false);
73 DagNode* dagify();
74 void indexVariables(VariableInfo& indicies);
75 void addContextVariables(const NatSet& externalVariables);
76 void determineContextVariables();
77 void markEager(int nrVariables,
78 const NatSet& eagerVariables,
79 Vector<int>& problemVariables);
80 ConnectedComponent* getComponent() const;
81 int getSortIndex() const;
82 Sort* getSort() const;
83 void setSortInfo(ConnectedComponent* component, int index);
84 int getSaveIndex() const;
85 bool matchIndependent(const Term* other) const;
86 bool honorsGroundOutMatch() const;
87 void setHonorsGroundOutMatch(bool flag);
88 bool willGroundOutMatch(const NatSet& boundUniquely) const;
89 void analyseCollapses();
90 bool hasEagerContext() const;
91 bool greedySafe(const VariableInfo& variableInfo, const NatSet& boundUniquely) const;
92 LhsAutomaton* compileLhs(bool matchAtTop,
93 const VariableInfo& variableInfo,
94 NatSet& boundUniquely,
95 bool& subproblemLikely);
96 int compileRhs(RhsBuilder& rhsBuilder,
97 VariableInfo& variableInfo,
98 TermBag& availableTerms,
99 bool eagerContext);
100 void compileTopRhs(RhsBuilder& rhsBuilder,
101 VariableInfo& variableInfo,
102 TermBag& availableTerms);
103 //
104 // These member functions must be defined for each derived class
105 //
106 virtual RawArgumentIterator* arguments() = 0;
107 virtual void deepSelfDestruct() = 0;
108 virtual Term* deepCopy2(SymbolMap* translator) const = 0;
109 virtual Term* normalize(bool full, bool& changed = discard) = 0;
110 virtual int compareArguments(const Term* other) const = 0;
111 virtual int compareArguments(const DagNode* other) const = 0;
112 virtual void findAvailableTerms(TermBag& availableTerms,
113 bool eagerContext,
114 bool atTop = false) = 0;
115 virtual void findEagerVariables(bool atTop, NatSet& eagerVariables) const = 0;
116 virtual void analyseConstraintPropagation(NatSet& boundUniquely) const = 0;
117 virtual LhsAutomaton* compileLhs2(bool matchAtTop,
118 const VariableInfo& variableInfo,
119 NatSet& boundUniquely,
120 bool& subproblemLikely) = 0;
121 virtual void markEagerArguments(int nrVariables,
122 const NatSet& eagerVariables,
123 Vector<int>& problemVariables) = 0;
124 virtual int compileRhs2(RhsBuilder& rhsBuilder,
125 VariableInfo& variableInfo,
126 TermBag& availableTerms,
127 bool eagerContext) = 0;
128 virtual DagNode* dagify2() = 0;
129 //
130 // The following function returns true if the lhs automaton for "this"
131 // is guarenteed to return "false" on any instance of "other" when running
132 // without extension and an empty substitution. It is used to optimize the
133 // compilation of patterns and can be defined conservatively --- returning
134 // false is always OK.
135 //
136 virtual bool earlyMatchFailOnInstanceOf(const Term* other) const;
137 //
138 // These member functions compute approximate relations between terms;
139 // i.e. they can return UNDECIDED whenever the true relation is too
140 // expensive to evaluate (or even undecidable). The default versions
141 // return UNDECIDED most of the time. Theory specific versions may be able
142 // to do better but must be prepared to handle UNDECIDED results from
143 // alien subterms. These functions are intended for use in optimizing
144 // lhs and rhs automata; if a result is UNDECIDED the optimization is quietly
145 // forgotten.
146 //
147 // The following function returns true if any subject that matches "other"
148 // is guarenteed to match "this" taking into account nonlinear variables
149 // in the context. It can be defined conservatively --- returning
150 // false is always OK. The sameVariableSet flag indicates whether
151 // variables in this are the same as (and thus trivially subsume) variables
152 // with the same name in "other". When both subterms are from the same
153 // pattern it should be set to true; when they are from different patterns
154 // it should be set to false since f(X, Y) does not subsume f(a, Y) if
155 // Y is already bound in the context of f(X, Y).
156 //
157 virtual bool subsumes(const Term* other, bool sameVariableSet) const;
158 //
159 // This pair of functions does the preprocessing needed to handle collapse
160 // theories correctly. analyseCollapses2() computes the set of symbols that
161 // could be the top symbol of the term following collapses caused by bindings
162 // to its variables. The default version will work for symbols with
163 // collapse-free theories. insertAbstractionVariables() inserts abstraction
164 // variables where needed to help out the matching algorithm by replacing
165 // tricky subpatterns with variables, whose binding will be matched against
166 // the subpattern at solve time. The default version will work for symbols
167 // whose matching algorithm does not need abstraction variables.
168 //
169 virtual void analyseCollapses2();
170 virtual void insertAbstractionVariables(VariableInfo& variableInfo);
171 //
172 // Runtime heuristic partial camparison between a term with variables
173 // and a dag, with a substitution that may bind some of the variables.
174 //
175 int partialCompare(const Substitution& partialSubstitution,
176 DagNode* other) const;
177 virtual int partialCompareUnstable(const Substitution& partialSubstitution,
178 DagNode* other) const;
179 virtual int partialCompareArguments(const Substitution& partialSubstitution,
180 DagNode* other) const;
181 //
182 // The following function should be redefined for any subclass that needs a
183 // non-naive treatment of it's arguments or has hidden data.
184 //
185 virtual Term* instantiate2(const Vector<Term*>& varBindings, SymbolMap* translator);
186
187 //
188 // The following function should be redefined for any theory that uses
189 // index based matching.
190 //
191 virtual void computeMatchIndices() const;
192
193 //
194 // Functionality for the stack based rewrite engine.
195 //
196 Instruction* term2InstructionSequence();
197 int recordSubterms(StackMachineRhsCompiler& compiler, TermSet& visited);
198 virtual int recordSubterms2(StackMachineRhsCompiler& compiler, TermSet& visited);
199
200 #ifdef COMPILER
201 void generateRhs(CompilationContext& context,
202 int indentLevel,
203 const Vector<VariableName>& varNames,
204 Symbol* lhsSymbol);
205 int gatherPartialResults(int nrVariables,
206 TermSet& compiled,
207 Vector<Symbol*>& symbols,
208 Vector<Vector<int> >& argLists);
209 #endif
210
211 #ifdef DUMP
212 //
213 // dump() routine is optional; Default will dump common stuff togther with args
214 // in naive way. Replacement routine should call dumpCommon() to dump stuff in
215 // base class.
216 //
217 virtual void dump(ostream& s, const VariableInfo& variableInfo, int indentLevel = 0);
218 void dumpCommon(ostream& s, const VariableInfo& variableInfo, int indentLevel);
219
220 private:
221 static void dumpVariableSet(ostream& s,
222 const NatSet& variableSet,
223 const VariableInfo& variableInfo);
224 static void dumpSymbolSet(ostream& s, const PointerSet& symbolSet);
225
226 #endif
227
228 protected:
229 static unsigned int hash(unsigned int v1, unsigned int v2);
230 static unsigned int hash(unsigned int v1, unsigned int v2, unsigned int v3);
231 static void commonSymbols(Vector<Term*>& terms, PointerSet& common);
232 void addCollapseSymbol(Symbol* symbol);
233 void addCollapseSymbols(const PointerSet& symbols);
234 void setHashValue(unsigned int value);
235 void setSaveIndex(int index);
236
237 private:
238 enum Flags
239 {
240 //
241 // A subterm is stable if its top symbol cannot change under instantiation.
242 //
243 STABLE = 1,
244 //
245 // A subterm is in an eager context if the path to its root contains only
246 // eagerly evaluated positions.
247 //
248 EAGER_CONTEXT = 2,
249 //
250 // A subterm "honors ground out match" if its matching algorithm guarantees
251 // never to to return a matching subproblem when all the terms variables
252 // are already bound.
253 //
254 HONORS_GROUND_OUT_MATCH = 4
255 };
256
257 static bool commonWithOtherPatterns(Vector<Term*>& patterns, int excluded, Symbol* symbol);
258 static bool hasGeqOrIncomparableVariable(Term* pattern, VariableSymbol* v);
259
260 static Vector<DagNode*> subDags;
261 static TermSet converted;
262 static bool setSortInfoFlag;
263
264 Symbol* topSymbol;
265 NatSet occursSet;
266 NatSet contextSet;
267 PointerSet collapseSet;
268 Ubyte flags;
269 short sortIndex;
270 ConnectedComponent* connectedComponent;
271 int saveIndex;
272 unsigned int hashValue;
273 int cachedSize;
274 };
275
276 inline
Term(Symbol * symbol)277 Term::Term(Symbol* symbol)
278 {
279 topSymbol = symbol;
280 flags = 0;
281 sortIndex = Sort::SORT_UNKNOWN;
282 saveIndex = NONE;
283 cachedSize = UNDEFINED;
284 }
285
286 inline Symbol*
symbol() const287 Term::symbol() const
288 {
289 return topSymbol;
290 }
291
292 inline bool
ground() const293 Term::ground() const
294 {
295 return occursSet.empty();
296 }
297
298 inline bool
stable() const299 Term::stable() const
300 {
301 return flags & STABLE;
302 }
303
304 inline const NatSet&
occursBelow() const305 Term::occursBelow() const
306 {
307 return occursSet;
308 }
309
310 inline const NatSet&
occursInContext() const311 Term::occursInContext() const
312 {
313 return contextSet;
314 }
315
316 inline const PointerSet&
collapseSymbols() const317 Term::collapseSymbols() const
318 {
319 return collapseSet;
320 }
321
322 inline Term*
deepCopy(SymbolMap * translator) const323 Term::deepCopy(SymbolMap* translator) const
324 {
325 Term* t = deepCopy2(translator);
326 t->setLineNumber(getLineNumber());
327 return t;
328 }
329
330 inline Term*
instantiate(const Vector<Term * > & varBindings,SymbolMap * translator)331 Term::instantiate(const Vector<Term*>& varBindings, SymbolMap* translator)
332 {
333 Term* t = instantiate2(varBindings, translator);
334 t->setLineNumber(getLineNumber());
335 return t;
336 }
337
338 inline int
compare(const Term * other) const339 Term::compare(const Term* other) const
340 {
341 Symbol* s = other->topSymbol;
342 return (topSymbol == s) ? compareArguments(other) : topSymbol->compare(s);
343 }
344
345 inline int
compare(const DagNode * other) const346 Term::compare(const DagNode* other) const
347 {
348 Symbol* s = other->symbol();
349 return (topSymbol == s) ? compareArguments(other) : topSymbol->compare(s);
350 }
351
352 inline int // inline this because it is heavily used at runtime
partialCompare(const Substitution & partialSubstitution,DagNode * other) const353 Term::partialCompare(const Substitution& partialSubstitution,
354 DagNode* other) const
355 {
356 if (!stable())
357 return partialCompareUnstable(partialSubstitution, other);
358 Symbol* s = other->symbol();
359 if (topSymbol == s)
360 return partialCompareArguments(partialSubstitution, other);
361 return (topSymbol->compare(s) < 0) ? LESS : GREATER;
362 }
363
364 inline bool
equal(const Term * other) const365 Term::equal(const Term* other) const
366 {
367 return topSymbol == other->topSymbol && compareArguments(other) == 0;
368 }
369
370 inline bool
equal(const DagNode * other) const371 Term::equal(const DagNode* other) const
372 {
373 return topSymbol == other->symbol() && compareArguments(other) == 0;
374 }
375
376 inline DagNode*
dagify()377 Term::dagify()
378 {
379 Assert(subDags.length() == converted.cardinality(),
380 "length/cardinality mismatch");
381 int e = converted.term2Index(this);
382 if (e >= 0)
383 return subDags[e];
384 DagNode* d = dagify2();
385 if (setSortInfoFlag)
386 {
387 Assert(sortIndex != Sort::SORT_UNKNOWN, "missing sort info");
388 d->setSortIndex(sortIndex);
389 d->setReduced();
390 }
391 converted.insert(this);
392 subDags.append(d);
393 return d;
394 }
395
396 inline int
recordSubterms(StackMachineRhsCompiler & compiler,TermSet & visited)397 Term::recordSubterms(StackMachineRhsCompiler& compiler, TermSet& visited)
398 {
399 int slotIndex = visited.term2Index(this);
400 return (slotIndex >= 0) ? slotIndex : recordSubterms2(compiler, visited);
401 }
402
403 inline void
markEager(int nrVariables,const NatSet & eagerVariables,Vector<int> & problemVariables)404 Term::markEager(int nrVariables,
405 const NatSet& eagerVariables,
406 Vector<int>& problemVariables)
407 {
408 flags |= EAGER_CONTEXT;
409 markEagerArguments(nrVariables, eagerVariables, problemVariables);
410 }
411
412 inline ConnectedComponent*
getComponent() const413 Term::getComponent() const
414 {
415 return connectedComponent;
416 }
417
418 inline int
getSortIndex() const419 Term::getSortIndex() const
420 {
421 return sortIndex;
422 }
423 inline Sort*
getSort() const424 Term::getSort() const
425 {
426 return (sortIndex == Sort::SORT_UNKNOWN) ? 0 : connectedComponent->sort(sortIndex);
427 }
428
429 inline int
getSaveIndex() const430 Term::getSaveIndex() const
431 {
432 return saveIndex;
433 }
434
435 inline void
setSaveIndex(int index)436 Term::setSaveIndex(int index)
437 {
438 saveIndex = index;
439 }
440
441 inline void
setSortInfo(ConnectedComponent * component,int index)442 Term::setSortInfo(ConnectedComponent* component, int index)
443 {
444 connectedComponent = component;
445 sortIndex = index;
446 }
447
448 inline bool
matchIndependent(const Term * other) const449 Term::matchIndependent(const Term* other) const
450 {
451 return earlyMatchFailOnInstanceOf(other) && other->earlyMatchFailOnInstanceOf(this);
452 }
453
454 inline void
addCollapseSymbol(Symbol * symbol)455 Term::addCollapseSymbol(Symbol* symbol)
456 {
457 (void) collapseSet.insert(symbol);
458 }
459
460 inline void
addCollapseSymbols(const PointerSet & symbols)461 Term::addCollapseSymbols(const PointerSet& symbols)
462 {
463 collapseSet.insert(symbols);
464 }
465
466 inline unsigned int
getHashValue() const467 Term::getHashValue() const
468 {
469 return hashValue;
470 }
471
472 inline unsigned int
hash(unsigned int v1,unsigned int v2)473 Term::hash(unsigned int v1, unsigned int v2)
474 {
475 return (v1 * v1) ^ (v1 >> 16) ^ v2; // symmetry with DagNode version
476 }
477
478 inline unsigned int
hash(unsigned int v1,unsigned int v2,unsigned int v3)479 Term::hash(unsigned int v1, unsigned int v2, unsigned int v3)
480 {
481 return (v1 * v1) ^ (v1 >> 16) ^ (v2 * v3); // symmetry with DagNode version
482 }
483
484 inline void
setHashValue(unsigned int value)485 Term::setHashValue(unsigned int value)
486 {
487 hashValue = value;
488 }
489
490 inline bool
honorsGroundOutMatch() const491 Term::honorsGroundOutMatch() const
492 {
493 return flags & HONORS_GROUND_OUT_MATCH;
494 }
495
496 inline void
setHonorsGroundOutMatch(bool flag)497 Term::setHonorsGroundOutMatch(bool flag)
498 {
499 if (flag) // HACK should probably start clear and set as needed
500 flags |= HONORS_GROUND_OUT_MATCH;
501 else
502 flags &= ~HONORS_GROUND_OUT_MATCH;
503 }
504
505 inline bool
willGroundOutMatch(const NatSet & boundUniquely) const506 Term::willGroundOutMatch(const NatSet& boundUniquely) const
507 {
508 return honorsGroundOutMatch() && boundUniquely.contains(occursSet);
509 }
510
511 inline bool
hasEagerContext() const512 Term::hasEagerContext() const
513 {
514 return flags & EAGER_CONTEXT;
515 }
516
517 inline bool
leq(const Sort * sort) const518 Term::leq(const Sort* sort) const
519 {
520 return ::leq(sortIndex, sort);
521 }
522
523 inline void
addContextVariables(const NatSet & externalVariables)524 Term::addContextVariables(const NatSet& externalVariables)
525 {
526 contextSet.insert(externalVariables);
527 }
528
529 //
530 // Output function for Term must be defined by library user
531 //
532 ostream& operator<<(ostream& s, const Term* term);
533
534 #endif
535