public interface ProverCore
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
|
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
|
static final java.lang.String PROCESSING_STRATEGY
ApplyStrategyInfo start(Proof proof, Goal goal)
proof
- the Proof instancegoal
- the goal to proveApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals)
proof
- the Proof instancegoals
- list of goals to proveApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, StrategySettings stratSet)
proof
- the Proof instancegoals
- list of goals to provestratSet
- the strategy settings to useApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout, boolean stopAtFirstNonCloseableGoal)
proof
- the Proof instancegoals
- list of goals to provemaxSteps
- an int with the maximal number of rule applications to be performedtimeout
- a long with a timeout when tyo stop the proof search at lateststopAtFirstNonCloseableGoal
- true if the prover shall stop at the first
encountered non-closable goalvoid addProverTaskObserver(ProverTaskListener observer)
observer
- the listener to addvoid removeProverTaskObserver(ProverTaskListener observer)
observer
- the listener to removevoid clear()
InteractiveProver.clear()
in order to prevent memory leaking.
When a proof obligation is abandoned all references to the proof must be reset.boolean hasBeenInterrupted()
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.