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

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

uint Arity
get

The arity of the function interpretation

Definition at line 164 of file FuncInterp.cs.

Expr Else
get

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

Definition at line 151 of file FuncInterp.cs.

Entry [] Entries
get

The entries in the function interpretation

Definition at line 133 of file FuncInterp.cs.

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 125 of file FuncInterp.cs.