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
|
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 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
|
private Proof proof
private int maxSteps
private long timeout
private ProverTaskListener ptl
private AutoSaver autoSaver
private Strategy strategy
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)