Z3 |

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

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

165 {
166 string res = "";
167 res += "[";
168 foreach (Entry e in Entries)
169 {
170 uint n = e.NumArgs;
171 if (n > 1) res += "[";
172 Expr[] args = e.Args;
173 for (uint i = 0; i < n; i++)
174 {
175 if (i != 0) res += ", ";
176 res += args[i];
177 }
178 if (n > 1) res += "]";
179 res += " -> " + e.Value + ", ";
180 }
181 res += "else -> " + Else;
182 res += "]";
183 return res;
184 }
Microsoft.Z3.FuncInterp.Entries
Entry[] Entries
The entries in the function interpretation
Definition: FuncInterp.cs:129
Microsoft.Z3.FuncInterp.Else
Expr Else
The (symbolic) ‘else’ value of the function interpretation.
Definition: FuncInterp.cs:145

## Property Documentation

## ◆ Arity

uint Arity
| get

The arity of the function interpretation

Definition at line 156 of file FuncInterp.cs.

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

## ◆ Else

Expr Else
| get

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

Definition at line 144 of file FuncInterp.cs.

145 {
146 get
147 {
148
149 return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
150 }
151 }

Referenced by FuncInterp.ToString().

## ◆ Entries

Entry [] Entries
| get

The entries in the function interpretation

Definition at line 128 of file FuncInterp.cs.

129 {
130 get
131 {
132
133 uint n = NumEntries;
134 Entry[] res = new Entry[n];
135 for (uint i = 0; i < n; i++)
136 res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
137 return res;
138 }
139 }
Microsoft.Z3.FuncInterp.NumEntries
uint NumEntries
The number of entries in the function interpretation.
Definition: FuncInterp.cs:121

Referenced by FuncInterp.ToString().

## ◆ NumEntries

uint NumEntries
| get

The number of entries in the function interpretation.

Definition at line 120 of file FuncInterp.cs.

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