public class EngineState
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private AbbrevMap |
abbrevMap |
private java.util.Map<java.lang.String,java.lang.Object> |
arbitraryVariables |
private java.io.File |
baseFileName |
private boolean |
echoOn
If set to true, outputs all commands to observers and console.
|
private Goal |
goal |
private Node |
lastSetGoalNode |
private java.util.Observer |
observer
nullable
|
private static DefaultTermParser |
PARSER |
private Proof |
proof |
private ValueInjector |
valueInjector |
Constructor and Description |
---|
EngineState(Proof proof) |
Modifier and Type | Method and Description |
---|---|
private Goal |
findGoalFromRoot(Node rootNode,
boolean checkAutomatic) |
AbbrevMap |
getAbbreviations() |
java.io.File |
getBaseFileName() |
Goal |
getFirstOpenAutomaticGoal() |
Goal |
getFirstOpenGoal(boolean checkAutomatic)
Returns the first open goal, which has to be automatic iff checkAutomatic
is true.
|
protected static Goal |
getGoal(ImmutableList<Goal> openGoals,
Node node) |
int |
getMaxAutomaticSteps() |
java.util.Observer |
getObserver() |
Proof |
getProof() |
ValueInjector |
getValueInjector() |
private static Node |
goUpUntilOpen(Node start) |
boolean |
isEchoOn() |
void |
setBaseFileName(java.io.File baseFileName) |
void |
setEchoOn(boolean echoOn) |
void |
setGoal(Goal g) |
void |
setGoal(Node node) |
void |
setMaxAutomaticSteps(int steps) |
void |
setObserver(java.util.Observer observer) |
Sequent |
toSequent(java.lang.String sequent) |
Sort |
toSort(java.lang.String sortName) |
Term |
toTerm(java.lang.String string,
Sort sort) |
private static final DefaultTermParser PARSER
private final java.util.Map<java.lang.String,java.lang.Object> arbitraryVariables
private final Proof proof
private AbbrevMap abbrevMap
private java.util.Observer observer
private java.io.File baseFileName
private ValueInjector valueInjector
private Goal goal
private Node lastSetGoalNode
private boolean echoOn
public EngineState(Proof proof)
protected static Goal getGoal(ImmutableList<Goal> openGoals, Node node)
public void setGoal(Goal g)
public Proof getProof()
public Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException
checkAutomatic
- Set to true if the returned Goal
should be automatic.ScriptException
- If there is no such Goal
, or something else goes
wrong.public Goal getFirstOpenAutomaticGoal() throws ScriptException
Goal
.ScriptException
- If there is no such Goal
.public Term toTerm(java.lang.String string, Sort sort) throws ParserException, ScriptException
ParserException
ScriptException
public Sort toSort(java.lang.String sortName) throws ParserException, ScriptException
ParserException
ScriptException
public Sequent toSequent(java.lang.String sequent) throws ParserException, ScriptException
ParserException
ScriptException
public int getMaxAutomaticSteps()
public void setMaxAutomaticSteps(int steps)
public java.util.Observer getObserver()
public void setObserver(java.util.Observer observer)
public java.io.File getBaseFileName()
public void setBaseFileName(java.io.File baseFileName)
public ValueInjector getValueInjector()
public AbbrevMap getAbbreviations()
public void setGoal(Node node)
public boolean isEchoOn()
public void setEchoOn(boolean echoOn)