Module Z3.Datatype

module Datatype: sig .. end
Functions to manipulate Datatype expressions

module Constructor: sig .. end
Datatype Constructors
val mk_constructor : context ->
Symbol.symbol ->
Symbol.symbol ->
Symbol.symbol list ->
Sort.sort option list -> int list -> Constructor.constructor
Create a datatype constructor. if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.
val mk_constructor_s : context ->
string ->
Symbol.symbol ->
Symbol.symbol list ->
Sort.sort option list -> int list -> Constructor.constructor
Create a datatype constructor. if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.
val mk_sort : context ->
Symbol.symbol -> Constructor.constructor list -> Sort.sort
Create a new datatype sort.
val mk_sort_s : context ->
string -> Constructor.constructor list -> Sort.sort
Create a new datatype sort.
val mk_sorts : context ->
Symbol.symbol list ->
Constructor.constructor list list -> Sort.sort list
Create mutually recursive datatypes.
val mk_sorts_s : context ->
string list ->
Constructor.constructor list list -> Sort.sort list
Create mutually recursive data-types.
val get_num_constructors : Sort.sort -> int
The number of constructors of the datatype sort.
val get_constructors : Sort.sort -> FuncDecl.func_decl list
The constructors.
val get_recognizers : Sort.sort -> FuncDecl.func_decl list
The recognizers.
val get_accessors : Sort.sort -> FuncDecl.func_decl list list
The constructor accessors.