FuncInterp Class Reference

Inheritance diagram for FuncInterp:

Data Structures
class	Entry

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

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

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 ( ) throws Z3Exception

inline

The arity of the function interpretation

Definition at line 141 of file FuncInterp.java.

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

Expr getElse ( ) throws Z3Exception

inline

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

Exceptions

Z3Exception

Definition at line 132 of file FuncInterp.java.

Referenced by FuncInterp.toString().

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

Entry [] getEntries ( ) throws Z3Exception

inline

The entries in the function interpretation

Exceptions

Z3Exception

Definition at line 117 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 ( ) throws Z3Exception

inline

The number of entries in the function interpretation.

Definition at line 107 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 149 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());
                }
        }