Uses of Class
fmrisc.ProofNavigator.State.ProverVersion

Packages that use State.ProverVersion

Package	Description
fmrisc.ProgramExplorer
fmrisc.ProofNavigator
fmrisc.ProofNavigator.Proving
fmrisc.ProofNavigator.Proving.CVCL

Uses of State.ProverVersion in fmrisc.ProgramExplorer

Methods in fmrisc.ProgramExplorer that return State.ProverVersion

Modifier and Type	Method and Description
static State.ProverVersion	Main.proverVersion() Return version of default prover.

Uses of State.ProverVersion in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return State.ProverVersion

Modifier and Type	Method and Description
static State.ProverVersion	State.getProverVersion() get version of prover currently in use
static State.ProverVersion	State.ProverVersion.valueOf(java.lang.String name) Returns the enum constant of this type with the specified name.
static State.ProverVersion[]	State.ProverVersion.values() Returns an array containing the constants of this enum type, in the order they are declared.

Methods in fmrisc.ProofNavigator with parameters of type State.ProverVersion

Modifier and Type	Method and Description
static boolean	State.init(java.lang.String name, java.lang.String cvcl, State.ProverVersion version) Initialize prover state using denoted context.
static boolean	State.init(java.lang.String name, java.lang.String cvcl, State.ProverVersion version, boolean firstOrder, boolean toLogical) Initialize prover state using denoted context.
static void	Main.setProperties(java.lang.String context, java.lang.String cvcl, State.ProverVersion version, boolean firstOrder, boolean toLogical) Set various properties.

Uses of State.ProverVersion in fmrisc.ProofNavigator.Proving

Methods in fmrisc.ProofNavigator.Proving that return State.ProverVersion

Modifier and Type	Method and Description
State.ProverVersion	ProofState.proverVersion() get prover version of proof state

Methods in fmrisc.ProofNavigator.Proving with parameters of type State.ProverVersion

Modifier and Type	Method and Description
static Proof	Proof.newProof(FormulaSymbol symbol, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) Construct new proof for formula denoted by symbol.

Constructors in fmrisc.ProofNavigator.Proving with parameters of type State.ProverVersion

Constructor and Description
ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) construct a root state from a single goal and without assumptions

Uses of State.ProverVersion in fmrisc.ProofNavigator.Proving.CVCL

Methods in fmrisc.ProofNavigator.Proving.CVCL that return State.ProverVersion

Modifier and Type	Method and Description
State.ProverVersion	CVCL.getVersion() Get version of checker.

Methods in fmrisc.ProofNavigator.Proving.CVCL with parameters of type State.ProverVersion

Modifier and Type	Method and Description
static void	CVCLPrinter.print(State.ProverVersion version, AST tree, java.io.PrintWriter out) Print abstract syntax tree in CVCL syntax.
static java.lang.String	CVCLPrinter.toString(State.ProverVersion version, AST tree) Convert abstract syntax tree to CVCL syntax.

Constructors in fmrisc.ProofNavigator.Proving.CVCL with parameters of type State.ProverVersion

Constructor and Description
CVCL(java.lang.String command, State.ProverVersion version, java.io.PrintWriter log, boolean useMask) Create CVCL instance by call of command