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