public class SymbolicExecutionStateWithProgCnt extends Triple<Term,Term,Term>
Constructor and Description |
---|
SymbolicExecutionStateWithProgCnt(Term symbolicState,
Term pathCondition,
Term programCounter) |
SymbolicExecutionStateWithProgCnt(Term symbolicState,
Term pathCondition,
Term programCounter,
Node correspondingNode) |
Modifier and Type | Method and Description |
---|---|
Node |
getCorrespondingNode() |
Term |
getPathCondition() |
Term |
getProgramCounter() |
Term |
getSymbolicState() |
void |
setCorrespondingNode(Node correspondingNode) |
java.lang.String |
toString() |
SymbolicExecutionState |
toSymbolicExecutionState() |
public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, Term programCounter)
symbolicState
- The symbolic state (parallel update).pathCondition
- The path condition (formula).programCounter
- The program counter: Formula with non-empty Java block and
post condition as only sub term.public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, Term programCounter, Node correspondingNode)
symbolicState
- The symbolic state (parallel update).pathCondition
- The path condition (formula).programCounter
- The program counter: Formula with non-empty Java block and
post condition as only sub term.correspondingNode
- The node corresponding to this SE state.public Term getSymbolicState()
public Term getPathCondition()
public Term getProgramCounter()
public Node getCorrespondingNode()
public void setCorrespondingNode(Node correspondingNode)
The
- node corresponding to this SE state.public SymbolicExecutionState toSymbolicExecutionState()
Copyright © 2003-2019 The KeY-Project.