de.uka.ilkd.key.symbolic_execution.object_model

Interface ISymbolicEquivalenceClass

All Superinterfaces:

ISymbolicElement

All Known Implementing Classes:

SymbolicEquivalenceClass, SymbolicLayoutReader.KeYlessEquivalenceClass

public interface ISymbolicEquivalenceClass
extends ISymbolicElement

An equivalence class which defines which Terms represent the same ISymbolicObject in an ISymbolicLayout.

Author:

Martin Hentschel

Method Summary

Modifier and Type	Method and Description
boolean	containsTerm(Term term) Checks if a Term is contained.
Term	getRepresentative() Returns the most representative term.
java.lang.String	getRepresentativeString() Returns the most representative term as human readable String.
ImmutableList<Term>	getTerms() Returns the terms which represents the same ISymbolicObject.
ImmutableList<java.lang.String>	getTermStrings() Returns the terms which represents the same ISymbolicObject as human readable String.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicElement

getSettings

Method Detail

getTerms

ImmutableList<Term> getTerms()

Returns the terms which represents the same ISymbolicObject.

Returns:

The terms which represents the same ISymbolicObject.

containsTerm

boolean containsTerm(Term term)

Checks if a Term is contained.

Parameters:

term - The Term to check.

Returns:

true Term is contained, false Term is not contained.

getTermStrings

ImmutableList<java.lang.String> getTermStrings()

Returns the terms which represents the same ISymbolicObject as human readable String.

Returns:

The terms which represents the same ISymbolicObject as human readable String.

getRepresentative

Term getRepresentative()

Returns the most representative term.

Returns:

The most representative term.

getRepresentativeString

java.lang.String getRepresentativeString()

Returns the most representative term as human readable String.

Returns:

The most representative term as human readable String.