Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

FunctionGraph Class Reference
[Managed (.NET) API]

Z3 Function graph object. More...

Data Fields
ConstDeclAstPtr	Declaration
array< FunctionEntry^>	Entries
ValuePtr	Else

---

Detailed Description

Z3 Function graph object.

The finite function graph of an uninterpreted function is represented as a list of FunctionEntry entries, together with a default value. The domain values not listed in the FunctionEntry array map to the default value Else.

Parameters:

	Declaration	contains the function declaration Ast.
	Entries	contains the array of entries where the function is defined explicitly.
	Contains	the default value of the function; where the function maps to a default value.

Definition at line 432 of file Microsoft.Z3.h.