Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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 169 of file FuncInterp.cs.

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

Property Documentation

uint Arity
get

The arity of the function interpretation

Definition at line 162 of file FuncInterp.cs.

Expr Else
get

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

Definition at line 149 of file FuncInterp.cs.

Entry [] Entries
get

The entries in the function interpretation

Definition at line 131 of file FuncInterp.cs.

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 123 of file FuncInterp.cs.