de.uka.ilkd.key.proof.join

Interface PredicateEstimator

All Known Implementing Classes:

StdPredicateEstimator

public interface PredicateEstimator

Responsible for estimating decision predicates for a join.

Author:

Benjamin Niedermann

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static interface	PredicateEstimator.Result Encapsulates a decision predicate for the delayed cut mechanism and the common parent node at which to prune, i.e. apply the delayed cut.

Field Summary

Fields

Modifier and Type	Field and Description
static PredicateEstimator	STD_ESTIMATOR

Method Summary

Modifier and Type	Method and Description
PredicateEstimator.Result	estimate(ProspectivePartner partner, Proof proof)

Field Detail

STD_ESTIMATOR

static final PredicateEstimator STD_ESTIMATOR

Method Detail

estimate

PredicateEstimator.Result estimate(ProspectivePartner partner,
                                   Proof proof)

Parameters:

partner - Structure comprising the partners of a join.

proof - The underlying proof.

Returns:

A decision predicate for the two nodes in partner. The predicate should be true in the sequent of the first node and false in the sequent of the second node.