dpvis.datastructures.impl
Class TermImpl

java.lang.Object
  dpvis.datastructures.impl.TermImpl

All Implemented Interfaces:

Term, java.io.Serializable

public class TermImpl
extends java.lang.Object
implements Term

See Also:

Serialized Form

Field Summary

Fields inherited from interface dpvis.datastructures.Term

NEW_VARIABLE_PREFIX

Constructor Summary

TermImpl(java.lang.String function, java.util.List<Term> subterms, boolean variable)

TermImpl(java.lang.String function, java.util.List<Term> subterms, boolean forbidden, boolean variable)

TermImpl(Term t)

Method Summary

void	cap(java.lang.String var, java.util.Collection<java.lang.String> definedFunctions) Replaces all (not necessarily immediate) subterms of this term that are rooted by function symbol given in the second argument by a new variable.
boolean	containsVariable(java.lang.String var) Computes whether the term contains the given variable.
boolean	containsVariablePrefix(java.lang.String prefix) Detects whether the variables of this term contain the given variable prefix.
void	demarkRoot() Removes the '#' mark from the root function of this term if it is present.
void	demarkVariables() Clears the variable flags of this term (and all of its subterms).
boolean	equals(java.lang.Object obj)
void	filter(java.util.Map<java.lang.String,java.util.List<java.lang.Integer>> filtering) Applies an argument filtering to the term.
java.util.Set<Term>	getAllForbiddenSubterms(boolean include) Computes all subterms of this term, that occur at forbidden positions (in the usual context-sensitve sense) in this term according to the forbidden flags.
java.util.Set<Pair<java.lang.String,java.lang.Integer>>	getAllFunctionSymbolsWithArity() Returns all function symbols (not variables) occurring in this term and its subterms, as pair together with their arities.
java.util.List<Term>	getAllowedSubtermsWithRoot(java.util.List<java.lang.String> rootSymbols) Extracts (deep) copies of all subterms, rooted by one of the given function symbols, that are allowed according to the forbidden flags.
java.util.Set<java.lang.String>	getForbiddenFunctions() Returns all function symbols that occur as root of a forbidden subterm of this term.
java.lang.String	getFunction() Gets the (root) function symbol (or variable) of this term.
java.util.Set<java.lang.String>	getFunctions() Gets all function symbols (not variables) contained in this term and all of its subterms.
java.util.Set<java.lang.String>	getHiddenSymbols() Computes the hidden symbols of a term, i.e. those function symbols (not variables) occurring as root of a non-replacing subterm of this term.
java.util.Set<java.lang.String>	getNonReplacingVariables() Returns the set of variables that occur at a non-replacing position in this term according to the forbidden flags.
java.util.List<java.lang.Integer>	getReplacementMap(java.lang.String function) Returns the replacment map for the specified function symbol, according to the forbidden flags of the term and its subterms.
java.util.Set<java.lang.String>	getReplacingVariables() Returns a set of variables occurring in this term at replacing positions according to the forbidden flags of this term and its subterms.
java.util.List<Term>	getSubterms() Gets the (immediate) subterms of this term.
java.util.Set<Term>	getSubtermsOfSignature(java.util.Set<java.lang.String> signature) Returns deep copies of all (not necessarily immediate) subterms of this term that are rooted by a function symbol contained in the given signature.
java.util.Set<java.lang.String>	getVariables() Computes all variables contained in this term (and its subterms), according to the variable flags.
boolean	hasConstructorContext(java.lang.String var, java.util.List<java.lang.String> definedSymbols) Checks whether the given variable occurs only inside constructor-contexts within this term, i.e. the root symbol if each subterm of this term containing the given variable is a constructor.
int	hashCode()
void	instantiate(Substitution subst) Instantiates the term with the given substitution.
boolean	isForbidden() Gets the forbidden flag of this term.
boolean	isLinear() Computes whether this term is linear, i.e. does not contain multiple occurrences of the same variable.
boolean	isNarrowable(RewriteSystem sys) Checks whether this term or one of its allowed (according to the forbidden flags) subterms can be narrowed according to the given Rewrite System R.
boolean	isProperSubterm(Term potentialSubterm) Checks if the given term is a proper subterm of this term.
boolean	isSubterm(Term potentialSubterm) Checks if the given term is a (not necessarily proper) subterm of this term.
boolean	isVariable() Gets the variable flag of this term.
void	markForbiddenTerms(java.util.Map<java.lang.String,java.util.List<java.lang.Integer>> repMap) Marks forbidden subterms according to the given replacement map.
void	markForbiddenTerms(java.lang.String function, java.util.List<java.lang.Integer> replacementMap)
void	markRoot() Marks the root function symbol with the character '#'.
void	markVariables(java.util.List<java.lang.String> vars) Marks the variables in a term, i.e. sets the variable flags for the term and all of its subterms.
java.util.Set<Pair<Term,Substitution>>	narrow(RewriteSystem trs, int variablePrefixCounter, boolean root, Strategy strat) Computes all (context-sensitive) narrowings of this term and its subterms (or only of the subterms if the root parameter is false) according to the given Rewrite System. the given strategy is used set the forbidden flags of resulting terms.
void	removeContextSensitivityFlags() Removes all forbidden flags from the rules of this Term.
void	ren(java.lang.String var) Linearizes the term, i.e. each variable of this term (and its subterms) is replaced by a new variable, in such a way that after the replacement the term is linear.
void	renameVariables() Renames all variables in the term by prefixing them with "_".
void	replaceVariable(java.lang.String oldVar, java.lang.String newVar) Replaces each occurrence of the variable oldVar by newVar.
void	setForbidden(boolean forbidden) Sets the forbidden flag of this term.
void	setFunction(java.lang.String function) Sets the (root) function symbol (or variable) of this term.
void	setSubterms(java.util.List<Term> subterms) Sets the (immediate) subterms of this term.
void	setVariable(boolean variable) Sets the variable flag of this term.
void	substituteAt(java.util.List<java.lang.Integer> pos, Term substitute) Substitutes the given substitute term for the subterm of this term at the specified position.
java.lang.String	toString()

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

