Package com.microsoft.z3

Class FuncInterp<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.FuncInterp<R>

public class FuncInterp<R extends Sort>
extends Z3Object

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	FuncInterp.Entry<R extends Sort>	An Entry object represents an element in the finite map used to encode a function interpretation.

Method Summary

Modifier and Type	Method	Description
int	getArity()	The arity of the function interpretation
Expr<R>	getElse()	The (symbolic) `else' value of the function interpretation.
FuncInterp.Entry<R>[]	getEntries()	The entries in the function interpretation
int	getNumEntries()	The number of entries in the function interpretation.
String	toString()	A string representation of the function interpretation.

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

getNumEntries

public int getNumEntries()

The number of entries in the function interpretation.

Returns:

an int

Throws:

Z3Exception - on error

getEntries

public FuncInterp.Entry<R>[] getEntries()

The entries in the function interpretation

Throws:

Z3Exception

Z3Exception - on error

getElse

public Expr<R> getElse()

The (symbolic) `else' value of the function interpretation.

Returns:

an Expr

Throws:

Z3Exception

Z3Exception - on error

getArity

public int getArity()

The arity of the function interpretation

Returns:

an int

Throws:

Z3Exception - on error

toString

public String toString()

A string representation of the function interpretation.

Overrides:

toString in class Object