|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use ProofState | |
---|---|
fmrisc.Communication | |
fmrisc.ProofNavigator | |
fmrisc.ProofNavigator.Commands | |
fmrisc.ProofNavigator.SWT | |
fmrisc.Proving |
Uses of ProofState in fmrisc.Communication |
---|
Methods in fmrisc.Communication with parameters of type ProofState | |
---|---|
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 |
---|
Methods in fmrisc.ProofNavigator that return ProofState | |
---|---|
static ProofState[] |
State.getReplayChildren()
Set children of current proof state during proof replay. |
Methods in fmrisc.ProofNavigator with parameters of type ProofState | |
---|---|
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 | |
---|---|
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 | |
---|---|
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.SWT |
---|
Methods in fmrisc.ProofNavigator.SWT that return ProofState | |
---|---|
ProofState |
ProofTreeItem.getState()
Return proof state associated to item. |
Methods in fmrisc.ProofNavigator.SWT with parameters of type ProofState | |
---|---|
static void |
ProofTreeItem.setNodes(org.eclipse.swt.widgets.Tree tree,
ProofState root)
Set tree to visualize the state tree with the denoted root state. |
void |
Top.setProofState(ProofState state)
Signal current proof state. |
static void |
MainSWT.setProofState(ProofState state)
Signal current proof state. |
Uses of ProofState in fmrisc.Proving |
---|
Methods in fmrisc.Proving that return ProofState | |
---|---|
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 v)
converts vector v of ProofState objects to ProofState array |
Methods in fmrisc.Proving with parameters of type ProofState | |
---|---|
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. |
Constructors in fmrisc.Proving with parameters of type ProofState | |
---|---|
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 |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |