de.uka.ilkd.key.proof.delayedcut

Interface ApplicationCheck

All Known Implementing Classes:

ApplicationCheck.NoNewSymbolsCheck

public interface ApplicationCheck

Determines conflicts relevant for a delayed cut application.

Author:

Benjamin Niedermann

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	ApplicationCheck.NoNewSymbolsCheck Implementation of an ApplicationCheck which examines if there are new symbols introduced below the cut node.

Method Summary

Modifier and Type	Method and Description
java.lang.String	check(Node cutNode, Term cutFormula)

Method Detail

check

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

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.