public class TCCGenerator
extends java.lang.Object
Constructor and Description |
---|
TCCGenerator(TheorySymbol tsymbol,
java.util.Vector<TheorySymbol> theories,
LogicEnvironment env,
java.io.File parent,
ErrorStream out)
Construct a type checking condition generator.
|
Modifier and Type | Method and Description |
---|---|
void |
abort()
Return to the parent context discarding all the assumptions and tasks
that were added to the subcontext since the last call of open().
|
void |
addTasks(TaskFolder folder)
Add generated tasks to task folder and reset state.
|
void |
assume(Formula formula)
Create an assumption.
|
void |
commit()
Return to the parent context and add to it all the tasks that were
created since the last call of open().
|
int |
getDepth()
Return depth of context stack.
|
void |
open()
Open a new subcontext.
|
void |
prove(java.lang.String name,
SourcePosition position,
Formula formula,
StateType resultType,
Name[] stateVars,
Name[] stateExcs)
Create a new task to prove the given formula.
|
java.io.File |
setDirectory(java.io.File parent)
Set new parent directory for generating task directories.
|
public TCCGenerator(TheorySymbol tsymbol, java.util.Vector<TheorySymbol> theories, LogicEnvironment env, java.io.File parent, ErrorStream out)
tsymbol
- the theory in which the tcc generator operates.theories
- the list of all theories referenced in dependence order.env
- the environment holding the referenced declarationsparent
- the directory used to create subdirectories for tcc tasksout
- a stream for printing messagespublic java.io.File setDirectory(java.io.File parent)
parent
- the new parent directory.public void addTasks(TaskFolder folder)
folder
- the folder to add the tasks to.public void assume(Formula formula)
formula
- the formula representing the assumption.public void prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs)
name
- the name of the taskposition
- a related source position (may be null)formula
- the formula to be provedresultType
- the current result type (null, if none)stateVars
- the current state vars (null, if none)stateExcs
- the current state exceptions (null, if none)public void open()
public void abort()
public void commit()
public int getDepth()