Module Z3.Model.FuncInterp

module FuncInterp: sig .. end
Function interpretations

A function interpretation is represented as a finite map and an 'else'. Each entry in the finite map represents the value of a function given a set of arguments.


type func_interp 
module FuncEntry: sig .. end
Function interpretations entries
val get_num_entries : func_interp -> int
The number of entries in the function interpretation.
val get_entries : func_interp ->
FuncEntry.func_entry list
The entries in the function interpretation
val get_else : func_interp -> Expr.expr
The (symbolic) `else' value of the function interpretation.
val get_arity : func_interp -> int
The arity of the function interpretation
val to_string : func_interp -> string
A string representation of the function interpretation.