FuncInterp Class Reference

Inheritance diagram for FuncInterp:

Data Structures
class	Entry

Public Member Functions
int	getNumEntries ()
Entry[]	getEntries ()
Expr	getElse ()
int	getArity ()
String	toString ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize ()

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 25 of file FuncInterp.java.

Member Function Documentation

int getArity ( )

inline

The arity of the function interpretation

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 151 of file FuncInterp.java.

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

Expr getElse ( )

inline

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

Exceptions

Z3Exception
Z3Exception	on error

Returns

an Expr

Definition at line 140 of file FuncInterp.java.

Referenced by FuncInterp.toString().

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

Entry [] getEntries ( )

inline

The entries in the function interpretation

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 123 of file FuncInterp.java.

Referenced by FuncInterp.toString().

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

int getNumEntries ( )

inline

The number of entries in the function interpretation.

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 112 of file FuncInterp.java.

Referenced by FuncInterp.getEntries().

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

String toString ( )

inline

A string representation of the function interpretation.

Definition at line 159 of file FuncInterp.java.

    {
        try
        {
            String res = "";
            res += "[";
            for (Entry 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;
        } catch (Z3Exception e)
        {
            return new String("Z3Exception: " + e.getMessage());
        }
    }