de.uka.ilkd.key.proof.delayedcut

Class ApplicationCheck.NoNewSymbolsCheck

java.lang.Object

de.uka.ilkd.key.proof.delayedcut.ApplicationCheck.NoNewSymbolsCheck

All Implemented Interfaces:

ApplicationCheck

Enclosing interface:

ApplicationCheck

public static class ApplicationCheck.NoNewSymbolsCheck
extends java.lang.Object
implements ApplicationCheck

Implementation of an ApplicationCheck which examines if there are new symbols introduced below the cut node. The existence of such symbols prohibits the replay procedure: This restriction ensures that symbols introduced within the respective subtrees are actually new symbols, as required by the corresponding rule definitions.

Author:

Benjamin Niedermann

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.proof.delayedcut.ApplicationCheck

ApplicationCheck.NoNewSymbolsCheck

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	ADD_INFORMATION
private static java.lang.String	INFORMATION1
private static java.lang.String	INFORMATION2
private java.util.Set<java.lang.String>	names
private Node	node

Constructor Summary

Constructors

Constructor and Description
NoNewSymbolsCheck()

Method Summary

Modifier and Type	Method and Description
private void	buildCaches(Node cutNode)
java.lang.String	check(Node cutNode, Term cutFormula)
private java.lang.String	checkFormula(Term formula)
private void	clearCaches()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

node

private Node node

names

private java.util.Set<java.lang.String> names

INFORMATION1

private static final java.lang.String INFORMATION1

See Also:

Constant Field Values

INFORMATION2

private static final java.lang.String INFORMATION2

See Also:

Constant Field Values

ADD_INFORMATION

private static final java.lang.String ADD_INFORMATION

See Also:

Constant Field Values

Constructor Detail

NoNewSymbolsCheck

public NoNewSymbolsCheck()

Method Detail

check

public java.lang.String check(Node cutNode,
                              Term cutFormula)

Specified by:

check in interface ApplicationCheck

Parameters:

cutNode - The node at which to apply the delayed cut.

cutFormula - The cut formula.

Returns:

A String representation of a possible conflict affecting a delayed cut application for the given node and cut formula or null if there is no conflict.

clearCaches

private void clearCaches()

buildCaches

private void buildCaches(Node cutNode)

checkFormula

private java.lang.String checkFormula(Term formula)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object