de.uka.ilkd.key.util.mergerule

Class SymbolicExecutionState

java.lang.Object

de.uka.ilkd.key.util.Pair<Term,Term>

de.uka.ilkd.key.util.mergerule.SymbolicExecutionState

public class SymbolicExecutionState
extends Pair<Term,Term>

A symbolic execution state is a pair of a symbolic state in form of a parallel update, and a path condition in form of a JavaDL formula.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private Node	correspondingNode

Fields inherited from class de.uka.ilkd.key.util.Pair

first, second

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionState(Term symbolicState, Term pathCondition)
SymbolicExecutionState(Term symbolicState, Term pathCondition, Node correspondingNode)

Method Summary

Modifier and Type	Method and Description
Node	getCorrespondingNode()
Term	getPathCondition()
Term	getSymbolicState()
private java.lang.String	rmN(java.lang.String str) Removes a trailing newline (\n) char from the given string.
void	setCorrespondingNode(Node correspondingNode)
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.util.Pair

equals, getFirstSet, getSecondSet, hashCode, toMap

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

correspondingNode

private Node correspondingNode

Constructor Detail

SymbolicExecutionState

public SymbolicExecutionState(Term symbolicState,
                              Term pathCondition)

Parameters:

symbolicState - The symbolic state (parallel update).

pathCondition - The path condition (formula).

SymbolicExecutionState

public SymbolicExecutionState(Term symbolicState,
                              Term pathCondition,
                              Node correspondingNode)

Parameters:

symbolicState - The symbolic state (parallel update).

pathCondition - The path condition (formula).

correspondingNode - The node corresponding to this SE state.

Method Detail

getSymbolicState

public Term getSymbolicState()

Returns:

The symbolic state.

getPathCondition

public Term getPathCondition()

Returns:

The path condition.

getCorrespondingNode

public Node getCorrespondingNode()

Returns:

The node corresponding to this SE state.

setCorrespondingNode

public void setCorrespondingNode(Node correspondingNode)

Parameters:

The - node corresponding to this SE state.

toString

public java.lang.String toString()

Overrides:

toString in class Pair<Term,Term>

rmN

private java.lang.String rmN(java.lang.String str)

Removes a trailing newline (\n) char from the given string.

Parameters:

str - The string to remove the newline char from.

Returns:

The given string with the removed trailing \n char, or the original string if it does not end with an \n.