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.

§ Else

Expr Else
get

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

Definition at line 151 of file FuncInterp.cs.

§ Entries

Entry [] Entries
get

The entries in the function interpretation

Definition at line 133 of file FuncInterp.cs.

§ NumEntries

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 125 of file FuncInterp.cs.