FuncInterp.Entry Class Reference

Inheritance diagram for FuncInterp.Entry:

Public Member Functions
Expr	getValue () throws Z3Exception
int	getNumArgs () throws Z3Exception
Expr[]	getArgs () 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

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

Definition at line 31 of file FuncInterp.java.

Member Function Documentation

Expr [] getArgs ( ) throws Z3Exception

inline

The arguments of the function entry.

Exceptions

Z3Exception

Definition at line 57 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

                {
                        int n = getNumArgs();
                        Expr[] res = new Expr[n];
                        for (int i = 0; i < n; i++)
                                res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
                                                getContext().nCtx(), getNativeObject(), i));
                        return res;
                }

int getNumArgs ( ) throws Z3Exception

inline

The number of arguments of the entry.

Definition at line 47 of file FuncInterp.java.

Referenced by FuncInterp.Entry.getArgs(), and FuncInterp.Entry.toString().

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

Expr getValue ( ) throws Z3Exception

inline

Return the (symbolic) value of this entry.

Exceptions

Z3Exception

Definition at line 38 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

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

String toString ( )

inline

A string representation of the function entry.

Definition at line 70 of file FuncInterp.java.

                {
                        try
                        {
                                int n = getNumArgs();
                                String res = "[";
                                Expr[] args = getArgs();
                                for (int i = 0; i < n; i++)
                                        res += args[i] + ", ";
                                return res + getValue() + "]";
                        } catch (Z3Exception e)
                        {
                                return new String("Z3Exception: " + e.getMessage());
                        }
                }