FuncInterp Class Reference

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.
More...

Inheritance diagram for FuncInterp:

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

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

Properties
uint	NumEntries [get]
	The number of entries in the function interpretation. More...
Entry[]	Entries [get]
	The entries in the function interpretation More...
Expr	Else [get]
	The (symbolic) ‘else’ value of the function interpretation. More...
uint	Arity [get]
	The arity of the function interpretation More...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object More...

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 29 of file FuncInterp.cs.

Member Function Documentation

ToString()

override string ToString ( )

inline

A string representation of the function interpretation.

Definition at line 151 of file FuncInterp.cs.

        {
            string res = "";
            res += "[";
            foreach (Entry e in Entries)
            {
                uint n = e.NumArgs;
                if (n > 1) res += "[";
                Expr[] args = e.Args;
                for (uint i = 0; i < n; i++)
                {
                    if (i != 0) res += ", ";
                    res += args[i];
                }
                if (n > 1) res += "]";
                res += " -> " + e.Value + ", ";
            }
            res += "else -> " + Else;
            res += "]";
            return res;
        }

Property Documentation

Arity

uint Arity

get

The arity of the function interpretation

Definition at line 143 of file FuncInterp.cs.

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

Else

Expr Else

get

The (symbolic) ‘else’ value of the function interpretation.

Definition at line 131 of file FuncInterp.cs.

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

Referenced by FuncInterp.ToString().

Entries

Entry [] Entries

get

The entries in the function interpretation

Definition at line 115 of file FuncInterp.cs.

        {
            get
            {
 
                uint n = NumEntries;
                Entry[] res = new Entry[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
                return res;
            }
        }

Referenced by FuncInterp.ToString().

NumEntries

uint NumEntries

get

The number of entries in the function interpretation.

Definition at line 107 of file FuncInterp.cs.

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