FuncInterp< R extends Sort > Class Template Reference

Inheritance diagram for FuncInterp< R extends Sort >:

Data Structures
class	Entry

Public Member Functions
int	getNumEntries ()
Entry< R >[]	getEntries ()
Expr< R >	getElse ()
int	getArity ()
String	toString ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

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.

Definition at line 28 of file FuncInterp.java.

Member Function Documentation

getArity()

int getArity ( )

inline

The arity of the function interpretation

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 158 of file FuncInterp.java.

    {
        return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
    }

getElse()

Expr<R> getElse ( )

inline

The (symbolic) ‘else’ value of the function interpretation.

Exceptions

Z3Exception
Z3Exception	on error

Returns

an Expr

Definition at line 147 of file FuncInterp.java.

    {
        return (Expr<R>) Expr.create(getContext(),
                Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
    }

getEntries()

Entry<R> [] getEntries ( )

inline

The entries in the function interpretation

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 130 of file FuncInterp.java.

    {
        int n = getNumEntries();
        Entry<R>[] res = new Entry[n];
        for (int i = 0; i < n; i++)
            res[i] = new Entry<>(getContext(), Native.funcInterpGetEntry(getContext()
                    .nCtx(), getNativeObject(), i));
        return res;
    }

getNumEntries()

int getNumEntries ( )

inline

The number of entries in the function interpretation.

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 119 of file FuncInterp.java.

    {
        return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
    }

toString()

String toString ( )

inline

A string representation of the function interpretation.

Definition at line 166 of file FuncInterp.java.

    {
        String res = "";
        res += "[";
        for (Entry<R> e : getEntries())
        {
            int n = e.getNumArgs();
            if (n > 1)
                res += "[";
            Expr<?>[] args = e.getArgs();
            for (int i = 0; i < n; i++)
            {
                if (i != 0)
                    res += ", ";
                res += args[i];
            }
            if (n > 1)
                res += "]";
            res += " -> " + e.getValue() + ", ";
        }
        res += "else -> " + getElse();
        res += "]";
        return res;
    }