fmrisc.ProofNavigator

Class State

java.lang.Object

fmrisc.ProofNavigator.State

public final class State
extends java.lang.Object

Execution context for the proof navigator.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	State.ProverVersion

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	NamespacePrefix
static java.lang.String	NamespaceURI
static java.lang.String	OMDocPrefix
static java.lang.String	OMDocURI
static java.lang.String	OpenMathPrefix
static java.lang.String	OpenMathURI
static java.lang.String	XMLPrefix
static java.lang.String	XMLURI

Constructor Summary

Constructors

Constructor and Description
State()

Method Summary

Modifier and Type	Method and Description
static boolean	booleanAsLogical() Is type BOOLEAN externally represented as LOGICAL (and type BIT as BOOLEAN)?
static boolean	firstOrderCheck() Are value types to be checked to be first-order?
static Context	getContext() get context used by proof navigator
static java.io.File	getContextDir() Get current context directory.
static Environment	getEnvironment() get environment used by proof navigator
static java.lang.String	getError() get error message set
static java.util.Stack<java.io.File>	getFileStack() Get file stack.
static CVCLFormulaMask	getFormulaMask() Get formula mask.
static Environment	getGlobal() get global environment of proof navigator
static boolean	getLabels() ask whether lexer shall produce labels rather than idents
static Expression	getLastTCC() get last type checking condition
static PNLexer	getLexer() get lexer used by proof navigator
static Presenter	getPresenter() Get current presenter.
static Proof	getProof() get current proof
static Prover	getProver() get prover currently in use
static java.io.PrintWriter	getProverLog() Get prover log
static State.ProverVersion	getProverVersion() get version of prover currently in use
static java.util.Stack<java.io.BufferedReader>	getReaderStack() Get reader stack.
static ProofState[]	getReplayChildren() Set children of current proof state during proof replay.
static Prover	getRunningProver() Get prover currently running.
static int	getServerPort() Get server port.
static Store	getStore() Get current store.
static java.io.BufferedReader	getSystemIn() get standard input stream
static java.io.PrintWriter	getSystemOut() get standard output stream
static boolean	init(java.lang.String name, java.lang.String cvcl, State.ProverVersion version) Initialize prover state using denoted context.
static boolean	init(java.lang.String name, java.lang.String cvcl, State.ProverVersion version, boolean firstOrder, boolean toLogical) Initialize prover state using denoted context.
static boolean	isAborted() Get prover abort state.
static Prover	newProver(java.io.PrintWriter log, int timeout, boolean mask) get new instance of a prover
static void	resetError() reset error message
static void	restoreOldProver() Restore old prover.
static void	setAborted(boolean aborted) Set prover abort state.
static void	setAutoSimplify(boolean on) Turn on/off automatic simplification
static void	setBigFont(boolean big) Set font size.
static void	setBooleanAsLogical(boolean value) Turn on/off whether BOOLEAN is externally represented as LOGICAL.
static boolean	setContextDir(java.io.File dir) Set context directory to denoted directory (creating it, if necessary).
static void	setEnvironment(Environment env) set environment used by proof navigator
static void	setError(java.lang.String error) set error message, does not override previously set message
static void	setFirstOrderCheck(boolean value) Turn on/off whether value types to be checked to be first-order?
static void	setFormulaMask(CVCLFormulaMask mask) Set formula mask.
static void	setLabels(boolean signal) signal that lexer shall produce labels rather than idents
static void	setLastTCC(Expression tcc) set last type checking condition
static void	setLexer(PNLexer lexer) set lexer used by proof navigator
static void	setNewProver() Set new prover.
static void	setProof(Proof proof) set current proof
static void	setReplayChildren(ProofState[] children) Set children of current proof state during proof replay.
static void	setRunningProver(Prover prover) Set prover currently running.
static void	setServerPort(int port) Set server port.
static void	setSystemIn(java.io.BufferedReader in) set standard input stream
static void	setSystemOut(java.io.PrintWriter out) set standard output stream
static void	skipNL() Skip new line from input stream
static boolean	useAutoSimplify() Is automatic simplification used?
static boolean	useBigFont() Get font size.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

