Helper class for declaring Z3 datatypes.
Follows the same pattern as Python Z3 API for declaring constructors before creating the actual datatype sort.
const List = new ctx.Datatype('List');List.declare('cons', ['car', ctx.Int.sort()], ['cdr', List]);List.declare('nil');const ListSort = List.create(); Copy
const List = new ctx.Datatype('List');List.declare('cons', ['car', ctx.Int.sort()], ['cdr', List]);List.declare('nil');const ListSort = List.create();
Readonly
Create the actual datatype sort from the declared constructors. For mutually recursive datatypes, use Context.createDatatypes instead.
Declare a constructor for this datatype.
Constructor name
Array of [field_name, field_sort] pairs
Helper class for declaring Z3 datatypes.
Follows the same pattern as Python Z3 API for declaring constructors before creating the actual datatype sort.
Example