NativeFuncInterp 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...

Data Structures
class	Entry
	Evaluation entry of a function. More...

Data Fields
Z3_func_decl	Declaration
	Function that is interpreted.
Entry[]	Entries
	Set of non-default entries defining the function graph.
Z3_ast	Else
	Default cause 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 39 of file NativeFuncInterp.cs.

Field Documentation

Declaration

Z3_func_decl Declaration

Function that is interpreted.

Definition at line 61 of file NativeFuncInterp.cs.

Else

Z3_ast Else

Default cause of the function interpretation.

Definition at line 71 of file NativeFuncInterp.cs.

Entries

Entry [] Entries

Set of non-default entries defining the function graph.

Definition at line 66 of file NativeFuncInterp.cs.