TermImpl

public TermImpl(Term t)

TermImpl

public TermImpl(java.lang.String function,
                java.util.List<Term> subterms,
                boolean forbidden,
                boolean variable)

TermImpl

public TermImpl(java.lang.String function,
                java.util.List<Term> subterms,
                boolean variable)

Method Detail

markForbiddenTerms

public void markForbiddenTerms(java.util.Map<java.lang.String,java.util.List<java.lang.Integer>> repMap)

Description copied from interface: Term

Marks forbidden subterms according to the given replacement map. Call this function to reassign the forbidden flags.

Specified by:

markForbiddenTerms in interface Term

Parameters:

repMap - The replacement map specifying the replacement restrictions.

markForbiddenTerms

public void markForbiddenTerms(java.lang.String function,
                               java.util.List<java.lang.Integer> replacementMap)

markVariables

public void markVariables(java.util.List<java.lang.String> vars)

Description copied from interface: Term

Marks the variables in a term, i.e. sets the variable flags for the term and all of its subterms.

Specified by:

markVariables in interface Term

Parameters:

vars - The list of variables that shall be marked.

getReplacementMap

public java.util.List<java.lang.Integer> getReplacementMap(java.lang.String function)
                                                    throws AmbiguityException

Description copied from interface: Term

Returns the replacment map for the specified function symbol, according to the forbidden flags of the term and its subterms. An empty list is returned for variables and constants and null in case the symbol is not present in this term.

Specified by:

getReplacementMap in interface Term

Parameters:

function - The function whose replacement restrictions shall be returned.

Returns:

The list of allowed argument positions of the given function.

Throws:

AmbiguityException - If the same function occurs with different replacement restrictions. This indicates a missing invalidation of the forbidden flags of this terms earlier.

isForbidden

public boolean isForbidden()

Description copied from interface: Term

Gets the forbidden flag of this term.

Specified by:

isForbidden in interface Term

Returns:

True if the forbidden flag is set, False otherwise.

setForbidden

public void setForbidden(boolean forbidden)

Description copied from interface: Term

Sets the forbidden flag of this term.

Specified by:

setForbidden in interface Term

Parameters:

forbidden - The new value of the forbidden flag.

isVariable

public boolean isVariable()

Description copied from interface: Term

Gets the variable flag of this term.

Specified by:

isVariable in interface Term

Returns:

True if the variable flag is set, False otherwise.

setVariable

public void setVariable(boolean variable)

Description copied from interface: Term

Sets the variable flag of this term.

Specified by:

