public class Launcher
extends java.lang.Object
configX()
methods.
In details the client must invoke:
configLauncherName(String)
to define the name of the main
application executing the launcher; this name is used in the help message
generated by the launcher.configStandardInputReader(_ProblemReader)
to define
the reader used to read a problem from standard input.configProblemDescriptionReader(String, Class)
and configProblemDescriptionReader(String, Class, boolean)
to define
at least a problem description reader (more than one reader can be
configured).configTheoremProver(String, Class)
and
configTheoremProver(String, Class, boolean)
to define at least a
theorem prover (more than one theorem prover can be configured).optConfigX
methods. In details:
optConfigCmdLineOptions(Options)
: to define command line options
for the client. The names of the added options cannot overlap the names of
the options defined by the launcher.optConfigInputSyntax(String)
: to define a message with the
description of the syntax of the formulas provided by standard input.optConfigWelcomeMessage(String)
: to define a welcome message.optConfigSingleExecutionConfigurator(_SingleExecutionConfigurator)
:
set the configurator to invoke before every execution. a
_SingleExecutionConfigurator
is an object allowing to properly
configure every element of the pipeline before its execution.
The method getCmdLineOptionsManager()
can be used to get direct
access to the command line options manager of the launcher.
processCmdLineArguments(String[])
providing as argument the
strings on the command line. These arguments are processed according with the
syntax of the defined options. If the syntax of the argument does not
contains errors the launcher configure its runtime options accordingly. Then
the method returns the Launcher.LaunchConfiguration
describing the launch
configuration corresponding to the parsed options (if any).
The launcher predefined command line options are the following:
--f3time Prints on the standard output timing info in
f3 format.
-h Print usage message and exit.
-i Read the formula from standard input.
--jtabwbtime Prints on the standard output timing info in
JTabWb format.
--latex-ctrees Save the LaTeX of the c-trees generated by the
proof-search in the specified file.
--latex-proof Save the LaTeX of the proof generated by a
successful proof-search in the specified file.
--log Save execution details in the the specified
file.
--logdir <filename> Defines the directory used to save log files.
-p <name> Set the theorem prover, if this option is not
set the default is used.
--provers Detailed description of available provers.
-r <name> Set the formula reader, if this option is not
set the default is used.
--readers Detailed description of available readers.
--save-trace Save the trace of the proof-search in the
specified file.
--testset <test-name> Execute a test on the problems specified on
the command line. test-name is used to name
the log files.
--time Save time execution details in the specified
file.
-v Print detailed informations on the proof
process.
The methods launch()
executes the proof-search according with the
specified command line arguments.
When the execution of the proof-search terminates, the client can inspect the
details of the performed proof-search accessing the ProofSearchData
object returned by the getLastProofSearchData()
method.
Modifier and Type | Class and Description |
---|---|
static class |
Launcher.LaunchConfiguration
An object of this class describes the current configuration of the
launcher.
|
static class |
Launcher.TestStatus
Describes the status of a test.
|
Constructor and Description |
---|
Launcher()
Constructs a new launcher.
|
Modifier and Type | Method and Description |
---|---|
void |
configInitialNodeSetBuilder(_InitialGoalBuilder builder)
Defines the initial node set builder to use.
|
void |
configLauncherName(java.lang.String launcherClassName)
Defines the name of the class using this launcher to execute a prover.
|
<T extends _ProblemReader> |
configProblemDescriptionReader(java.lang.String name,
java.lang.Class<T> reader)
Adds a problem description reader with the specified name and
implementation to this launcher.
|
<T extends _ProblemReader> |
configProblemDescriptionReader(java.lang.String name,
java.lang.Class<T> reader,
boolean isDefault)
Adds a problem description reader with the specified name and
implementation to this launcher specifying if it is (
isDefault==true ) or not (isDefault==false ) the
default problem description reader for this launcher. |
void |
configStandardInputReader(_ProblemReader stdInputProblemReader)
Defines the reader used to parse a problem from standard input when
-i option is set. |
<T extends _Prover> |
configTheoremProver(java.lang.String name,
java.lang.Class<T> prover)
Adds to this launcher a theorem prover with the specified name and
implementation.
|
<T extends _Prover> |
configTheoremProver(java.lang.String name,
java.lang.Class<T> prover,
boolean isDefault)
Adds a theorem prover with the specified name and implementation to this
launcher specifying if it is (
isDefault==true ) or not (
isDefault==false ) the default prover for this launcher. |
org.apache.commons.cli.Options |
getCmdLineOptionsManager()
Returns the command line options manger used by this launcher.
|
Launcher.LaunchConfiguration |
getCurrentLauncherConfiguration()
Return an object describing the relevant details about the configuration of
the launcher.
|
ProofSearchData |
getLastProofSearchData()
Returns data about the last proof-search.
|
void |
launch()
Launches the prover.
|
void |
optConfigCmdLineOptions(org.apache.commons.cli.Options options)
Add the specified command options to the command line options for this
launcher.
|
void |
optConfigInputSyntax(java.lang.String str)
Defines the message the launcher prints before reading from standard input;
in general the message consists of a short description of the syntax of
input formulas.
|
void |
optConfigSingleExecutionConfigurator(_SingleExecutionConfigurator configurator) |
void |
optConfigWelcomeMessage(java.lang.String str)
Defines the message the launcher prints before prover execution; in general
the message consists of the name and the version of the launcher.
|
Launcher.LaunchConfiguration |
processCmdLineArguments(java.lang.String[] args)
Processes the command line arguments and defines the configuration of the
launcher; the method returns the object describing the essential details of
the current launcher configuration.
|
void |
setTraceGenerationMode(boolean flag)
If
flag is true the launcher invoke the engine in trace
execution mode. |
public void configLauncherName(java.lang.String launcherClassName)
launcherClassName
- the name of the class invoking this launcher.public <T extends _Prover> void configTheoremProver(java.lang.String name, java.lang.Class<T> prover) throws ProverDefinitionException
T
- the class of the proverprover
- the class implementing the provername
- the name of the proverProverDefinitionException
- if there is some problem with the added
prover.public <T extends _Prover> void configTheoremProver(java.lang.String name, java.lang.Class<T> prover, boolean isDefault) throws ProverDefinitionException
isDefault==true
) or not (
isDefault==false
) the default prover for this launcher. The
default prover is the last one for which this method is invoked with
isDefault==true
.T
- the class of the provername
- the name of the prover.prover
- the class implementing the prover.isDefault
- specify if this is the default prover for the launcher.ProverDefinitionException
- if there is some problem with the added
prover.public <T extends _ProblemReader> void configProblemDescriptionReader(java.lang.String name, java.lang.Class<T> reader) throws ReaderDefinitionException
T
- the class implementing the problem description readername
- the name of the readerreader
- the class implementing the readerReaderDefinitionException
- if there is some problem with the added
readerpublic <T extends _ProblemReader> void configProblemDescriptionReader(java.lang.String name, java.lang.Class<T> reader, boolean isDefault) throws ReaderDefinitionException
isDefault==true
) or not (isDefault==false
) the
default problem description reader for this launcher. The default reader is
the last one for which this method is invoked with
isDefault==true
.T
- the class implementing the problem description readername
- the name of the readerreader
- the class implementing the readerisDefault
- specify if this is the default reader for the launcherReaderDefinitionException
- if there is some problem with the added
readerpublic void configInitialNodeSetBuilder(_InitialGoalBuilder builder)
builder
- the initial node set builder.public void configStandardInputReader(_ProblemReader stdInputProblemReader)
-i
option is set.stdInputProblemReader
- the problem description reader for standard input.public void optConfigSingleExecutionConfigurator(_SingleExecutionConfigurator configurator)
public ProofSearchData getLastProofSearchData()
public org.apache.commons.cli.Options getCmdLineOptionsManager()
public Launcher.LaunchConfiguration getCurrentLauncherConfiguration()
public void launch() throws LauncherExecutionException, LauncherConfigurationException
LauncherExecutionException
- if processComdLineOptions has not been
executed before this method invocationLauncherConfigurationException
- if the current configuration cannot
be executedpublic Launcher.LaunchConfiguration processCmdLineArguments(java.lang.String[] args)
args
- the command line argumentspublic void optConfigCmdLineOptions(org.apache.commons.cli.Options options) throws LauncherConfigurationException
LauncherOptionDefinitionException
is
thrown.options
- the options to addLauncherOptionDefinitionException
- if one of the added options has a
name conflicting with one of the launcher optionsLauncherConfigurationException
public void setTraceGenerationMode(boolean flag)
flag
is true the launcher invoke the engine in trace
execution mode. Since trace execution mode is incompatible with verbose
execution mode if the current configuration is inconsistent an exception is
thrown.flag
- if true
the trace is generatedLauncherConfigurationException
- if the resulting configuration is
inconsistent.public void optConfigWelcomeMessage(java.lang.String str)
str
- the welcome message.public void optConfigInputSyntax(java.lang.String str)
str
- the welcome message.