1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2010 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 dag nodes.
25 //
26 #ifndef _dagNode_hh_
27 #define _dagNode_hh_
28 //#include "gmpxx.h"
29 #include "symbol.hh"
30 #include "redexPosition.hh"
31
32 class DagNode
33 {
34 NO_COPYING(DagNode);
35
36 public:
37 DagNode(Symbol* symbol, int sortIndex = Sort::SORT_UNKNOWN);
~DagNode()38 virtual ~DagNode() {}
39 void setCallDtor();
40 //
41 // Nasty cross casting stuff.
42 //
43 MemoryCell* getMemoryCell();
44 const MemoryCell* getMemoryCell() const;
45 //
46 // Static members (for memory management).
47 //
48 void* operator new(size_t size);
49 void* operator new(size_t size, DagNode* old);
50 void* operator new(size_t size, int);
51 //
52 // These member functions should not be overridden.
53 //
54 Symbol* symbol() const;
55 int compare(const DagNode* other) const;
56 bool equal(const DagNode* other) const;
57 bool leq(const Sort* sort) const;
58 bool fastLeq(const Sort* sort) const;
59
60 bool isReduced() const;
61 void reduce(RewritingContext& context);
62 void mark();
63 void setReduced();
64 void setUnrewritable();
65 bool isUnrewritable() const;
66 void setUnstackable();
67 bool isUnstackable() const;
68 void setGround();
69 bool isGround() const;
70 void setIrreducibleByVariantEquations();
71 bool isIrreducibleByVariantEquations() const;
72
73 void copySetRewritingFlags(const DagNode* other);
74 void copySortIndex(const DagNode* other);
75 void upgradeSortIndex(const DagNode* other);
76 Byte getTheoryByte() const;
77 void setTheoryByte(Byte value);
78
79 DagNode* copyReducible();
80 DagNode* copyEagerUptoReduced();
81 void clearCopyPointers();
82 DagNode* copyAndReduce(RewritingContext& context);
83 void setSortIndex(int index);
84 int getSortIndex() const;
85 Sort* getSort() const;
86 void computeTrueSort(RewritingContext& context);
87 void repudiateSortInfo();
88 bool checkSort(const Sort* boundSort, Subproblem*& returnedSubproblem);
89 bool checkSort(const Sort* boundSort, RewritingContext& context);
90 bool inErrorSort();
91 bool matchVariable(int index,
92 const Sort* sort,
93 bool copyToAvoidOverwriting,
94 Substitution& solution,
95 Subproblem*& returnedSubproblem,
96 ExtensionInfo* extensionInfo);
97 //
98 // Currently only used as an efficiency measure in changing the sorts
99 // of fresh variables introduced by unification.
100 //
101 void replaceSymbol(Symbol* newSymbol);
102 //
103 // These member functions must be defined for each derived class.
104 //
105 virtual RawDagArgumentIterator* arguments() = 0;
106 virtual size_t getHashValue() = 0;
107 virtual int compareArguments(const DagNode* other) const = 0;
108 virtual void overwriteWithClone(DagNode* old) = 0;
109 virtual DagNode* makeClone() = 0;
110 virtual DagNode* copyWithReplacement(int argIndex, DagNode* replacement) = 0;
111 virtual DagNode* copyWithReplacement(Vector<RedexPosition>& redexStack,
112 int first,
113 int last) = 0;
114 virtual void stackArguments(Vector<RedexPosition>& redexStack,
115 int parentIndex,
116 bool respectFrozen) = 0;
117 //
118 // Interface for unification.
119 //
120 enum ReturnResult
121 {
122 GROUND,
123 NONGROUND,
124 UNIMPLEMENTED
125 };
126
127 virtual ReturnResult computeBaseSortForGroundSubterms();
128 bool computeSolvedForm(DagNode* rhs, UnificationContext& solution, PendingUnificationStack& pending);
129 virtual bool computeSolvedForm2(DagNode* rhs, UnificationContext& solution, PendingUnificationStack& pending);
130
131 void insertVariables(NatSet& occurs);
insertVariables2(NatSet & occurs)132 virtual void insertVariables2(NatSet& occurs) {}
133 //
134 // instantiate() returns 0 if instantiation does not change term.
135 //
136 DagNode* instantiate(const Substitution& substitution);
instantiate2(const Substitution & substitution)137 virtual DagNode* instantiate2(const Substitution& substitution) { CantHappen("Not implemented"); return 0; }
138 //
139 // instantiateWithCopies() is similar but uses copies in eager positions.
140 //
141 DagNode* instantiateWithCopies(const Substitution& substitution, const Vector<DagNode*>& eagerCopies);
instantiateWithCopies2(const Substitution & substitution,const Vector<DagNode * > & eagerCopies)142 virtual DagNode* instantiateWithCopies2(const Substitution& substitution, const Vector<DagNode*>& eagerCopies)
143 { CantHappen("Not implemented"); return 0; }
144 void computeGeneralizedSort(const SortBdds& sortBdds,
145 const Vector<int>& realToBdd, // first BDD variable for each free real variable
146 Vector<Bdd>& generalizedSort);
147 void computeGeneralizedSort2(const SortBdds& sortBdds,
148 const Vector<int>& realToBdd, // first BDD variable for each free real variable
149 Vector<Bdd>& outputBdds);
150 //
151 // Interface for narrowing.
152 //
153 bool indexVariables(NarrowingVariableInfo& indices, int baseIndex);
154 virtual bool indexVariables2(NarrowingVariableInfo& indices, int baseIndex);
instantiateWithReplacement(const Substitution & substitution,const Vector<DagNode * > & eagerCopies,int argIndex,DagNode * newDag)155 virtual DagNode* instantiateWithReplacement(const Substitution& substitution, const Vector<DagNode*>& eagerCopies, int argIndex, DagNode* newDag)
156 { CantHappen("Not implemented"); return 0; }
157 //
158 // These member functions must be defined for each derived class in theories
159 // that need extension.
160 //
161 virtual bool matchVariableWithExtension(int index,
162 const Sort* sort,
163 Substitution& solution,
164 Subproblem*& returnedSubproblem,
165 ExtensionInfo* extensionInfo);
166 virtual void partialReplace(DagNode* replacement, ExtensionInfo* extensionInfo);
167 virtual DagNode* partialConstruct(DagNode* replacement, ExtensionInfo* extensionInfo);
168 virtual ExtensionInfo* makeExtensionInfo();
169 //
170 // Utility function for variant narrowing.
171 //
172 bool reducibleByVariantEquation(RewritingContext& context);
173
174 #ifdef DUMP
175 //
176 // dump() routine is optional; Default will dump common stuff togther with args
177 // in naive way. Replacement routine should call dumpCommon() to dump stuff in
178 // base class.
179 //
180 virtual void dump(ostream& s, int indentLevel = 0);
181 void dumpCommon(ostream& s, int indentLevel);
182 #endif
183
184 protected:
185 enum Sizes
186 {
187 //
188 // We use 2 of the available words in a memory cell; one for our
189 // symbol/copy pointer and one for our virtual function table pointer.
190 // It would be nice to do this in a cleaner way, rather than assume
191 // the existence/size of our virtual function table pointer.
192 //
193 nrWords = 3 // HACK
194 };
195
196 static size_t hash(size_t v1, size_t v2);
197 static size_t hash(size_t v1, size_t v2, size_t v3);
198 //
199 // Functions to set and test the status of the hash valid flag.
200 //
201 void setHashValid();
202 bool isHashValid() const;
203 //
204 // These member functions must be defined for each derived class.
205 //
206 virtual DagNode* markArguments() = 0;
207 virtual DagNode* copyEagerUptoReduced2() = 0;
208 virtual void clearCopyPointers2() = 0;
209
210 private:
211 enum Flags
212 {
213 REDUCED = 1, // reduced up to strategy by equations
214 COPIED = 2, // copied in current copy operation; copyPointer valid
215 UNREWRITABLE = 4, // reduced and not rewritable by rules
216 UNSTACKABLE = 8, // unrewritable and all subterms unstackable or frozen
217 //CACHED = 16, // node exists as part of a cache
218 GROUND_FLAG = 16, // no variables occur below this node
219 HASH_VALID = 32, // node has a valid hash value (storage is theory dependent)
220 //
221 // We can share a the same bit for this flag since the rule rewriting strategy that needs UNREWRITABLE will
222 // never be combined with variant narrowing.
223 //
224 IRREDUCIBLE_BY_VARIANT_EQUATIONS = 4
225 };
226
227 bool isCopied() const;
228 void setCopied();
229 void clearCopied();
230
231 union
232 {
233 //
234 // Since copy pointers are needed infrequently we will use the top symbol slot
235 // and restore the top symbol from the copy of the dag node when the entire
236 // copy operation in finished; this is slightly hairy but dag nodes are the
237 // fundemental runtime data structure and need to be highly optimized.
238 //
239 Symbol* topSymbol;
240 DagNode* copyPointer;
241 };
242 };
243
244 #define SAFE_INSTANTIATE(dagNode, eagerFlag, substitution, eagerCopies) \
245 if (DagNode* _t = (eagerFlag ? \
246 dagNode->instantiateWithCopies(substitution, eagerCopies) : \
247 dagNode->instantiate(substitution))) \
248 dagNode = _t
249
250 //
251 // Output function for DagNode must be defined by library user.
252 //
253 ostream& operator<<(ostream& s, DagNode* dagNode);
254
255 #include "memoryCell.hh"
256
257 inline MemoryCell*
getMemoryCell()258 DagNode::getMemoryCell()
259 {
260 return static_cast<MemoryCell*>(static_cast<void*>(this));
261 }
262
263 inline const MemoryCell*
getMemoryCell() const264 DagNode::getMemoryCell() const
265 {
266 return static_cast<const MemoryCell*>(static_cast<const void*>(this));
267 }
268
269 inline void
copySetRewritingFlags(const DagNode * other)270 DagNode::copySetRewritingFlags(const DagNode* other)
271 {
272 getMemoryCell()->copySetFlags(REDUCED | UNREWRITABLE | UNSTACKABLE | GROUND_FLAG,
273 other->getMemoryCell());
274 }
275
276 inline void
copySortIndex(const DagNode * other)277 DagNode::copySortIndex(const DagNode* other)
278 {
279 getMemoryCell()->setHalfWord(other->getMemoryCell()->getHalfWord());
280 }
281
282 inline void
upgradeSortIndex(const DagNode * other)283 DagNode::upgradeSortIndex(const DagNode* other)
284 {
285 //
286 // We set the sort to best of original and other sorts; that is:
287 // SORT_UNKNOWN, SORT_UNKNOWN -> SORT_UNKNOWN
288 // SORT_UNKNOWN, valid-sort -> valid-sort
289 // valid-sort, SORT_UNKNOWN -> valid-sort
290 // valid-sort, valid-sort -> valid-sort
291 //
292 // We can do it with a bitwise AND trick because valid sorts should
293 // always be in agreement and SORT_UNKNOWN is represented by -1, i.e.
294 // all 1 bits.
295 //
296 getMemoryCell()->setHalfWord(getMemoryCell()->getHalfWord() &
297 other->getMemoryCell()->getHalfWord());
298 }
299
300 inline void
setCallDtor()301 DagNode::setCallDtor()
302 {
303 getMemoryCell()->setCallDtor();
304 }
305
306 inline int
getSortIndex() const307 DagNode::getSortIndex() const
308 {
309 return getMemoryCell()->getHalfWord();
310 }
311
312 inline void
setSortIndex(int index)313 DagNode::setSortIndex(int index)
314 {
315 getMemoryCell()->setHalfWord(index);
316 }
317
318 inline void
replaceSymbol(Symbol * newSymbol)319 DagNode::replaceSymbol(Symbol* newSymbol)
320 {
321 topSymbol = newSymbol;
322 }
323
324 inline void
repudiateSortInfo()325 DagNode::repudiateSortInfo()
326 {
327 setSortIndex(Sort::SORT_UNKNOWN);
328 }
329
330 //#include "memoryCellNew.hh"
331
332 inline void*
operator new(size_t size)333 DagNode::operator new(size_t size)
334 {
335 //
336 // MemoryCell::allocateMemoryCell() no longer sets the half word to
337 // Sort::SORT_UNKNOWN. This reposibility is shifted to DagNode::DagNode()
338 // which can set it to other values as an optimization.
339 //
340 Assert(size <= sizeof(MemoryCell), "dag node too big");
341 MemoryCell* m = MemoryCell::allocateMemoryCell();
342 //
343 // We are obligated to clear the flags. We do this here rather than in
344 // MemoryCell::allocateMemoryCell() to allow the compiler to optimize any
345 // flag setting our caller might do.
346 //
347 m->clearAllFlags();
348 return m;
349 }
350
351
352 inline void*
operator new(size_t size,int)353 DagNode::operator new(size_t size, int)
354 {
355 //
356 // This is a specialized version of the above which creates the DagNode
357 // with its reduced flag already set, to save an instruction.
358 //
359 // The int parameter is a dummy to allow this version to be selected.
360 //
361 Assert(size <= sizeof(MemoryCell), "dag node too big");
362 MemoryCell* m = MemoryCell::allocateMemoryCell();
363 //
364 // We are obligated to clear the flags. We do this here rather than in
365 // MemoryCell::allocateMemoryCell() to allow the compiler to optimize any
366 // flag setting our caller might do.
367 //
368 m->initFlags(REDUCED);
369 return m;
370 }
371
372 inline void*
operator new(size_t,DagNode * old)373 DagNode::operator new(size_t /* size */, DagNode* old)
374 {
375 if (old->getMemoryCell()->needToCallDtor())
376 old->~DagNode(); // explicitly call virtual destructor
377 old->getMemoryCell()->clearAllExceptMarked();
378 // old->repudiateSortInfo(); // shouldn't be needed now that sort info setting has been shifted to DagNode::DagNode()
379 //DebugAdvisory("in place new called, old = " << (void*)(old));
380 //Assert(old->getSortIndex() == Sort::SORT_UNKNOWN, "bad sort init");
381 return static_cast<void*>(old);
382 }
383
384 inline
DagNode(Symbol * symbol,int sortIndex)385 DagNode::DagNode(Symbol* symbol, int sortIndex)
386 {
387 setSortIndex(sortIndex);
388 topSymbol = symbol;
389 //DebugAdvisory("created dag node for " << symbol << " at " << (void*)(this));
390 //DebugAdvisoryCheck(getSortIndex() == Sort::SORT_UNKNOWN,
391 // "bad sort in dagnode");
392 }
393
394 inline Symbol*
symbol() const395 DagNode::symbol() const
396 {
397 return topSymbol;
398 }
399
400 inline int
compare(const DagNode * other) const401 DagNode::compare(const DagNode* other) const
402 {
403 if (this == other)
404 return 0; // pointers to same shared node
405 Symbol* s = other->topSymbol;
406 return (topSymbol == s) ? compareArguments(other) : topSymbol->compare(s);
407 }
408
409 inline bool
equal(const DagNode * other) const410 DagNode::equal(const DagNode* other) const
411 {
412 return this == other || (topSymbol == other->topSymbol && compareArguments(other) == 0);
413 }
414
415 inline bool
isReduced() const416 DagNode::isReduced() const
417 {
418 return getMemoryCell()->getFlag(REDUCED);
419 }
420
421 inline void
setReduced()422 DagNode::setReduced()
423 {
424 getMemoryCell()->setFlag(REDUCED);
425 }
426
427 inline bool
isCopied() const428 DagNode::isCopied() const
429 {
430 return getMemoryCell()->getFlag(COPIED);
431 }
432
433 inline void
setCopied()434 DagNode::setCopied()
435 {
436 getMemoryCell()->setFlag(COPIED);
437 }
438
439 inline void
clearCopied()440 DagNode::clearCopied()
441 {
442 getMemoryCell()->clearFlag(COPIED);
443 }
444
445 inline void
setUnrewritable()446 DagNode::setUnrewritable()
447 {
448 getMemoryCell()->setFlag(UNREWRITABLE);
449 }
450
451 inline bool
isUnrewritable() const452 DagNode::isUnrewritable() const
453 {
454 return getMemoryCell()->getFlag(UNREWRITABLE);
455 }
456
457 inline void
setUnstackable()458 DagNode::setUnstackable()
459 {
460 getMemoryCell()->setFlag(UNSTACKABLE);
461 }
462
463 inline bool
isUnstackable() const464 DagNode::isUnstackable() const
465 {
466 return getMemoryCell()->getFlag(UNSTACKABLE);
467 }
468
469 inline void
setGround()470 DagNode::setGround()
471 {
472 getMemoryCell()->setFlag(GROUND_FLAG);
473 }
474
475 inline bool
isGround() const476 DagNode::isGround() const
477 {
478 return getMemoryCell()->getFlag(GROUND_FLAG);
479 }
480
481 inline void
setIrreducibleByVariantEquations()482 DagNode::setIrreducibleByVariantEquations()
483 {
484 getMemoryCell()->setFlag(IRREDUCIBLE_BY_VARIANT_EQUATIONS);
485 }
486
487 inline bool
isIrreducibleByVariantEquations() const488 DagNode::isIrreducibleByVariantEquations() const
489 {
490 return getMemoryCell()->getFlag(IRREDUCIBLE_BY_VARIANT_EQUATIONS);
491 }
492
493 inline void
setHashValid()494 DagNode::setHashValid()
495 {
496 getMemoryCell()->setFlag(HASH_VALID);
497 }
498
499 inline bool
isHashValid() const500 DagNode::isHashValid() const
501 {
502 return getMemoryCell()->getFlag(HASH_VALID);
503 }
504
505 inline Byte
getTheoryByte() const506 DagNode::getTheoryByte() const
507 {
508 return getMemoryCell()->getByte();
509 }
510
511 inline void
setTheoryByte(Byte value)512 DagNode::setTheoryByte(Byte value)
513 {
514 getMemoryCell()->setByte(value);
515 }
516
517 //
518 // We use Symbol::fastComputeTrueSort() inline function which in turn uses
519 // our setSortIndex() inline function.
520 //
521 #include "symbol2.hh"
522
523 inline void
reduce(RewritingContext & context)524 DagNode::reduce(RewritingContext& context)
525 {
526 while (!isReduced())
527 {
528 if (!(topSymbol->eqRewrite(this, context)))
529 {
530 setReduced();
531 topSymbol->fastComputeTrueSort(this, context);
532 break;
533 }
534 }
535 }
536
537 inline void
mark()538 DagNode::mark()
539 {
540 Assert(this != 0, "bad dag node");
541 Assert(topSymbol->arity() >= 0 &&
542 topSymbol->arity() <= 30, // arbitrary - but helps catch bugs
543 "bad symbol at " << static_cast<void*>(topSymbol));
544 DagNode* d = this;
545 while (!(d->getMemoryCell()->isMarked()))
546 {
547 d->getMemoryCell()->setMarked();
548 //
549 // markArguments() returns a pointer our the last argument
550 // rather than calling mark() on it. This allows us to
551 // do tail recursion elimination on the last argument
552 // which is important for cons style lists.
553 //
554 d = d->markArguments();
555 if (d == 0)
556 break; // leaf
557 }
558 }
559
560 inline bool
inErrorSort()561 DagNode::inErrorSort()
562 {
563 int t = getSortIndex();
564 if (t == Sort::SORT_UNKNOWN)
565 {
566 topSymbol->computeBaseSort(this);
567 t = getSortIndex();
568 if (!(topSymbol->sortConstraintFree()))
569 setSortIndex(Sort::SORT_UNKNOWN);
570 }
571 return t == Sort::ERROR_SORT;
572 }
573
574 inline Sort*
getSort() const575 DagNode::getSort() const
576 {
577 return (getSortIndex() == Sort::SORT_UNKNOWN) ? 0 :
578 topSymbol->rangeComponent()->sort(getSortIndex());
579 }
580
581 inline void
computeTrueSort(RewritingContext & context)582 DagNode::computeTrueSort(RewritingContext& context)
583 {
584 if (getSortIndex() == Sort::SORT_UNKNOWN)
585 topSymbol->normalizeAndComputeTrueSort(this, context);
586 }
587
588 inline DagNode*
copyEagerUptoReduced()589 DagNode::copyEagerUptoReduced()
590 {
591 if (isReduced())
592 return this;
593 if (!isCopied())
594 {
595 copyPointer = copyEagerUptoReduced2(); // this destroys our top symbol
596 setCopied();
597 }
598 return copyPointer;
599 }
600
601 inline void
clearCopyPointers()602 DagNode::clearCopyPointers()
603 {
604 if (isCopied())
605 {
606 clearCopied();
607 topSymbol = copyPointer->topSymbol; // restore our top symbol from copy
608 clearCopyPointers2(); // can't safely call this until top symbol restored
609 }
610 }
611
612 inline DagNode*
copyReducible()613 DagNode::copyReducible()
614 {
615 DagNode* d = copyEagerUptoReduced();
616 clearCopyPointers();
617 return d;
618 }
619
620 inline DagNode*
copyAndReduce(RewritingContext & context)621 DagNode::copyAndReduce(RewritingContext& context)
622 {
623 DagNode* d = copyReducible();
624 d->reduce(context);
625 return d;
626 }
627
628 inline DagNode*
instantiate(const Substitution & substitution)629 DagNode::instantiate(const Substitution& substitution)
630 {
631 return isGround() ? 0 : instantiate2(substitution);
632 }
633
634 inline DagNode*
instantiateWithCopies(const Substitution & substitution,const Vector<DagNode * > & eagerCopies)635 DagNode::instantiateWithCopies(const Substitution& substitution, const Vector<DagNode*>& eagerCopies)
636 {
637 return isGround() ? 0 : instantiateWithCopies2(substitution, eagerCopies);
638 }
639
640 inline void
insertVariables(NatSet & occurs)641 DagNode::insertVariables(NatSet& occurs)
642 {
643 if (!isGround())
644 insertVariables2(occurs);
645 }
646
647 inline bool
indexVariables(NarrowingVariableInfo & indices,int baseIndex)648 DagNode::indexVariables(NarrowingVariableInfo& indices, int baseIndex)
649 {
650 if (isGround())
651 return true; // no variables below us to index
652 bool ground = indexVariables2(indices, baseIndex);
653 if (ground)
654 setGround();
655 return ground;
656 }
657
658 inline bool
leq(const Sort * sort) const659 DagNode::leq(const Sort* sort) const
660 {
661 return ::leq(getSortIndex(), sort);
662 }
663
664 inline bool
fastLeq(const Sort * sort) const665 DagNode::fastLeq(const Sort* sort) const
666 {
667 //
668 // Only works for sorts on which fastGeqSufficient() is true.
669 //
670 return sort->fastGeq(getSortIndex());
671 }
672
673 inline size_t
hash(size_t v1,size_t v2)674 DagNode::hash(size_t v1, size_t v2)
675 {
676 return (v1 * v1) ^ (v1 >> 16) ^ v2; // best function to date on empirical measurement
677 }
678
679 inline size_t
hash(size_t v1,size_t v2,size_t v3)680 DagNode::hash(size_t v1, size_t v2, size_t v3)
681 {
682 return (v1 * v1) ^ (v1 >> 16) ^ (v2 * v3);
683 }
684
685 #endif
686