setVariable in interface Term

Parameters:

variable - The new value of the variable flag.

getFunction

public java.lang.String getFunction()

Description copied from interface: Term

Gets the (root) function symbol (or variable) of this term.

Specified by:

getFunction in interface Term

Returns:

The (root) function symbol (or variable) of this term.

setFunction

public void setFunction(java.lang.String function)

Description copied from interface: Term

Sets the (root) function symbol (or variable) of this term.

Specified by:

setFunction in interface Term

Parameters:

function - Thee new (root) function symbol (or variable) of this term.

getSubterms

public java.util.List<Term> getSubterms()

Description copied from interface: Term

Gets the (immediate) subterms of this term.

Specified by:

getSubterms in interface Term

Returns:

The (immediate) subterms of this term. May be null.

setSubterms

public void setSubterms(java.util.List<Term> subterms)

Description copied from interface: Term

Sets the (immediate) subterms of this term.

Specified by:

setSubterms in interface Term

Parameters:

subterms - The new (immediate) subterms of this term. May be null.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getVariables

public java.util.Set<java.lang.String> getVariables()

Description copied from interface: Term

Computes all variables contained in this term (and its subterms), according to the variable flags.

Specified by:

getVariables in interface Term

Returns:

Set of variables contained in this term.

getAllowedSubtermsWithRoot

public java.util.List<Term> getAllowedSubtermsWithRoot(java.util.List<java.lang.String> rootSymbols)

Description copied from interface: Term

Extracts (deep) copies of all subterms, rooted by one of the given function symbols, that are allowed according to the forbidden flags. The forbidden flags are preserved in the copies of the subterms.

Specified by:

getAllowedSubtermsWithRoot in interface Term

Parameters:

rootSymbols - The list of functions specifying the root symbols of subterms that shall be returned.

Returns:

The list of subterms with the given root symbols.

markRoot

public void markRoot()

Description copied from interface: Term

Marks the root function symbol with the character '#'.

Specified by:

markRoot in interface Term

demarkRoot

public void demarkRoot()

Description copied from interface: Term

Removes the '#' mark from the root function of this term if it is present. Otherwise this method does nothing.

Specified by:

demarkRoot in interface Term

instantiate

public void instantiate(Substitution subst)

Description copied from interface: Term

Instantiates the term with the given substitution.

Specified by:

instantiate in interface Term

Parameters:

subst - The substitution that is used for the instantiation.

containsVariable

public boolean containsVariable(java.lang.String var)

Description copied from interface: Term

Computes whether the term contains the given variable.

Specified by:

containsVariable in interface Term

Parameters:

var - The variable whose containment in the term shall be checked.

Returns:

True if the variable is contained in the term, False otherwise.

renameVariables

public void renameVariables()

Description copied from interface: Term

Renames all variables in the term by prefixing them with "_". Equal variables will still be equal after the renaming. Note that in order to prepare two terms such that they do not share any variables it is in general not sufficient to call renameVariables() on one of them. Rather you should use code like the following for terms t1, t2. Set varIntersection = new HashSet(t1.getVariables); while (!varIntersection.retainAll(t2.getVariables).isEmpty()) { t1.renameVaribles(); varIntersection = new HashSet(t1.getVariables()); }

Specified by:

renameVariables in interface Term

ren

public void ren(java.lang.String var)

Description copied from interface: Term

Linearizes the term, i.e. each variable of this term (and its subterms) is replaced by a new variable, in such a way that after the replacement the term is linear. Equal variables will not be equal anymore after this function is called.

Specified by:

ren in interface Term

Parameters:

var - The prefix for the new variable names, it will be extended by a counter yielding the full names of the new variables.

cap

public void cap(java.lang.String var,
                java.util.Collection<java.lang.String> definedFunctions)

Description copied from interface: Term

Replaces all (not necessarily immediate) subterms of this term that are rooted by function symbol given in the second argument by a new variable. Equal occurrences of subterms will not be replaced by equal variables.

Specified by:

cap in interface Term

Parameters:

var - The prefix for the new variable names, it will be extended by a counter yielding the full names of the new variables.

definedFunctions - A collection of function symbols defining the roots of subterms that are to be replaced.

demarkVariables

public void demarkVariables()

Description copied from interface: Term

Clears the variable flags of this term (and all of its subterms). After calling this method all variables of the term will be treated as constants.

