public class Engine
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
Engine.ExecutionMode
Engine execution mode flags.
|
Constructor and Description |
---|
Engine(_Prover prover,
_AbstractGoal goal)
Builds an instance of the engine act that allows to search for a proof of
the goal specified as argument (initial goal) using the specified
prover.
|
Engine(_Prover prover,
_AbstractGoal goal,
Engine.ExecutionMode mode)
Builds an instance of the engine act that allows to search for a proof of
the goal specified as argument (initial goal) using the specified
prover.
|
Modifier and Type | Method and Description |
---|---|
_AbstractGoal |
getInitialGoal()
Returns the initial goal.
|
IterationInfo |
getLastIterationInfo()
Returns a bunch of detailed information on the last iteration performed by
the prover.
|
ProofSearchResult |
getResult()
Returns the result of the last proof-search.
|
Trace |
getTrace()
Returns the trace of the last proof-search or null if the engine has not
been executed in trace mode (see
Engine.ExecutionMode ). |
ProofSearchResult |
searchProof()
Searches a proof for the initial goal and, if it terminates, returns the
result of the proof-search.
|
public Engine(_Prover prover, _AbstractGoal goal, Engine.ExecutionMode mode)
prover
- the prover to use.goal
- the initial node set.mode
- the execution mode.public Engine(_Prover prover, _AbstractGoal goal)
prover
- the prover to use.goal
- the initial node set.public _AbstractGoal getInitialGoal()
public ProofSearchResult getResult()
public Trace getTrace()
Engine.ExecutionMode
).public ProofSearchResult searchProof()
public IterationInfo getLastIterationInfo()