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

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

MetaLevelOpSymbol Class Reference

Inheritance diagram for MetaLevelOpSymbol:
Inheritance graph
Collaboration diagram for MetaLevelOpSymbol:
Collaboration graph

List of all members.

Public Types

enum  CtorStatus { IS_CTOR = 1, IS_NON_CTOR = 2, IS_COMPLEX = IS_CTOR | IS_NON_CTOR }
typedef Vector< int > SourceSet

Public Member Functions

void addOpDeclaration (const Vector< Sort * > &domainAndRange, bool constructorFlag)
int arity () const
bool attachData (const Vector< Sort * > &opDeclaration, const char *purpose, const Vector< const char * > &data)
bool attachSymbol (const char *purpose, Symbol *symbol)
bool attachTerm (const char *purpose, Term *term)
virtual bool canProduceErrorSort () const
virtual bool canResolveTheoryClash ()
int compare (const Symbol *other) const
void compileEquations ()
virtual void compileOpDeclarations ()
virtual void compileRules ()
virtual void compileSortConstraints ()
void computeBaseSort (DagNode *subject)
void computeGeneralizedSort (const SortBdds &sortBdds, const Vector< int > &realToBdd, DagNode *subject, Vector< Bdd > &generalizedSort)
void computePossibleDomainSorts (const NatSet &rangeSorts, Vector< NatSet > &domainSorts)
virtual void computeSortFunctionBdds (const SortBdds &sortBdds, Vector< Bdd > &sortFunctionBdds) const
void constrainToExactSort (DagNode *subject, RewritingContext &context)
void constrainToSmallerSort (DagNode *subject, RewritingContext &context)
void copyAttachments (Symbol *original, SymbolMap *map)
const ConnectedComponentdomainComponent (int argNr) const
virtual bool domainSortAlwaysLeqThan (Sort *sort, int argNr)
bool eagerArgument (int argNr) const
bool eqRewrite (DagNode *subject, RewritingContext &context)
bool equationFree () const
bool evaluatedArgument (int argNr) const
void fastComputeTrueSort (DagNode *subject, RewritingContext &context)
void fillInSortInfo (Term *subject)
void finalizeSortInfo ()
int getCtorStatus () const
void getDataAttachments (const Vector< Sort * > &opDeclaration, Vector< const char * > &purposes, Vector< Vector< const char * > > &data)
const Vector< Equation * > & getEquations () const
const NatSetgetFrozen () const
unsigned int getHashValue ()
int getIndexWithinModule () const
int getLineNumber () const
const NatSetgetMaximalOpDeclSet (Sort *target)
MetaLevelgetMetaLevel () const
ModulegetModule () const
const Vector< OpDeclaration > & getOpDeclarations () const
const Vector< Rule * > & getRules () const
SortgetSingleNonErrorSort () const
const Vector< SortConstraint * > & getSortConstraints () const
const Vector< int > & getStrategy () const
void getSymbolAttachments (Vector< const char * > &purposes, Vector< Symbol * > &symbols)
void getTermAttachments (Vector< const char * > &purposes, Vector< Term * > &terms)
int getUniqueSortIndex ()
bool hasFrozenArguments () const
int id () const
virtual bool interSymbolPass ()
virtual bool isConstructor (DagNode *subject)
bool isMemoized () const
bool isStable () const
bool kindLevelDeclarationsOnly () const
DagNodemakeCanonical (DagNode *original, HashConsSet *hcs)
DagNodemakeCanonicalCopy (DagNode *original, HashConsSet *hcs)
DagNodemakeDagNode (const Vector< DagNode * > &args)
TermmakeTerm (const Vector< Term * > &args)
virtual UnificationSubproblemmakeUnificationSubproblem ()
void memoEnter (SourceSet &sourceSet, DagNode *destination)
bool memoRewrite (SourceSet &sourceSet, DagNode *subject, RewritingContext &context)
 MetaLevelOpSymbol (int id, int nrArgs, const Vector< int > &strategy)
