| Home | • | Docs | • | Download | • | • | FAQ | • | Awards | • | Status | • | MSR |
|---|
An Efficient SMT Solver
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.
| 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 640 of file Microsoft.Z3.h.