Module Z3.Model

type model
module FuncInterp : sig ... end
val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option
val get_const_interp_e : model -> Expr.expr -> Expr.expr option
val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option
val get_num_consts : model -> int
val get_const_decls : model -> FuncDecl.func_decl list
val get_num_funcs : model -> int
val get_func_decls : model -> FuncDecl.func_decl list
val get_decls : model -> FuncDecl.func_decl list
val eval : model -> Expr.expr -> bool -> Expr.expr option
val evaluate : model -> Expr.expr -> bool -> Expr.expr option
val get_num_sorts : model -> int
val get_sorts : model -> Sort.sort list
val sort_universe : model -> Sort.sort -> Expr.expr list
val to_string : model -> string