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

---

Constructor & Destructor Documentation

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

Definition at line 180 of file FuncInterp.java.

        {
                super(ctx, obj);
        }

---

Member Function Documentation

void decRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 191 of file FuncInterp.java.

        {
                getContext().funcInterp_DRQ().add(o);
                super.decRef(o);
        }

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

void incRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 185 of file FuncInterp.java.

        {
                getContext().funcInterp_DRQ().incAndClear(getContext(), o);
                super.incRef(o);
        }

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