Logo Search packages:      
Sourcecode: maude version File versions  Download package

Public Types | Public Member Functions | Protected Member Functions | Static Protected Member Functions | Private Types | Private Member Functions | Static Private Member Functions | Private Attributes | Static Private Attributes | Friends

ACU_DagNode Class Reference

Inheritance diagram for ACU_DagNode:
Inheritance graph
[legend]
Collaboration diagram for ACU_DagNode:
Collaboration graph
[legend]

List of all members.

Public Types

enum  NormalizationStatus { FRESH, ASSIGNMENT, TREE }
enum  ReturnResult { GROUND, NONGROUND, UNIMPLEMENTED }

Public Member Functions

 ACU_DagNode (ACU_Symbol *symbol, int size, NormalizationStatus status=FRESH)
RawDagArgumentIteratorarguments ()
int argVecComputeBaseSort () const
bool checkSort (const Sort *boundSort, Subproblem *&returnedSubproblem)
bool checkSort (const Sort *boundSort, RewritingContext &context)
void clearCopyPointers ()
int compare (const DagNode *other) const
int compareArguments (const DagNode *other) const
ReturnResult computeBaseSortForGroundSubterms ()
void computeGeneralizedSort (const SortBdds &sortBdds, const Vector< int > &realToBdd, Vector< Bdd > &generalizedSort)
bool computeSolvedForm (DagNode *rhs, UnificationContext &solution, PendingUnificationStack &pending)
bool computeSolvedForm2 (DagNode *rhs, UnificationContext &solution, PendingUnificationStack &pending)
void computeTrueSort (RewritingContext &context)
DagNodecopyAndReduce (RewritingContext &context)
DagNodecopyEagerUptoReduced ()
DagNodecopyReducible ()
void copySetRewritingFlags (const DagNode *other)
void copySortIndex (const DagNode *other)
DagNodecopyWithReplacement (Vector< RedexPosition > &redexStack, int first, int last)
DagNodecopyWithReplacement (int argIndex, DagNode *replacement)
bool equal (const DagNode *other) const
DagNodegetArgument (int i) const
size_t getHashValue ()
const MemoryCellgetMemoryCell () const
MemoryCellgetMemoryCell ()
int getMultiplicity (int i) const
NormalizationStatus getNormalizationStatus () const
int getSize () const
SortgetSort () const
int getSortIndex () const
Byte getTheoryByte () const
bool indexVariables (NarrowingVariableInfo &indices, int baseIndex)
bool indexVariables2 (NarrowingVariableInfo &indices, int baseIndex)
bool inErrorSort ()
void insertVariables (NatSet &occurs)
void insertVariables2 (NatSet &occurs)
DagNodeinstantiate (const Substitution &substitution)
DagNodeinstantiate2 (const Substitution &substitution)
DagNodeinstantiateWithReplacement (const Substitution &substitution, int argIndex, DagNode *newDag)
bool isFresh () const
bool isGround () const
bool isReduced () const
bool isTree () const
bool isUnrewritable () const
bool isUnstackable () const
bool leq (const Sort *sort) const
DagNodemakeClone ()
ExtensionInfomakeExtensionInfo ()
void mark ()
bool matchVariable (int index, const Sort *sort, bool copyToAvoidOverwriting, Substitution &solution, Subproblem *&returnedSubproblem, ExtensionInfo *extensionInfo)
bool matchVariableWithExtension (int index, const Sort *sort, Substitution &solution, Subproblem *&returnedSubproblem, ExtensionInfo *extensionInfo)
int nrArgs () const
void * operator new (size_t size)
void * operator new (size_t size, DagNode *old)
void overwriteWithClone (DagNode *old)
DagNodepartialConstruct (DagNode *replacement, ExtensionInfo *extensionInfo)
void partialReplace (DagNode *replacement, ExtensionInfo *extensionInfo)
void reduce (RewritingContext &context)
void replaceSymbol (Symbol *newSymbol)
void repudiateSortInfo ()
void setCallDtor ()
void setGround ()
void setNormalizationStatus (NormalizationStatus status)
void setReduced ()
void setSortIndex (int index)
void setTheoryByte (Byte value)
void setUnrewritable ()
void setUnstackable ()
void stackArguments (Vector< RedexPosition > &stack, int parentIndex, bool respectFrozen)
ACU_Symbolsymbol () const
void upgradeSortIndex (const DagNode *other)

Protected Member Functions

bool isHashValid () const
void setHashValid ()

Static Protected Member Functions

static size_t hash (size_t v1, size_t v2)
static size_t hash (size_t v1, size_t v2, size_t v3)

Private Types

typedef ACU_Pair Pair
enum  Sizes { CONVERT_THRESHOLD = 8, MERGE_THRESHOLD = 16, INITIAL_RUNS_BUFFER_SIZE = 4 }

Private Member Functions

int binarySearch (DagNode *key) const
int binarySearch (Term *key) const
void clearCopyPointers2 ()
void collapse (DagNode *arg)
void copyAndBinaryInsert (const ACU_DagNode *source, DagNode *dagNode, int multiplicity)
DagNodecopyEagerUptoReduced2 ()
bool dumbNormalizeAtTop ()
bool eliminateArgument (Term *target)
bool eliminateSubject (DagNode *target, int multiplicity, Vector< int > &subjectMultiplicity)
void fastMerge (const ACU_TreeDagNode *source0, const ACU_TreeDagNode *source1)
void fastMerge (const ACU_DagNode *source0, const ACU_TreeDagNode *source1)
void fastMerge (const ACU_DagNode *source0, const ACU_DagNode *source1)
int findFirstPotentialMatch (Term *key, const Substitution &partial) const
void flattenSortAndUniquize (int expansion)
void insertAlien (ACU_BaseDagNode *normalForm, int nMult, DagNode *alien, int aMult)
DagNodemarkArguments ()
void mergeSortAndUniquize ()
bool normalizeAtTop ()
void sortAndUniquize ()

Static Private Member Functions

static ArgVec< Pair >::iterator fastCopy (ArgVec< Pair >::const_iterator i, ArgVec< Pair >::const_iterator e, ArgVec< Pair >::iterator d)
static ArgVec< Pair >::iterator fastCopy (ACU_FastIter &i, ArgVec< Pair >::iterator d)

Private Attributes

ArgVec< PairargArray

Static Private Attributes

static Vector< int > runsBuffer

Friends

class ACU_AlienAlienLhsAutomaton
class ACU_BaseDagNode
class ACU_CollectorLhsAutomaton
class ACU_DagArgumentIterator
class ACU_ExtensionInfo
class ACU_GndLhsAutomaton
class ACU_LhsAutomaton
class ACU_NGA_LhsAutomaton
class ACU_NonLinearLhsAutomaton
class ACU_RhsAutomaton
class ACU_Subproblem
class ACU_Symbol
class ACU_Term
class ACU_TreeDagNode
class ACU_UnificationSubproblem2
class ACU_VarLhsAutomaton
ACU_DagNodegetACU_DagNode (DagNode *dagNode)

Detailed Description

Definition at line 38 of file ACU_DagNode.hh.


The documentation for this class was generated from the following files:

Generated by  Doxygen 1.6.0   Back to index