dpvis.datastructures
Interface DependencyPairProblem

All Superinterfaces:

java.io.Serializable

All Known Implementing Classes:

DependencyPairProblemImpl

public interface DependencyPairProblem
extends java.io.Serializable

Class for storing a single Dependency Pair Problem.

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 dependency pairs and the rewrite system of this problem.
java.util.Set<Rule>	getDependencyPairs() Gets the set of Dependency Pairs that are contained in this DP problem
java.util.Set<java.lang.String>	getDependencyPairSymbols() Returns the root symbols of left- and right-hand sides of dependency pairs of the DP problem.
java.util.Set<java.lang.String>	getHiddenSymbols() Computes the hidden symbols of a DP problem (P, R), i.e. those defined functions of the signature of R, that occur at a forbidden position in one of the right hand sides of pairs in P.
RewriteSystem	getRewriteSystem() Gets the Rewrite System associated with this DP Problem
java.util.Set<java.lang.String>	getSignature() Gets the signature specifying those terms whose termination shall be proved.
boolean	isComplete()
boolean	isContextSensitive()
boolean	isMinimal()
void	setComplete(boolean complete)
void	setContextSensitive(boolean contextSensitive)
void	setDependencyPairs(java.util.Set<Rule> dependencyPairs) Sets the set of Dependency pairs
void	setMinimal(boolean minimal)
void	setRewriteSystem(RewriteSystem rewriteSystem) Sets the Rewrite System for this DP Problem
void	setSignature(java.util.Set<java.lang.String> signature) Sets the signature specifying those terms whose termination shall be proved.

Method Detail

getDependencyPairs

java.util.Set<Rule> getDependencyPairs()

Gets the set of Dependency Pairs that are contained in this DP problem

Returns:

Set of Dependency Pairs

setDependencyPairs

void setDependencyPairs(java.util.Set<Rule> dependencyPairs)

Sets the set of Dependency pairs

Parameters:

dependencyPairs - The new Set of Dependency Pairs

getRewriteSystem

RewriteSystem getRewriteSystem()

Gets the Rewrite System associated with this DP Problem

Returns:

The RewriteSystem

setRewriteSystem

void setRewriteSystem(RewriteSystem rewriteSystem)

Sets the Rewrite System for this DP Problem

Parameters:

rewriteSystem - The new Rewrite System

getHiddenSymbols

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

Computes the hidden symbols of a DP problem (P, R), i.e. those defined functions of the signature of R, that occur at a forbidden position in one of the right hand sides of pairs in P.

Returns:

The set of hidden symbols

getSignature

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

Gets the signature specifying those terms whose termination shall be proved. For a DP Problem (P, R) this will be the signature of R most of the time.

Returns:

The signature identifying relevant terms for the termination analysis as set of Functions.

setSignature

void setSignature(java.util.Set<java.lang.String> signature)

Sets the signature specifying those terms whose termination shall be proved. For a DP Problem (P, R) this will be the signature of R most of the time.

Parameters:

signature - The signature identifying relevant terms for the termination analysis as set of Functions.

getDependencyPairSymbols

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

Returns the root symbols of left- and right-hand sides of dependency pairs of the DP problem.

Returns:

The dependency pair symbols (sometimes called tuple symbols) of the DP problem.

filter

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

Applies an argument filtering to the dependency pairs and the rewrite system of this problem. 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.

isMinimal

boolean isMinimal()

setMinimal

void setMinimal(boolean minimal)

isContextSensitive

boolean isContextSensitive()

setContextSensitive

void setContextSensitive(boolean contextSensitive)

isComplete

boolean isComplete()

setComplete

void setComplete(boolean complete)