NamespacePrefix

public static final java.lang.String NamespacePrefix

See Also:

Constant Field Values

NamespaceURI

public static final java.lang.String NamespaceURI

See Also:

Constant Field Values

OpenMathPrefix

public static final java.lang.String OpenMathPrefix

See Also:

Constant Field Values

OpenMathURI

public static final java.lang.String OpenMathURI

See Also:

Constant Field Values

OMDocPrefix

public static final java.lang.String OMDocPrefix

See Also:

Constant Field Values

OMDocURI

public static final java.lang.String OMDocURI

See Also:

Constant Field Values

XMLPrefix

public static final java.lang.String XMLPrefix

See Also:

Constant Field Values

XMLURI

public static final java.lang.String XMLURI

See Also:

Constant Field Values

Constructor Detail

State

public State()

Method Detail

init

public static boolean init(java.lang.String name,
                           java.lang.String cvcl,
                           State.ProverVersion version)

Initialize prover state using denoted context.

Parameters:

name - the name (path) of the context (if null, default name is used)

cvcl - the name (path) to the prover executable (if null, default name and type is used)

version - the version of the prover used (ignored, if cvcl is null)

Returns:

true iff everything went okay

init

public static boolean init(java.lang.String name,
                           java.lang.String cvcl,
                           State.ProverVersion version,
                           boolean firstOrder,
                           boolean toLogical)

Initialize prover state using denoted context.

Parameters:

name - the name (path) of the context (if null, default name is used)

cvcl - the name (path) to the prover executable (if null, default name and type is used)

version - the version of the prover used (ignored, if cvcl is null)

firstOrder - true, if logic is first order (must be true for CVCL)

toLogical - true, if formula type is LOGICAL

Returns:

true iff everything went okay

getContextDir

public static java.io.File getContextDir()

Get current context directory.

Returns:

the current context directory.

setContextDir

public static boolean setContextDir(java.io.File dir)

Set context directory to denoted directory (creating it, if necessary).

Parameters:

dir - directory where all generated files are stored.

Returns:

true iff directory exists or can be generated and is writable

newProver

public static Prover newProver(java.io.PrintWriter log,
                               int timeout,
                               boolean mask)

get new instance of a prover

Parameters:

log - stream for prover to write log messages to (null, if none)

timeout - timeout for prover in seconds (0, if none)

mask - true iff quantified formulas are to be masked

Returns:

a new prover instance

getSystemOut

public static java.io.PrintWriter getSystemOut()

get standard output stream

Returns:

standard output stream used by system

setSystemOut

public static void setSystemOut(java.io.PrintWriter out)

set standard output stream

Parameters:

out - standard output stream used by system

getSystemIn

public static java.io.BufferedReader getSystemIn()

get standard input stream

Returns:

standard input stream used by system

setSystemIn

public static void setSystemIn(java.io.BufferedReader in)

set standard input stream

Parameters:

in - standard input stream used by system

skipNL

public static void skipNL()

Skip new line from input stream

setLastTCC

public static void setLastTCC(Expression tcc)

set last type checking condition

Parameters:

tcc - the type checking condition generated last

getLastTCC

public static Expression getLastTCC()

get last type checking condition

Returns:

the type checking condition generated last

setLexer

public static void setLexer(PNLexer lexer)

set lexer used by proof navigator

Parameters:

lexer - used by the proof navigator

getLexer

public static PNLexer getLexer()

get lexer used by proof navigator

Returns:

lexer used by proof navigator

setLabels

public static void setLabels(boolean signal)

signal that lexer shall produce labels rather than idents

Parameters:

signal - true iff lexer shall produce labels

getLabels

public static boolean getLabels()

ask whether lexer shall produce labels rather than idents

Returns:

true ff lexer shall produce labels

setError

public static void setError(java.lang.String error)

set error message, does not override previously set message

Parameters:

error - the error message

resetError

public static void resetError()

reset error message

getError

public static java.lang.String getError()

get error message set

Returns:

the error message (null if none set)

setEnvironment

