de.uka.ilkd.key.smt

Class FunValueQuery

java.lang.Object

de.uka.ilkd.key.smt.AbstractQuery

de.uka.ilkd.key.smt.FunValueQuery

All Implemented Interfaces:

Query

class FunValueQuery
extends AbstractQuery

Query for finding out the value of a function(classinvariant or model field) for an object in a heap.

Author:

mihai

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	functionID
private java.lang.String	heapID
private java.lang.String	objectId

Fields inherited from class de.uka.ilkd.key.smt.AbstractQuery

result

Fields inherited from interface de.uka.ilkd.key.smt.Query

SELECT_ID

Constructor Summary

Constructors

Constructor and Description
FunValueQuery(java.lang.String objectId, java.lang.String heapID, java.lang.String functionID)

Method Summary

Modifier and Type	Method and Description
java.lang.String	getFunctionID()
java.lang.String	getHeapID()
java.lang.String	getObjectID()
java.lang.String	getQuery()
void	setResult(java.lang.String s) Stores the result from the z3 solver.

Methods inherited from class de.uka.ilkd.key.smt.AbstractQuery

echo, enclose, getResult, getVal

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

objectId

private java.lang.String objectId

heapID

private java.lang.String heapID

functionID

private java.lang.String functionID

Constructor Detail

FunValueQuery

public FunValueQuery(java.lang.String objectId,
                     java.lang.String heapID,
                     java.lang.String functionID)

Method Detail

getObjectID

public java.lang.String getObjectID()

getHeapID

public java.lang.String getHeapID()

getFunctionID

public java.lang.String getFunctionID()

getQuery

public java.lang.String getQuery()

setResult

public void setResult(java.lang.String s)

Description copied from interface: Query

Stores the result from the z3 solver.

Specified by:

setResult in interface Query

Overrides:

setResult in class AbstractQuery

Parameters:

s - the result to set