public final class ProofState
extends java.lang.Object
Constructor and Description |
---|
ProofState(Proof proof)
Construct a skeleton proof state
(all fields but the proof remain uninitialized).
|
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
|
ProofState(ProofState parent,
Environment env)
construct a proof state without path and formulas yet
|
Modifier and Type | Method and Description |
---|---|
Formula[] |
add(Formula[] formulas,
Formula formula)
Adds a formula to a sequence of formulas in this state.
|
Formula[] |
add(Formula[] formulas,
Formula[] formulas0)
Adds a sequence of formulas to a sequence of formulas in this state.
|
void |
addOpen(java.util.Vector<ProofState> vector)
Add open state and all open children recursively to vector.
|
void |
close(java.lang.String reason)
close the state.
|
Formula[] |
copy(Formula[] formulas)
Copy a sequence of formulas in this state.
|
void |
extend(Command command,
ProofState[] children)
command extends current state by adding and labeling children
|
boolean |
firstOrder()
is prover first order?
|
Formula |
getAssumption(java.lang.String label)
returns assumption with denoted label
|
Formula[] |
getAssumptions()
get assumptions of proof state
|
Formula[] |
getAxioms()
get axioms of proof state
|
ProofState[] |
getChildren()
get children of proof state
|
Command |
getCommand()
get command of proof state
|
Expression[] |
getCounterExample()
Get counterexample for state.
|
Environment |
getEnvironment()
get environment of proof state
|
Formula |
getFormula(java.lang.String label)
returns formula (assumption or goal) with denoted label
|
Formula |
getGoal(java.lang.String label)
returns goal with denoted label
|
Formula[] |
getGoals()
get goals of proof state
|
java.lang.String |
getLabel()
return label of proof state
|
ProofStateListener |
getListener()
Get listener that is notified when proof state has changed.
|
ProofState |
getParent()
get parent of proof state
|
java.lang.String |
getPath()
get path of proof state
|
Proof |
getProof()
get proof to which proof state belong
|
UniqueNameTable |
getSkolemTable()
Get unique name table to be used for creating skolemization constants.
|
void |
hasChanged(boolean file)
Signal that state has changed updating presentation of this state.
|
boolean |
isClosed()
check whether proof state is closed
|
void |
labelChildren()
Label the children of the current state.
|
void |
open()
open the state.
|
void |
print(java.io.PrintWriter out)
print proof state on output stream
|
void |
print(java.io.PrintWriter out,
int level)
Print proof state including children.
|
State.ProverVersion |
proverVersion()
get prover version of proof state
|
void |
redo()
Redo the proof at the denoted state (if possible)
|
Formula[] |
remove(Formula[] formulas,
Formula formula)
Remove a formula from a sequence of formulas in this state.
|
Formula[] |
replace(Formula[] formulas,
Formula formula,
Formula rformula)
Replace a formula in a sequence of formulas in this state.
|
void |
setAssumptions(Formula[] formulas)
set assumptions of proof state
|
void |
setAutoSimplify(boolean on)
Set automatic simplification status of proof state
|
void |
setAxioms(Formula[] formulas)
Set axioms of proof state.
|
void |
setChildren(Command command,
ProofState[] children)
set children of proof state
|
void |
setCommand(Command command)
set command of proof state
|
void |
setCounterExample(Expression[] formulas)
Set counterexample for state.
|
void |
setEnvironment(Environment env)
set environment of proof state
|
void |
setGoals(Formula[] formulas)
set goals of proof state
|
void |
setListener(ProofStateListener listener)
Set listener that is notified when proof state has changed.
|
void |
setParent(ProofState parent)
set parent of proof state
|
void |
setPath(java.lang.String path)
set path of proof state
|
boolean |
simplify(boolean hard)
simplify the current proof state and potentially close it.
|
boolean |
toLogical()
is conversion BOOLEAN to LOGICAL to be applied?
|
boolean |
useAutoSimplify()
get automatic simplification status of proof state
|
public ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical)
proof
- the proof to which the state belongsenv
- the environment in which all constants are declaredgoal
- the goal formulaautoSimplify
- true iff automatic simplification is on in stateproverVersion
- the version of the prover used in simplificationfirstOrder
- is prover first order?toLogical
- is conversion boolean to logical to be applied?public ProofState(ProofState parent, Environment env)
parent
- the parent stateenv
- the environment in which all constants are declaredpublic ProofState(Proof proof)
proof
- the proof to which the state shall belong.public java.lang.String getLabel()
public Proof getProof()
public java.lang.String getPath()
public void setPath(java.lang.String path)
path
- the path of the state (must be unique in the current proof)public ProofState getParent()
public void setParent(ProofState parent)
parent
- the parent of the statepublic Environment getEnvironment()
public void setEnvironment(Environment env)
env
- the environment.public Formula[] getAxioms()
public void setAxioms(Formula[] formulas)
formulas
- the axioms of the statepublic Formula[] getAssumptions()
public void setAssumptions(Formula[] formulas)
formulas
- the assumptions of the statepublic Formula[] getGoals()
public void setGoals(Formula[] formulas)
formulas
- the goals of the statepublic Expression[] getCounterExample()
public void setCounterExample(Expression[] formulas)
formulas
- sequence of formulas interpreted as a conjunction.public Command getCommand()
public void setCommand(Command command)
command
- the command applied to the proof statepublic boolean useAutoSimplify()
public State.ProverVersion proverVersion()
public boolean firstOrder()
public boolean toLogical()
public void setAutoSimplify(boolean on)
on
- true iff automatic simplification is to be switched onpublic ProofState[] getChildren()
public void setChildren(Command command, ProofState[] children)
command
- the command that generated the childrenchildren
- the new children of the statepublic Formula getAssumption(java.lang.String label)
label
- the labelpublic Formula getGoal(java.lang.String label)
label
- the labelpublic Formula getFormula(java.lang.String label)
label
- the labelpublic UniqueNameTable getSkolemTable()
public void setListener(ProofStateListener listener)
listener
- the listener that is notified.public ProofStateListener getListener()
public void hasChanged(boolean file)
file
- true iff also presentation on file is to be changed.public void print(java.io.PrintWriter out)
out
- the stream on which to print the formulapublic void close(java.lang.String reason)
reason
- explanation why state is closed.public void open()
public void redo()
public void labelChildren()
public void extend(Command command, ProofState[] children)
command
- the command extending the statechildren
- the children of the proof statepublic boolean isClosed()
public boolean simplify(boolean hard)
hard
- true iff hard (and time-consuming) simplification is tried.public Formula[] copy(Formula[] formulas)
formulas
- a sequence of formulaspublic Formula[] add(Formula[] formulas, Formula formula)
formulas
- a sequence of formulasformula
- a formula belonging to this statepublic Formula[] add(Formula[] formulas, Formula[] formulas0)
formulas
- a sequence of formulasformulas0
- a sequence of formulas belonging to this statepublic Formula[] remove(Formula[] formulas, Formula formula)
formulas
- a sequence of formulasformula
- a formula occuring in that sequence oncepublic Formula[] replace(Formula[] formulas, Formula formula, Formula rformula)
formulas
- a sequence of formulasformula
- a formula occuring in that sequence oncerformula
- a formula belonging to this statepublic void print(java.io.PrintWriter out, int level)
out
- the stream to print the state to.level
- the level of the proof state (0 = root).public void addOpen(java.util.Vector<ProofState> vector)
vector
- vector receiving all open proof states.