Module Z3.FiniteDomain

module FiniteDomain: sig .. end
Functions to manipulate Finite Domain expressions

val mk_sort : context -> Symbol.symbol -> int -> Sort.sort
Create a new finite domain sort.
val mk_sort_s : context -> string -> int -> 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 -> int
The size of the finite domain sort.