public static void setEnvironment(Environment env)

set environment used by proof navigator

Parameters:

env - environment to be used by proof navigator

getEnvironment

public static Environment getEnvironment()

get environment used by proof navigator

Returns:

environment used by proof navigator

getGlobal

public static Environment getGlobal()

get global environment of proof navigator

Returns:

flobal environment of proof navigator

getContext

public static Context getContext()

get context used by proof navigator

Returns:

context used by proof navigator

getProver

public static Prover getProver()

get prover currently in use

Returns:

prover currently in use

getProverVersion

public static State.ProverVersion getProverVersion()

get version of prover currently in use

Returns:

version of the prover currently in use

setNewProver

public static void setNewProver()

Set new prover.

restoreOldProver

public static void restoreOldProver()

Restore old prover.

setRunningProver

public static void setRunningProver(Prover prover)

Set prover currently running.

Parameters:

prover - currently running prover.

getRunningProver

public static Prover getRunningProver()

Get prover currently running.

Returns:

prover currently running.

setProof

public static void setProof(Proof proof)

set current proof

Parameters:

proof - proof currently under development (null, if none)

getProof

public static Proof getProof()

get current proof

Returns:

proof currently under development (null, if none)

getStore

public static Store getStore()

Get current store.

Returns:

current store.

getPresenter

public static Presenter getPresenter()

Get current presenter.

Returns:

current presenter.

getProverLog

public static java.io.PrintWriter getProverLog()

Get prover log

Returns:

the log file

getFileStack

public static java.util.Stack<java.io.File> getFileStack()

Get file stack.

Returns:

the stack.

getReaderStack

public static java.util.Stack<java.io.BufferedReader> getReaderStack()

Get reader stack.

Returns:

the stack.

getFormulaMask

public static CVCLFormulaMask getFormulaMask()

Get formula mask.

Returns:

the formula mask.

setFormulaMask

public static void setFormulaMask(CVCLFormulaMask mask)

Set formula mask.

Parameters:

mask - the formula mask.

setServerPort

public static void setServerPort(int port)

Set server port.

Parameters:

port - the port used by the command server

getServerPort

public static int getServerPort()

Get server port.

Returns:

the port used by the command server

setAborted

public static void setAborted(boolean aborted)

Set prover abort state.

Parameters:

aborted - true if the prover has been aborted.

isAborted

public static boolean isAborted()

Get prover abort state.

Returns:

true if the prover has been aborted.

setBigFont

public static void setBigFont(boolean big)

Set font size.

Parameters:

big - true iff big fonts are to be displayed.

useBigFont

public static boolean useBigFont()

Get font size.

Returns:

true if big fonts are to be displayed.

setReplayChildren

public static void setReplayChildren(ProofState[] children)

Set children of current proof state during proof replay.

Parameters:

children - the children states (null, if none).

getReplayChildren

public static ProofState[] getReplayChildren()

Set children of current proof state during proof replay.

Returns:

the children (null, if none).

setAutoSimplify

public static void setAutoSimplify(boolean on)

Turn on/off automatic simplification

Parameters:

on - true iff automatic simplification is turned on.

useAutoSimplify

public static boolean useAutoSimplify()

Is automatic simplification used?

Returns:

true iff automatic simplification is used.

firstOrderCheck

public static boolean firstOrderCheck()

Are value types to be checked to be first-order?

Returns:

true iff value types are to be checked to be first-order.

booleanAsLogical

public static boolean booleanAsLogical()

Is type BOOLEAN externally represented as LOGICAL (and type BIT as BOOLEAN)?

Returns:

true iff BOOLEAN is externally represented as LOGICAL.

setFirstOrderCheck

public static void setFirstOrderCheck(boolean value)

Turn on/off whether value types to be checked to be first-order?

Parameters:

value - true iff value types are to be checked to be first-order.

setBooleanAsLogical

public static void setBooleanAsLogical(boolean value)

Turn on/off whether BOOLEAN is externally represented as LOGICAL.

Parameters:

value - true iff BOOLEAN is to be externally represented as LOGICAL.