de.uka.ilkd.key.prover

Interface ProverCore

All Known Implementing Classes:

AbstractProverCore, ApplyStrategy

public interface ProverCore

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PROCESSING_STRATEGY constant used by some listeners to determine if a proof macro is running

Method Summary

Modifier and Type	Method and Description
void	addProverTaskObserver(ProverTaskListener observer) adds a task listener
void	clear() Used by, e.g., InteractiveProver.clear() in order to prevent memory leaking.
boolean	hasBeenInterrupted() Returns true iff the last run has been stopped due to a received InterruptedException.
void	removeProverTaskObserver(ProverTaskListener observer) removes a task listener
ApplyStrategyInfo	start(Proof proof, Goal goal) starts a proof search for a given goals using the given strategy settings instead the ones configures in the proof
ApplyStrategyInfo	start(Proof proof, ImmutableList<Goal> goals) starts a proof search for a set of goals using the given strategy settings instead the ones configures in the proof
ApplyStrategyInfo	start(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout, boolean stopAtFirstNonCloseableGoal) This entry point to the proof may provide inconsistent data.
ApplyStrategyInfo	start(Proof proof, ImmutableList<Goal> goals, StrategySettings stratSet) starts a proof search for a set of goals using the given strategy settings instead the ones configures in the proof

Field Detail

PROCESSING_STRATEGY

static final java.lang.String PROCESSING_STRATEGY

constant used by some listeners to determine if a proof macro is running

See Also:

Constant Field Values

Method Detail

start

ApplyStrategyInfo start(Proof proof,
                        Goal goal)

starts a proof search for a given goals using the given strategy settings instead the ones configures in the proof

Parameters:

proof - the Proof instance

goal - the goal to prove

Returns:

an information object about the performed work (e.g. number of rules applied)

start

ApplyStrategyInfo start(Proof proof,
                        ImmutableList<Goal> goals)

starts a proof search for a set of goals using the given strategy settings instead the ones configures in the proof

Parameters:

proof - the Proof instance

goals - list of goals to prove

Returns:

an information object about the performed work (e.g. number of rules applied)

start

ApplyStrategyInfo start(Proof proof,
                        ImmutableList<Goal> goals,
                        StrategySettings stratSet)

starts a proof search for a set of goals using the given strategy settings instead the ones configures in the proof

Parameters:

proof - the Proof instance

goals - list of goals to prove

stratSet - the strategy settings to use

Returns:

an information object about the performed work (e.g. number of rules applied)

start

ApplyStrategyInfo start(Proof proof,
                        ImmutableList<Goal> goals,
                        int maxSteps,
                        long timeout,
                        boolean stopAtFirstNonCloseableGoal)

This entry point to the proof may provide inconsistent data. The properties within the proof may differ to the explicit data. This is discouraged. starts a proof search for a set of goals

Parameters:

proof - the Proof instance

goals - list of goals to prove

maxSteps - an int with the maximal number of rule applications to be performed

timeout - a long with a timeout when tyo stop the proof search at latest

stopAtFirstNonCloseableGoal - true if the prover shall stop at the first encountered non-closable goal

Returns:

an information object about the performed work (e.g. number of rules applied)

addProverTaskObserver

void addProverTaskObserver(ProverTaskListener observer)

adds a task listener

Parameters:

observer - the listener to add

removeProverTaskObserver

void removeProverTaskObserver(ProverTaskListener observer)

removes a task listener

Parameters:

observer - the listener to remove

clear

void clear()

Used by, e.g., InteractiveProver.clear() in order to prevent memory leaking. When a proof obligation is abandoned all references to the proof must be reset.

hasBeenInterrupted

boolean hasBeenInterrupted()

Returns true iff the last run has been stopped due to a received InterruptedException. This exception would have been swallowed by the system. However, the cancelled flag is set in this case which allows detection of such a condition.

Returns:

whether the last run has been interrupted