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.