Datatype (docs.findlib-94.z3.Z3.Datatype)

module Constructor : sig ... end

val mk_constructor : 
  context ->
  Symbol.symbol ->
  Symbol.symbol ->
  Symbol.symbol list ->
  Sort.sort option list ->
  int list ->
  Constructor.constructor

val mk_constructor_s : 
  context ->
  string ->
  Symbol.symbol ->
  Symbol.symbol list ->
  Sort.sort option list ->
  int list ->
  Constructor.constructor

val mk_sort_ref : context -> Symbol.symbol -> Sort.sort

val mk_sort_ref_s : context -> string -> Sort.sort

val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort

val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort

val mk_sort : 
  context ->
  Symbol.symbol ->
  Constructor.constructor list ->
  Sort.sort

val mk_sort_s : context -> string -> Constructor.constructor list -> Sort.sort

val mk_polymorphic_sort : 
  context ->
  Symbol.symbol ->
  Sort.sort list ->
  Constructor.constructor list ->
  Sort.sort

val mk_polymorphic_sort_s : 
  context ->
  string ->
  Sort.sort list ->
  Constructor.constructor list ->
  Sort.sort

val mk_sorts : 
  context ->
  Symbol.symbol list ->
  Constructor.constructor list list ->
  Sort.sort list

val mk_sorts_s : 
  context ->
  string list ->
  Constructor.constructor list list ->
  Sort.sort list

val get_num_constructors : Sort.sort -> int

val get_constructors : Sort.sort -> FuncDecl.func_decl list

val get_recognizers : Sort.sort -> FuncDecl.func_decl list

val get_accessors : Sort.sort -> FuncDecl.func_decl list list

val update_field : 
  context ->
  FuncDecl.func_decl ->
  Expr.expr ->
  Expr.expr ->
  Expr.expr