Z3 |

Data Structures | Public Member Functions | Properties
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:

## Data Structures
class | DecRefQueue

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

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

76 {
77 uint n = NumArgs;
78 string res = "[";
79 Expr[] args = Args;
80 for (uint i = 0; i < n; i++)
81 res += args[i] + ", ";
82 return res + Value + "]";
83 }
Microsoft.Z3.FuncInterp.Entry.NumArgs
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:52
Microsoft.Z3.FuncInterp.Entry.Value
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:41
Microsoft.Z3.FuncInterp.Entry.Args
Expr[] Args
The arguments of the function entry.
Definition: FuncInterp.cs:60

## Property Documentation

## ◆ Args

Expr [] Args
| get

The arguments of the function entry.

Definition at line 59 of file FuncInterp.cs.

60 {
61 get
62 {
63
64 uint n = NumArgs;
65 Expr[] res = new Expr[n];
66 for (uint i = 0; i < n; i++)
67 res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
68 return res;
69 }
70 }

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.

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

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.

41 {
42 get
43 {
44 return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
45 }
46 }

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