FuncInterp.Entry Class Reference

An Entry object represents an element in the finite map used to encode a function interpretation. More...

Inheritance diagram for FuncInterp.Entry:

Public Member Functions
override string	ToString ()
	A string representation of the function entry. More...
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
Expr	Value [get]
	Return the (symbolic) value of this entry. More...
uint	NumArgs [get]
	The number of arguments of the entry. More...
Expr[]	Args [get]
	The arguments of the function entry. More...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object More...

Detailed Description

An Entry object represents an element in the finite map used to encode a function interpretation.

Definition at line 35 of file FuncInterp.cs.

Member Function Documentation

ToString()

override string ToString ( )

inline

A string representation of the function entry.

Definition at line 75 of file FuncInterp.cs.

            {
                uint n = NumArgs;
                string res = "[";
                Expr[] args = Args;
                for (uint i = 0; i < n; i++)
                    res += args[i] + ", ";
                return res + Value + "]";
            }

Property Documentation

Args

Expr [] Args

get

The arguments of the function entry.

Definition at line 59 of file FuncInterp.cs.

            {
                get
                {
 
                    uint n = NumArgs;
                    Expr[] res = new Expr[n];
                    for (uint i = 0; i < n; i++)
                        res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
                    return res;
                }
            }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().

NumArgs

uint NumArgs

get

The number of arguments of the entry.

Definition at line 51 of file FuncInterp.cs.

            {
                get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
            }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().

Value

Expr Value

get

Return the (symbolic) value of this entry.

Definition at line 40 of file FuncInterp.cs.

            {
                get
                {
                    return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
                }
            }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().