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

Entry[] | Entries |

Set of non-default entries defining the function graph More... | |

Z3_ast | Else |

Default cause of the function interpretation More... | |

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.

Z3_func_decl Declaration |

Function that is interpreted

Definition at line 61 of file NativeFuncInterp.cs.

Z3_ast Else |

Default cause of the function interpretation

Definition at line 71 of file NativeFuncInterp.cs.

Entry [] Entries |

Set of non-default entries defining the function graph

Definition at line 66 of file NativeFuncInterp.cs.

Generated on Sat Jan 14 2023 14:44:09 for Z3 by 1.9.1