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 }
Entry[] Entries
The entries in the function interpretation
Definition: FuncInterp.cs:129
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 }
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 }