dpvis.datastructures
Interface RewriteSystem

All Superinterfaces:

java.io.Serializable

All Known Implementing Classes:

RewriteSystemImpl

public interface RewriteSystem
extends java.io.Serializable

Class modelling a Rewrite System.

Author:

Felix

Method Summary

void	filter(java.util.Map<java.lang.String,java.util.List<java.lang.Integer>> filtering) Applies an argument filtering to the rules of the rewrite system.
java.util.Set<Pair<java.lang.String,java.lang.Integer>>	getAllFunctionSymbolsWithArity() Gets the list of function symbols of the rewrite system together with the corresponding arities.
java.util.List<java.lang.String>	getDefinedFunctionSymbols() Gets the defined function symbols of the rewrite system, i.e.
java.util.List<Rule>	getRules() Gets the rules of the rewrite system.
java.util.Set<java.lang.String>	getSignature() Gets the signature of the rewrite system.
Strategy	getStrategy() Gets the strategy of the rewrite system.
java.util.List<java.lang.String>	getVariables() Extracts all variables that are used in the rules of the rewrite systems.
boolean	isConditional() Computes whether the rewrite system is conditional, i.e.
java.util.List<Term>	narrow(Term t) Narrows a given term with respect to this rewrite system.
void	removeContextSensitivityFlags() Removes all forbidden flags from the rules of this Rewrite System.
void	reverse() Swaps the direction of all rules of the Rewrite System, i.e.
void	setRules(java.util.List<Rule> rules) Sets the rules of the rewrite system.
void	setStrategy(Strategy strategy) Sets the strategy of the rewrite system.
void	setVariables(java.util.List<java.lang.String> variables) Sets those functions that shall be interpreted as variables.

Method Detail

reverse

void reverse()

Swaps the direction of all rules of the Rewrite System, i.e. the left-hand side of each rule becomes the new right-hand side and vice versa. Note that the reverse method may produce rule with variables as left-hand sides or extra variables in right-hand sides.

getRules

java.util.List<Rule> getRules()

Gets the rules of the rewrite system.

Returns:

The rules of the rewrite system.

setRules

void setRules(java.util.List<Rule> rules)

Sets the rules of the rewrite system.

Parameters:

rules - The new rules of the rewrite system.

getStrategy

Strategy getStrategy()

Gets the strategy of the rewrite system.

Returns:

The strategy of the rewrite system.

setStrategy

void setStrategy(Strategy strategy)

Sets the strategy of the rewrite system.

Parameters:

strategy - The new strategy of the rewrite system.

getVariables

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

Extracts all variables that are used in the rules of the rewrite systems.

Returns:

The list of variables of the rewrite system.

setVariables

void setVariables(java.util.List<java.lang.String> variables)

Sets those functions that shall be interpreted as variables.

Parameters:

variables - The new variables of the TRS.

getDefinedFunctionSymbols

java.util.List<java.lang.String> getDefinedFunctionSymbols()

Gets the defined function symbols of the rewrite system, i.e. the functions that occur as root of the left-hand side of at least one rule.

Returns:

The defined function symbols of the rewite system.

narrow

java.util.List<Term> narrow(Term t)

Narrows a given term with respect to this rewrite system. All possible one step narrowings are computed, i.e. all possible narrowing steps are applied to all subterms of the given term.

Parameters:

t - The term to be narrowed

Returns:

A list of all one-step narrowings of the given term.

getSignature

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

Gets the signature of the rewrite system.

Returns:

The signature of the rewrite system.

filter

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

Applies an argument filtering to the rules of the rewrite system. 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).

Parameters:

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

isConditional

boolean isConditional()

Computes whether the rewrite system is conditional, i.e. contains conditional rules.

Returns:

True if the rewrite system contains at least one conditional rule, False otherwise.

getAllFunctionSymbolsWithArity

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

Gets the list of function symbols of the rewrite system together with the corresponding arities.

Returns:

A list of Pairs of function symbols and arities.

removeContextSensitivityFlags

void removeContextSensitivityFlags()

Removes all forbidden flags from the rules of this Rewrite System.