Package com.microsoft.z3

Class FuncInterp.Entry<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.FuncInterp.Entry<R>

Enclosing class:

FuncInterp<R extends Sort>

public static class FuncInterp.Entry<R extends Sort>
extends Z3Object

An Entry object represents an element in the finite map used to encode a function interpretation.

Method Summary

Modifier and Type	Method	Description
Expr<?>[]	getArgs()	The arguments of the function entry.
int	getNumArgs()	The number of arguments of the entry.
Expr<R>	getValue()	Return the (symbolic) value of this entry.
String	toString()	A string representation of the function entry.

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

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

Method Details

getValue

public Expr<R> getValue()

Return the (symbolic) value of this entry.

Throws:

Z3Exception

Z3Exception - on error

getNumArgs

public int getNumArgs()

The number of arguments of the entry.

Throws:

Z3Exception - on error

getArgs

public Expr<?>[] getArgs()

The arguments of the function entry.

Throws:

Z3Exception

Z3Exception - on error

toString

public String toString()

A string representation of the function entry.

Overrides:

toString in class Object