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 func_decl

module Parameter : sig ... end

val mk_func_decl : 
  context ->
  Symbol.symbol ->
  Sort.sort list ->
  Sort.sort ->
  func_decl

val mk_func_decl_s : 
  context ->
  string ->
  Sort.sort list ->
  Sort.sort ->
  func_decl

val mk_rec_func_decl : 
  context ->
  Symbol.symbol ->
  Sort.sort list ->
  Sort.sort ->
  func_decl

val mk_rec_func_decl_s : 
  context ->
  string ->
  Sort.sort list ->
  Sort.sort ->
  func_decl

val add_rec_def : context -> func_decl -> Expr.expr list -> Expr.expr -> unit

val mk_fresh_func_decl : 
  context ->
  string ->
  Sort.sort list ->
  Sort.sort ->
  func_decl

val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl

val mk_const_decl_s : context -> string -> Sort.sort -> func_decl

val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl

val equal : func_decl -> func_decl -> bool

val to_string : func_decl -> string

val get_id : func_decl -> int

val get_arity : func_decl -> int

val get_domain_size : func_decl -> int

val get_domain : func_decl -> Sort.sort list

val get_range : func_decl -> Sort.sort

val get_decl_kind : func_decl -> Z3enums.decl_kind

val get_name : func_decl -> Symbol.symbol

val get_num_parameters : func_decl -> int

val get_parameters : func_decl -> Parameter.parameter list

val apply : func_decl -> Expr.expr list -> Expr.expr