public final class StateProblem
extends java.lang.Object
Constructor and Description |
---|
StateProblem(Declaration[] decls,
Formula goal,
java.util.Map<Symbol,Symbol> map,
StateType stateType,
Type stringType,
java.util.Collection<VariableSymbol> variables,
java.util.Collection<ClassSymbol> exceptions,
ErrorStream out)
Construct a proving problem.
|
Modifier and Type | Method and Description |
---|---|
ClassicalProblem |
classicalProblem()
Translate the task into a predicate logic proving task.
|
void |
print(java.io.PrintWriter out)
Print task to output stream.
|
public StateProblem(Declaration[] decls, Formula goal, java.util.Map<Symbol,Symbol> map, StateType stateType, Type stringType, java.util.Collection<VariableSymbol> variables, java.util.Collection<ClassSymbol> exceptions, ErrorStream out)
decls
- the declarations of entities referenced in the goal.goal
- the goal to be proved.map
- a map of type symbols to new type symbolsstateType
- the current state type (null, if no state)stringType
- the string typevariables
- the modifiable variablesexceptions
- the throwable exceptionsout
- a stream for printing messagespublic void print(java.io.PrintWriter out)
out
- the stream to print topublic ClassicalProblem classicalProblem()