de.uka.ilkd.key.util

Class ProofStarter

java.lang.Object

de.uka.ilkd.key.util.ProofStarter

public class ProofStarter
extends java.lang.Object

This class encapsulates the registration of a proof for a given problem. It then starts a proof attempt. After the proof attempt stops (successfully or not) the side proof is by default unregistered, but can be accessed via this class.

Author:

Richard Bubel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ProofStarter.UserProvidedInput Proof obligation for a given formula or sequent

Field Summary

Fields

Modifier and Type	Field and Description
private AutoSaver	autoSaver
private int	maxSteps
private Proof	proof
private ProverTaskListener	ptl
private Strategy	strategy
private long	timeout

Constructor Summary

Constructors

Constructor and Description
ProofStarter(boolean useAutoSaver) creates an instance of the ProofStarter
ProofStarter(ProverTaskListener ptl, boolean useAutoSaver) creates an instance of the ProofStarter

Method Summary

Modifier and Type	Method and Description
int	getMaxRuleApplications() Returns the maximal steps to be performed.
Proof	getProof() Returns the managed side Proof.
void	init(Proof proof)
void	init(Sequent sequentToProve, ProofEnvironment env, java.lang.String proofName) creates a new proof object for sequentToProve and registers it in the given environment
void	init(Term formulaToProve, ProofEnvironment env) creates a new proof object for formulaToProve and registers it in the given environment
void	setMaxRuleApplications(int maxSteps) set maximal steps to be performed
void	setStrategy(Strategy strategy)
void	setStrategyProperties(StrategyProperties sp)
void	setTimeout(long timeout) set timeout
ApplyStrategyInfo	start() starts proof attempt
ApplyStrategyInfo	start(ImmutableList<Goal> goals) starts proof attempt

Methods inherited from class java.lang.Object

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

Field Detail

proof

private Proof proof

maxSteps

private int maxSteps

timeout

private long timeout

ptl

private ProverTaskListener ptl

autoSaver

private AutoSaver autoSaver

strategy

private Strategy strategy

Constructor Detail

ProofStarter

public ProofStarter(boolean useAutoSaver)

creates an instance of the ProofStarter

Parameters:

the - ProofEnvironment in which the proof shall be performed

ProofStarter

public ProofStarter(ProverTaskListener ptl,
                    boolean useAutoSaver)

creates an instance of the ProofStarter

Parameters:

the - ProofEnvironment in which the proof shall be performed

Method Detail

init

public void init(Term formulaToProve,
                 ProofEnvironment env)
          throws ProofInputException

creates a new proof object for formulaToProve and registers it in the given environment

Throws:

ProofInputException

init

public void init(Sequent sequentToProve,
                 ProofEnvironment env,
                 java.lang.String proofName)
          throws ProofInputException

creates a new proof object for sequentToProve and registers it in the given environment

Throws:

ProofInputException

setTimeout

public void setTimeout(long timeout)

set timeout

Parameters:

timeout -

getMaxRuleApplications

public int getMaxRuleApplications()

Returns the maximal steps to be performed.

Returns:

The maximal steps to be performed.

setMaxRuleApplications

public void setMaxRuleApplications(int maxSteps)

set maximal steps to be performed

Parameters:

maxSteps -

setStrategy

public void setStrategy(Strategy strategy)

setStrategyProperties

public void setStrategyProperties(StrategyProperties sp)

start

public ApplyStrategyInfo start()

starts proof attempt

Returns:

the proof after the attempt terminated

start

public ApplyStrategyInfo start(ImmutableList<Goal> goals)

starts proof attempt

Returns:

the proof after the attempt terminated

init

public void init(Proof proof)

getProof

public Proof getProof()

Returns the managed side Proof.

Returns:

The managed side Proof.