Specified by:

demarkVariables in interface Term

isLinear

public boolean isLinear()

Description copied from interface: Term

Computes whether this term is linear, i.e. does not contain multiple occurrences of the same variable.

Specified by:

isLinear in interface Term

Returns:

True if the term is linear, False otherwise.

getReplacingVariables

public java.util.Set<java.lang.String> getReplacingVariables()

Description copied from interface: Term

Returns a set of variables occurring in this term at replacing positions according to the forbidden flags of this term and its subterms. This function assumes that this term itself is not forbidden, i.e. is not subterm of some other term.

Specified by:

getReplacingVariables in interface Term

Returns:

The set of variables that occur at replacing positions.

getHiddenSymbols

public java.util.Set<java.lang.String> getHiddenSymbols()

Description copied from interface: Term

Computes the hidden symbols of a term, i.e. those function symbols (not variables) occurring as root of a non-replacing subterm of this term.

Specified by:

getHiddenSymbols in interface Term

Returns:

The hidden symbols of this term.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

narrow

public java.util.Set<Pair<Term,Substitution>> narrow(RewriteSystem trs,
                                                     int variablePrefixCounter,
                                                     boolean root,
                                                     Strategy strat)

Description copied from interface: Term

Computes all (context-sensitive) narrowings of this term and its subterms (or only of the subterms if the root parameter is false) according to the given Rewrite System. the given strategy is used set the forbidden flags of resulting terms. However, in order to determine the allowed subterms that are narrowed the forbidden flags of this term are used. You need to make sure that forbidden flags of this term and the given strategy are coherent.

Specified by:

narrow in interface Term

Parameters:

trs - The Rewrite System that is used for the narrowing.

