public final class Main
extends java.lang.Object
Constructor and Description |
---|
Main() |
Modifier and Type | Method and Description |
---|---|
static boolean |
ask(java.lang.String question)
Ask question to be answered by user with 'y' or 'n'
|
static java.lang.String |
askText(java.lang.String question)
Prompt a question and read the answer.
|
static void |
displayDeclarations()
Signal that declarations are to be displayed.
|
static boolean |
displayGoal(Declaration[] decls,
FormulaDeclaration goal)
Display goal
|
static void |
exit(int code)
Terminate program with denoted exit code.
|
static java.lang.String |
getVersion()
Return version string.
|
static void |
init()
Initialize the system state.
|
static boolean |
isRunning()
Signal whether command is being processed.
|
static void |
main(java.lang.String[] args)
Command line interface to ProofNavigator.
|
static void |
mainInternal(Top top)
ProgramExplorer interface to ProofNavigator
|
static boolean |
newDeclaration(Declaration decl)
Signal new declaration.
|
static boolean |
open(java.lang.String path)
Read command from file with denoted path.
|
static Command |
parse()
Parse next command.
|
static Command |
parseString(java.lang.String string)
Parse string as command.
|
static void |
proofDone(Proof proof)
Signal that proof is completed.
|
static void |
quit()
Quit (session or current proof) after asking user whether to do so.
|
static java.lang.String |
readLine()
Read line of input from console.
|
static int |
readNumber(java.lang.String prompt,
int a,
int b)
Ask user for a number in the range a..b.
|
static void |
resetProof()
Signal there is no current proof.
|
static void |
run()
Run ProofNavigator interpreter.
|
static boolean |
setContext(java.lang.String path)
Set context directory.
|
static void |
setProof(Proof proof)
Signal current proof.
|
static void |
setProofState(ProofState state)
Signal current proof state.
|
static void |
setProperties(java.lang.String context,
java.lang.String cvcl,
State.ProverVersion version,
boolean firstOrder,
boolean toLogical)
Set various properties.
|
public static void main(java.lang.String[] args)
args
- command line arguments (call with "--help" to see which)public static void mainInternal(Top top)
top
- the Top instance used by the ProgramExplorerpublic static java.lang.String getVersion()
public static void init()
public static void run()
public static Command parse()
public static Command parseString(java.lang.String string)
string
- the string to be passed.public static void exit(int code)
code
- the exit codepublic static void quit()
public static java.lang.String readLine()
public static java.lang.String askText(java.lang.String question)
question
- the question.public static int readNumber(java.lang.String prompt, int a, int b)
prompt
- the message printed for asking.a
- the lower bound of the number.b
- the upper bound of the number.public static boolean ask(java.lang.String question)
question
- the question askedpublic static void setProof(Proof proof)
proof
- the current proofpublic static void resetProof()
public static void setProofState(ProofState state)
state
- the current proof state.public static boolean newDeclaration(Declaration decl)
decl
- the new declaration.public static boolean displayGoal(Declaration[] decls, FormulaDeclaration goal)
decls
- the declaration list.goal
- the goal declaration.public static void displayDeclarations()
public static boolean open(java.lang.String path)
path
- the (absolute or relative) path to the file.public static boolean setContext(java.lang.String path)
path
- the (absolute or relative) path to context directory
(if null, a default path is used).public static boolean isRunning()
public static void proofDone(Proof proof)
proof
- the completed proof.public static void setProperties(java.lang.String context, java.lang.String cvcl, State.ProverVersion version, boolean firstOrder, boolean toLogical)
context
- the context directory.cvcl
- the prover command path.version
- the prover version.firstOrder
- true if logic is first ordertoLogical
- true if formula type is LOGICAL.