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

Member Function Documentation

◆ ToString()

override string ToString ( )
inline

A string representation of the function interpretation.

Definition at line 171 of file FuncInterp.cs.

172  {
173  string res = "";
174  res += "[";
175  foreach (Entry e in Entries)
176  {
177  uint n = e.NumArgs;
178  if (n > 1) res += "[";
179  Expr[] args = e.Args;
180  for (uint i = 0; i < n; i++)
181  {
182  if (i != 0) res += ", ";
183  res += args[i];
184  }
185  if (n > 1) res += "]";
186  res += " -> " + e.Value + ", ";
187  }
188  res += "else -> " + Else;
189  res += "]";
190  return res;
191  }
Entry [] Entries
The entries in the function interpretation
Definition: FuncInterp.cs:133
Expr Else
The (symbolic) `else&#39; value of the function interpretation.
Definition: FuncInterp.cs:151

Property Documentation

◆ Arity

uint Arity
get

The arity of the function interpretation

Definition at line 164 of file FuncInterp.cs.

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

◆ Else

Expr Else
get

The (symbolic) `else' value of the function interpretation.

Definition at line 151 of file FuncInterp.cs.

151  {
152  get
153  {
154  Contract.Ensures(Contract.Result<Expr>() != null);
155 
156  return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
157  }
158  }

◆ Entries

Entry [] Entries
get

The entries in the function interpretation

Definition at line 133 of file FuncInterp.cs.

133  {
134  get
135  {
136  Contract.Ensures(Contract.Result<Entry[]>() != null);
137  Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
138 
139  uint n = NumEntries;
140  Entry[] res = new Entry[n];
141  for (uint i = 0; i < n; i++)
142  res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
143  return res;
144  }
145  }
uint NumEntries
The number of entries in the function interpretation.
Definition: FuncInterp.cs:125

◆ NumEntries

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 125 of file FuncInterp.cs.

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