Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

Properties

uint NumEntries [get]
 The number of entries in the function interpretation.
 
Entry[] Entries [get]
 The entries in the function interpretation
 
Expr Else [get]
 The (symbolic) `else' value of the function interpretation.
 
uint Arity [get]
 The arity of the function interpretation
 

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

{
string res = "";
res += "[";
foreach (Entry e in Entries)
{
uint n = e.NumArgs;
if (n > 1) res += "[";
Expr[] args = e.Args;
for (uint i = 0; i < n; i++)
{
if (i != 0) res += ", ";
res += args[i];
}
if (n > 1) res += "]";
res += " -> " + e.Value + ", ";
}
res += "else -> " + Else;
res += "]";
return res;
}

Property Documentation

uint Arity
get

The arity of the function interpretation

Definition at line 159 of file FuncInterp.cs.

Expr Else
get

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

Definition at line 148 of file FuncInterp.cs.

Entry [] Entries
get

The entries in the function interpretation

Definition at line 129 of file FuncInterp.cs.

uint NumEntries
get

The number of entries in the function interpretation.

Definition at line 121 of file FuncInterp.cs.