z3 4.11.2 · OCaml Package

z3

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.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