dpvis.datastructures
Interface Term

All Superinterfaces:

java.io.Serializable

All Known Implementing Classes:

TermImpl

public interface Term
extends java.io.Serializable

Class modelling a term. A term consists of a function symbol of a variable (String function) and a possibly empty list of subterms (List subterms). Whether the function is a variable or a proper function symbol is indicated by a flag (boolean variable). Please make sure that no function symbol ends with a '#' character. Names ending with such characters are reserved for dependency pair symbols. Terms can be marked as forbidden (boolean forbidden) in case a context-sensitive strategy is used. This provides the computational convenience of not checking the status explicitly every time it is needed. However, the forbidden flags must be manually invalidated as soon as a subterm is put out of its context.

Author:

Felix

Field Summary

static java.lang.String

NEW_VARIABLE_PREFIX

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).
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.
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	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.

Field Detail

NEW_VARIABLE_PREFIX

static final java.lang.String NEW_VARIABLE_PREFIX

See Also:

Constant Field Values

Method Detail

markForbiddenTerms

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

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

Parameters:

repMap - The replacement map specifying the replacement restrictions.

markVariables

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.

Parameters:

vars - The list of variables that shall be marked.

getReplacementMap

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

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.

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

boolean isForbidden()

Gets the forbidden flag of this term.

Returns:

True if the forbidden flag is set, False otherwise.

setForbidden

void setForbidden(boolean forbidden)

Sets the forbidden flag of this term.

Parameters:

forbidden - The new value of the forbidden flag.

isVariable

boolean isVariable()

Gets the variable flag of this term.

Returns:

True if the variable flag is set, False otherwise.

setVariable

void setVariable(boolean variable)

Sets the variable flag of this term.

Parameters:

variable - The new value of the variable flag.

getFunction

java.lang.String getFunction()

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

Returns:

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

setFunction

void setFunction(java.lang.String function)

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

Parameters:

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

getSubterms

java.util.List<Term> getSubterms()

Gets the (immediate) subterms of this term.

Returns:

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

setSubterms

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

Sets the (immediate) subterms of this term.

Parameters:

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

getVariables

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

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

Returns:

Set of variables contained in this term.

getAllowedSubtermsWithRoot

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. The forbidden flags are preserved in the copies of the subterms.

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

void markRoot()

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

demarkRoot

void demarkRoot()

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

instantiate

void instantiate(Substitution subst)

Instantiates the term with the given substitution.

Parameters:

subst - The substitution that is used for the instantiation.

containsVariable

boolean containsVariable(java.lang.String var)

Computes whether the term contains the given variable.

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

void renameVariables()

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()); }

ren

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. Equal variables will not be equal anymore after this function is called.

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

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. Equal occurrences of subterms will not be replaced by equal variables.

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

void demarkVariables()

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.

isLinear

boolean isLinear()

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

Returns:

True if the term is linear, False otherwise.

getReplacingVariables

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. This function assumes that this term itself is not forbidden, i.e. is not subterm of some other term.

Returns:

The set of variables that occur at replacing positions.

getNonReplacingVariables

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.

Returns:

the set of variables occurring at forbidden positions.

getHiddenSymbols

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.

Returns:

The hidden symbols of this term.

narrow

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. 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.

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

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

Replaces each occurrence of the variable oldVar by newVar.

Parameters:

oldVar - The variable that is to be replaced.

newVar - The substitute variable.

containsVariablePrefix

boolean containsVariablePrefix(java.lang.String prefix)

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

Parameters:

prefix - The prefix whose presence shall be checked.

Returns:

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

getFunctions

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

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

Returns:

The set of function symbols contained in this term.

getSubtermsOfSignature

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. Forbidden flags are preserved in the copies of the subterms.

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

boolean isSubterm(Term potentialSubterm)

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.

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

boolean isProperSubterm(Term potentialSubterm)

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.

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

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.

Returns:

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

filter

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

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.

Parameters:

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

isNarrowable

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. This function is used to check whether this term is a (context-sensitive) Narrowing Normal Form w.r.t. R.

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

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.

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

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.

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

void removeContextSensitivityFlags()

Removes all forbidden flags from the rules of this Term.

getForbiddenFunctions

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

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

Returns:

All forbidden functions.

substituteAt

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.

Parameters:

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

substitute - The term to be substituted