package z3

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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