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

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

ACU_NumberOpSymbol Class Reference

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

List of all members.

Public Types

enum  CtorStatus { IS_CTOR = 1, IS_NON_CTOR = 2, IS_COMPLEX = IS_CTOR | IS_NON_CTOR }
enum  PermuteStrategy { EAGER, SEMI_EAGER, LAZY }
typedef Vector< int > SourceSet
enum  Structure { UNSTRUCTURED, LIMIT_SORT, PURE_SORT }

Public Member Functions

 ACU_NumberOpSymbol (int id)
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)
virtual bool attachTerm (const char *purpose, Term *term)
virtual bool canProduceErrorSort () const
bool canResolveTheoryClash ()
int compare (const Symbol *other) const
virtual void compileEquations ()
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)
int computeMultSortIndex (int index1, int index2, int multiplicity)
void computePossibleDomainSorts (const NatSet &rangeSorts, Vector< NatSet > &domainSorts)
virtual void computeSortFunctionBdds (const SortBdds &sortBdds, Vector< Bdd > &sortFunctionBdds) const
int computeSortIndex (int index1, int index2)
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 ()
TermgetIdentity () const
DagNodegetIdentityDag ()
int getIndexWithinModule () const
int getLineNumber () const
const NatSetgetMaximalOpDeclSet (Sort *target)
ModulegetModule () const
const Vector< OpDeclaration > & getOpDeclarations () const
PermuteStrategy getPermuteStrategy () 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)
virtual void getTermAttachments (Vector< const char * > &purposes, Vector< Term * > &terms)
int getUniqueSortIndex ()
bool hasCyclicIdentity () const
bool hasFrozenArguments () const
bool hasIdentity () const
bool hasUnequalLeftIdentityCollapse () const
bool hasUnequalRightIdentityCollapse () const
int id () const
bool interSymbolPass ()
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)
UnificationSubproblemmakeUnificationSubproblem ()
void memoEnter (SourceSet &sourceSet, DagNode *destination)
bool memoRewrite (SourceSet &sourceSet, DagNode *subject, RewritingContext &context)
bool mightCollapseToOurSymbol (const Term *subterm) const
bool mightMatchOurIdentity (const Term *subterm) const
bool mightMatchPattern (Term *pattern)
void normalizeAndComputeTrueSort (DagNode *subject, RewritingContext &context)
void offerEquation (Equation *equation)
void offerRule (Rule *rule)
void offerSortConstraint (SortConstraint *sortConstraint)
void orderSortConstraints ()
virtual void postInterSymbolPass ()
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
DagNoderuleRewrite (DagNode *subject, RewritingContext &context)
virtual void saveHiddenState ()
void setFrozen (const NatSet &frozen)
void setIdentity (Term *id)
void setLineNumber (int lineNr)
void setModuleInfo (Module *module, int indexWithinModule)
void setPermuteFrozen (const NatSet &frozen)
void setPermuteStrategy (const Vector< int > &userStrategy)
void setStrategy (const Vector< int > &userStrategy, int nrArgs, bool memoFlag)
int sortBound (const Sort *sort) const
bool sortConstraintFree () const
Structure sortStructure (const Sort *sort) const
void stackArguments (DagNode *subject, Vector< RedexPosition > &stack, int parentIndex)
bool standardStrategy () const
bool takeIdentity (const Sort *sort)
int traverse (int position, int sortIndex) const
bool unevaluatedArguments () const
int unificationPriority () const
const SortuniformSort () const
bool useTree () const

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)
void commutativeSortCompletion ()
int ctorTraverse (int position, int sortIndex) const
void idempotentSortCheck ()
void leftIdentitySortCheck ()
DagNodemakeDagNode (const Vector< DagNode * > &args, const Vector< int > &multiplicities)
void processIdentity ()
bool reduceArgumentsAndNormalize (DagNode *subject, RewritingContext &context)
void resetEachRule ()
void rightIdentitySortCheck ()
bool safeToInspectSortConstraints ()
bool specialSortHandling () const

Static Protected Attributes

static const Vector< int > standard

Private Member Functions

bool eqRewrite2 (DagNode *subject, RewritingContext &context)

Private Attributes

MinusSymbolminusSymbol
int op
SuccSymbolsuccSymbol

Detailed Description

Definition at line 30 of file ACU_NumberOpSymbol.hh.


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

Generated by  Doxygen 1.6.0   Back to index