variablePrefixCounter - a number that is added as (additional) prefix to the variables that are created in the process of narrowing (through the variable renaming of the rules used for narrowing). This parameter can be useful to prevent narrowings from terms with disjoint variables from sharing variables, i.e. e.g. use a variable prefix of 0 for the first narrowing process and 300 for the second one. Alternatively you can rename the variables of narrowings by hand (@see Term#renameVariables).

root - A boolean indicating whether root narrowing steps shall be considered as well. True means that no root narrowings are considered.

strat - The Strategy that is used to set the forbidden flags of the narrowings.

Returns:

The of all narrowings together with the substitutions that were used in the unification process.

replaceVariable

public void replaceVariable(java.lang.String oldVar,
                            java.lang.String newVar)

Description copied from interface: Term

Replaces each occurrence of the variable oldVar by newVar.

Specified by:

replaceVariable in interface Term

Parameters:

oldVar - The variable that is to be replaced.

newVar - The substitute variable.

containsVariablePrefix

public boolean containsVariablePrefix(java.lang.String prefix)

Description copied from interface: Term

Detects whether the variables of this term contain the given variable prefix.

Specified by:

containsVariablePrefix in interface Term

Parameters:

prefix - The prefix whose presence shall be checked.

Returns:

True if the variable prefix is present in the term, False otherwise.

getFunctions

public java.util.Set<java.lang.String> getFunctions()

Description copied from interface: Term

Gets all function symbols (not variables) contained in this term and all of its subterms.

Specified by:

getFunctions in interface Term

Returns:

The set of function symbols contained in this term.

getSubtermsOfSignature

public java.util.Set<Term> getSubtermsOfSignature(java.util.Set<java.lang.String> signature)

Description copied from interface: Term

Returns deep copies of all (not necessarily immediate) subterms of this term that are rooted by a function symbol contained in the given signature. Forbidden flags are preserved in the copies of the subterms.

Specified by:

getSubtermsOfSignature in interface Term

Parameters:

signature - The signature identifying terms that shall be returned.

Returns:

The set of subterms rooted by a function symbole of the given signature.

isSubterm

public boolean isSubterm(Term potentialSubterm)

Description copied from interface: Term

Checks if the given term is a (not necessarily proper) subterm of this term. The forbidden flag is ignored when checking the equalsity of the given term and the subterms of this term.

Specified by:

isSubterm in interface Term

Parameters:

potentialSubterm - The term that is checked for an occurrence as a subterm of this term.

Returns:

True if the given term is a subterm of this term, False otherwise.

isProperSubterm

public boolean isProperSubterm(Term potentialSubterm)

Description copied from interface: Term

Checks if the given term is a proper subterm of this term. The forbidden flag is ignored when checking the equalsity of the given term and the subterms of this term.

Specified by:

isProperSubterm in interface Term

Parameters:

potentialSubterm - The term that is checked for an occurrence as a subterm of this term.

Returns:

True if the given term is a subterm of this term, False otherwise.

getAllFunctionSymbolsWithArity

public java.util.Set<Pair<java.lang.String,java.lang.Integer>> getAllFunctionSymbolsWithArity()

Description copied from interface: Term

Returns all function symbols (not variables) occurring in this term and its subterms, as pair together with their arities.

Specified by:

getAllFunctionSymbolsWithArity in interface Term

Returns:

The set of functions occurring in this term together with their arities.

filter

public void filter(java.util.Map<java.lang.String,java.util.List<java.lang.Integer>> filtering)

Description copied from interface: Term

Applies an argument filtering to the term. An argument filtering is specified by a mapping from functions to lists of argument positions, e.g. f -> [2, 3]. The argument positions in the list specify those arguments of the function symbol that are filtered, i.e. removed. So the above filtering applied to the term f(x, y, z) yields f(x). In order to indicate a collapsing filtering negative integers are used, e.g. f -> [-2], which yields y if applied to f(x, y, z). Note that when calling this function the filtered information is lost. So make sure to copy a term before filtering it, if its unfiltered version is still needed.

Specified by:

filter in interface Term

Parameters:

filtering - The filtering given by a mapping from functions to lists of argument positions.

isNarrowable

public boolean isNarrowable(RewriteSystem sys)

Description copied from interface: Term

Checks whether this term or one of its allowed (according to the forbidden flags) subterms can be narrowed according to the given Rewrite System R. This function is used to check whether this term is a (context-sensitive) Narrowing Normal Form w.r.t. R.

Specified by:

isNarrowable in interface Term

Parameters:

sys - The Rewrite System that is used for the narrowing.

Returns:

False if this term is Narrowing Normal Form w.r.t. R, True otherwise.

hasConstructorContext

public boolean hasConstructorContext(java.lang.String var,
                                     java.util.List<java.lang.String> definedSymbols)

Description copied from interface: Term

Checks whether the given variable occurs only inside constructor-contexts within this term, i.e. the root symbol if each subterm of this term containing the given variable is a constructor.

Specified by:

hasConstructorContext in interface Term

Parameters:

var - The variable that shall be checked for occurence in constructor contexts.

definedSymbols - The set of defined function symbols, and thus implicitly the set of constructors.

Returns:

True if the variable occurrs only in constructor contexts.

getAllForbiddenSubterms

public java.util.Set<Term> getAllForbiddenSubterms(boolean include)

Description copied from interface: Term

Computes all subterms of this term, that occur at forbidden positions (in the usual context-sensitve sense) in this term according to the forbidden flags.

Specified by:

getAllForbiddenSubterms in interface Term

Parameters:

include - Include this term in the list. If this flag is set all subterms of this term are included as well. Call the function with true only if the term on which it is called is forbidden. In doubt set it to false.

Returns:

The set of subterms of this term, that occur at forbidden positions.

removeContextSensitivityFlags

public void removeContextSensitivityFlags()

Description copied from interface: Term

Removes all forbidden flags from the rules of this Term.

Specified by:

removeContextSensitivityFlags in interface Term

getNonReplacingVariables

public java.util.Set<java.lang.String> getNonReplacingVariables()

Description copied from interface: Term

Returns the set of variables that occur at a non-replacing position in this term according to the forbidden flags.

Specified by:

getNonReplacingVariables in interface Term

Returns:

the set of variables occurring at forbidden positions.

getForbiddenFunctions

public java.util.Set<java.lang.String> getForbiddenFunctions()

Description copied from interface: Term

Returns all function symbols that occur as root of a forbidden subterm of this term.

Specified by:

getForbiddenFunctions in interface Term

Returns:

All forbidden functions.

substituteAt

public void substituteAt(java.util.List<java.lang.Integer> pos,
                         Term substitute)

Description copied from interface: Term

Substitutes the given substitute term for the subterm of this term at the specified position.

Specified by:

substituteAt in interface Term

Parameters:

pos - The position of the subterm that is to be replaced

substitute - The term to be substituted