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