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_ref : context -> Symbol.symbol -> Sort.sort

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

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.