Uses of Class
fmrisc.ProofNavigator.Proving.ProofState

Packages that use ProofState

Package	Description
fmrisc.ProofNavigator
fmrisc.ProofNavigator.Commands
fmrisc.ProofNavigator.Communication
fmrisc.ProofNavigator.Proving
fmrisc.ProofNavigator.SWT

Uses of ProofState in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return ProofState

Modifier and Type	Method and Description
static ProofState[]	State.getReplayChildren() Set children of current proof state during proof replay.

Methods in fmrisc.ProofNavigator with parameters of type ProofState

Modifier and Type	Method and Description
static void	Main.setProofState(ProofState state) Signal current proof state.
static void	State.setReplayChildren(ProofState[] children) Set children of current proof state during proof replay.

Uses of ProofState in fmrisc.ProofNavigator.Commands

Methods in fmrisc.ProofNavigator.Commands that return ProofState

Modifier and Type	Method and Description
ProofState[]	ProofCommand.process(ProofState state) process proof state.
ProofState[]	ProofCommandBase.process(ProofState state) process proof state (in environment denoted by that state).

Methods in fmrisc.ProofNavigator.Commands with parameters of type ProofState

Modifier and Type	Method and Description
ProofState[]	ProofCommand.process(ProofState state) process proof state.
ProofState[]	ProofCommandBase.process(ProofState state) process proof state (in environment denoted by that state).

Uses of ProofState in fmrisc.ProofNavigator.Communication

Methods in fmrisc.ProofNavigator.Communication with parameters of type ProofState

Modifier and Type	Method and Description
java.io.File	Presenter.getFile(ProofState state) Construct file name for proof state
java.io.File	Presenter.writeProofState(ProofState state) Write proof state and return corresponding file.

Uses of ProofState in fmrisc.ProofNavigator.Proving

Methods in fmrisc.ProofNavigator.Proving that return ProofState

Modifier and Type	Method and Description
ProofState[]	ProofState.getChildren() get children of proof state
ProofState	Proof.getCurrent() get current open proof state
ProofState	Proof.getOpenGoal() get open leaf goal
ProofState[]	Proof.getOpenGoals() get open leaf goals
ProofState	ProofState.getParent() get parent of proof state
ProofState	Proof.getRoot() get root of proof
ProofState	Formula.getState() Get proof state of formula.
ProofState	Proof.getState(java.lang.String tag) Get proof state with denoted tag.
static ProofState	Instantiating.instantiate(Formula formula) Extend proof state by instantiations of given formula
static ProofState	Instantiating.instantiate(Formula[] formulas) Extend proof state by instantiations of given formulas
static ProofState	Instantiating.instantiate(ProofState state) Extend given proof state by instantiations of quantified formulas.
static ProofState[]	ProofUtil.toProofStateArray(java.util.Vector<ProofState> v) converts vector v of ProofState objects to ProofState array

Methods in fmrisc.ProofNavigator.Proving with parameters of type ProofState

Modifier and Type	Method and Description
void	Proof.close(ProofState state) Inform proof that state was closed.
static GroundExpressions	GroundExpressions.compute(ProofState state) Compute collection of ground subexpressions of a proof state.
void	Proof.cut(ProofState state) Cut proof at denoted state.
void	ProofState.extend(Command command, ProofState[] children) command extends current state by adding and labeling children
void	Proof.extend(ProofState state, ProofState[] children) Inform proof that state was extended by children.
void	Proof.extend(ProofState state, ProofState[] children) Inform proof that state was extended by children.
static ProofState	Instantiating.instantiate(ProofState state) Extend given proof state by instantiations of quantified formulas.
boolean	Proof.redo(ProofState state) Redo proof at denoted state.
boolean	Proof.replay(ProofState state) Replay skeleton proof on proof state and its children.
void	ProofState.setChildren(Command command, ProofState[] children) set children of proof state
void	Proof.setCurrent(ProofState state) set current open proof state
void	ProofState.setParent(ProofState parent) set parent of proof state
static boolean	ProverReasoning.simplify(ProofState state, boolean hard, boolean generate) Simplify the current proof state and potentially close it.
static boolean	ProverReasoning.simplify(ProofState state, Formula formula, boolean hard) Simplify a single formula in some proof state.

Method parameters in fmrisc.ProofNavigator.Proving with type arguments of type ProofState

Modifier and Type	Method and Description
void	ProofState.addOpen(java.util.Vector<ProofState> vector) Add open state and all open children recursively to vector.
static ProofState[]	ProofUtil.toProofStateArray(java.util.Vector<ProofState> v) converts vector v of ProofState objects to ProofState array

Constructors in fmrisc.ProofNavigator.Proving with parameters of type ProofState

Constructor and Description
Formula(ProofState state, Expression formula, boolean isGoal) construct a formula from an expression
Formula(ProofState state, Formula formula) construct a copy of the given formula in the denoted state
ProofState(ProofState parent, Environment env) construct a proof state without path and formulas yet

Uses of ProofState in fmrisc.ProofNavigator.SWT

Methods in fmrisc.ProofNavigator.SWT that return ProofState

Modifier and Type	Method and Description
ProofState	ProofTreeItem.getState() Return proof state associated to item.

Methods in fmrisc.ProofNavigator.SWT with parameters of type ProofState

Modifier and Type	Method and Description
static void	ProofTreeItem.setNodes(org.eclipse.swt.widgets.Tree tree, ProofState root) Set tree to visualize the state tree with the denoted root state.
static void	MainSWT.setProofState(ProofState state) Signal current proof state.
void	Top.setProofState(ProofState state) Signal current proof state.