FuncInterp.Entry Class Reference

Inheritance diagram for FuncInterp.Entry:

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

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

inline

The arguments of the function entry.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 60 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 ( )

inline

The number of arguments of the entry.

Exceptions

Z3Exception

on error

Definition at line 49 of file FuncInterp.java.

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

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

Expr getValue ( )

inline

Return the (symbolic) value of this entry.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 39 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 73 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());
            }
        }