Module Z3.Z3List

module Z3List: sig .. end

Functions to manipulate List expressions

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

Create a new list sort.

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

Create a new list sort.

val get_nil_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the nil function of this list sort.

val get_is_nil_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the isNil function of this list sort.

val get_cons_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the cons function of this list sort.

val get_is_cons_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the isCons function of this list sort.

val get_head_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the head function of this list sort.

val get_tail_decl : Sort.sort -> FuncDecl.func_decl

The declaration of the tail function of this list sort.

val nil : Sort.sort -> Expr.expr

The empty list.