Module Z3.FiniteDomain

module FiniteDomain: sig .. end

Functions to manipulate Finite Domain expressions

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

Create a new finite domain sort.

val mk_sort_s : context -> string -> int64 -> Sort.sort

Create a new finite domain sort.

val is_finite_domain : Expr.expr -> bool

Indicates whether the term is of an array sort.

val is_lt : Expr.expr -> bool

Indicates whether the term is a less than predicate over a finite domain.

val get_size : Sort.sort -> int64

The size of the finite domain sort.