bool mightMatchPattern (Term *pattern)
void normalizeAndComputeTrueSort (DagNode *subject, RewritingContext &context)
void offerEquation (Equation *equation)
void offerRule (Rule *rule)
void offerSortConstraint (SortConstraint *sortConstraint)
void orderSortConstraints ()
void postInterSymbolPass ()
virtual void postOpDeclarationPass ()
ConnectedComponentrangeComponent () const
virtual bool rangeSortAlwaysLeqThan (Sort *sort)
virtual bool rangeSortNeverLeqThan (Sort *sort)
void reset ()
virtual void resetRules ()
virtual void restoreHiddenState ()
bool ruleFree () const
virtual DagNoderuleRewrite (DagNode *subject, RewritingContext &context)
virtual void saveHiddenState ()
virtual void setFrozen (const NatSet &frozen)
void setLineNumber (int lineNr)
void setModuleInfo (Module *module, int indexWithinModule)
void setStrategy (const Vector< int > &userStrategy, int nrArgs, bool memoFlag)
bool sortConstraintFree () const
void stackArguments (DagNode *subject, Vector< RedexPosition > &stack, int parentIndex)
bool standardStrategy () const
int traverse (int position, int sortIndex) const
bool unevaluatedArguments () const
virtual int unificationPriority () const

Static Public Member Functions

static FreeSymbolnewFreeSymbol (int id, int arity, const Vector< int > &strategy=standard, bool memoFlag=false)

Protected Member Functions

bool acceptEquation (Equation *equation)
bool acceptRule (Rule *rule)
bool acceptSortConstraint (SortConstraint *sortConstraint)
bool applyReplace (DagNode *subject, RewritingContext &context, ExtensionInfo *extensionInfo=0)
bool applyReplaceNoOwise (DagNode *subject, RewritingContext &context, ExtensionInfo *extensionInfo=0)
DagNodeapplyRules (DagNode *subject, RewritingContext &context, ExtensionInfo *extensionInfo)
int ctorTraverse (int position, int sortIndex) const
void resetEachRule ()
bool safeToInspectSortConstraints ()
bool specialSortHandling () const

Protected Attributes

FreeNet discriminationNet

Static Protected Attributes

static const Vector< int > standard

Private Types

typedef bool(MetaLevelOpSymbol::* DescentFunctionPtr )(FreeDagNode *subject, RewritingContext &context)

Private Member Functions

bool complexStrategy (DagNode *subject, RewritingContext &context)
bool dagifySubstitution (const Vector< Term * > &variables, Vector< Term * > &values, Vector< DagRoot * > &dags, RewritingContext &context)
bool downSearchType (DagNode *arg, SequenceSearch::SearchType &searchType) const
bool getCachedNarrowingSequenceSearch (MetaModule *m, FreeDagNode *subject, RewritingContext &context, Int64 solutionNr, NarrowingSequenceSearch *&search, Int64 &lastSolutionNr)
void initializeSubstitution (Vector< Symbol * > &variables, Vector< Term * > &values, VariableInfo &rule, Substitution &substitution)
MatchSearchStatemakeMatchSearchState (MetaModule *m, FreeDagNode *subject, RewritingContext &context) const
MatchSearchStatemakeMatchSearchState2 (MetaModule *m, FreeDagNode *subject, RewritingContext &context) const
NarrowingSequenceSearchmakeNarrowingSequenceSearch (MetaModule *m, FreeDagNode *subject, RewritingContext &context) const
NarrowingSequenceSearchmakeNarrowingSequenceSearch2 (MetaModule *m, FreeDagNode *subject, RewritingContext &context) const
RewriteSequenceSearchmakeRewriteSequenceSearch (MetaModule *m, FreeDagNode *subject, RewritingContext &context) const
bool metaUnify2 (FreeDagNode *subject, RewritingContext &context, bool disjoint)
 NO_COPYING (MetaLevelOpSymbol)
bool noDuplicates (const Vector< Term * > &terms)
bool okToBind ()

Static Private Member Functions

static bool getCachedMatchSearchState (MetaModule *m, FreeDagNode *subject, RewritingContext &context, Int64 solutionNr, MatchSearchState *&state, Int64 &lastSolutionNr)
static bool getCachedRewriteSearchState (MetaModule *m, FreeDagNode *subject, RewritingContext &context, Int64 solutionNr, RewriteSearchState *&state, Int64 &lastSolutionNr)
static bool getCachedRewriteSequenceSearch (MetaModule *m, FreeDagNode *subject, RewritingContext &context, Int64 solutionNr, RewriteSequenceSearch *&search, Int64 &lastSolutionNr)
static bool getCachedUnificationProblem (MetaModule *m, FreeDagNode *subject, Int64 solutionNr, UnificationProblem *&unification, Int64 &lastSolutionNr)
static DagNodeterm2Dag (Term *t)
static RewritingContextterm2RewritingContext (Term *term, RewritingContext &context)

Private Attributes

DescentFunctionPtr descentFunction

Detailed Description

Definition at line 31 of file metaLevelOpSymbol.hh.

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

Generated by  Doxygen 1.6.0   Back to index