Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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 ()

Package Functions

 Entry (Context ctx, long obj) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) 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.


Constructor & Destructor Documentation

Entry ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 86 of file FuncInterp.java.

                {
                        super(ctx, obj);
                }

Member Function Documentation

void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 97 of file FuncInterp.java.

                {
                        getContext().funcEntry_DRQ().add(o);
                        super.decRef(o);
                }
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()));
                }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 91 of file FuncInterp.java.

                {
                        getContext().funcEntry_DRQ().incAndClear(getContext(), o);
                        super.incRef(o);
                }
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());
                        }
                }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines