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  }

Property Documentation

◆ Arity

uint Arity
get

The arity of the function interpretation

Definition at line 157 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 145 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 129 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  }

Referenced by FuncInterp.ToString().

◆ NumEntries

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 121 of file FuncInterp.cs.

121  {
122  get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
123  }
Microsoft.Z3.FuncInterp.NumEntries
uint NumEntries
The number of entries in the function interpretation.
Definition: FuncInterp.cs:121
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