public class ProofStarter
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
ProofStarter.UserProvidedInput
Proof obligation for a given formula or sequent
|
Constructor and Description |
---|
ProofStarter(boolean useAutoSaver)
creates an instance of the ProofStarter
|
ProofStarter(ProverTaskListener ptl,
boolean useAutoSaver)
creates an instance of the ProofStarter
|
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
|
public ProofStarter(boolean useAutoSaver)
the
- ProofEnvironment in which the proof shall be performedpublic ProofStarter(ProverTaskListener ptl, boolean useAutoSaver)
the
- ProofEnvironment in which the proof shall be performedpublic void init(Term formulaToProve, ProofEnvironment env) throws ProofInputException
ProofInputException
public void init(Sequent sequentToProve, ProofEnvironment env, java.lang.String proofName) throws ProofInputException
ProofInputException
public void setTimeout(long timeout)
timeout
- public int getMaxRuleApplications()
public void setMaxRuleApplications(int maxSteps)
maxSteps
- public void setStrategy(Strategy strategy)
public void setStrategyProperties(StrategyProperties sp)
public ApplyStrategyInfo start()
public ApplyStrategyInfo start(ImmutableList<Goal> goals)
public void init(Proof proof)
Copyright © 2003-2019 The KeY-Project.