z3 4.11.2 · OCaml Package

z3

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Integer : sig ... end

module Real : sig ... end

val is_int : Expr.expr -> bool

val is_arithmetic_numeral : Expr.expr -> bool

val is_le : Expr.expr -> bool

val is_ge : Expr.expr -> bool

val is_lt : Expr.expr -> bool

val is_gt : Expr.expr -> bool

val is_add : Expr.expr -> bool

val is_sub : Expr.expr -> bool

val is_uminus : Expr.expr -> bool

val is_mul : Expr.expr -> bool

val is_div : Expr.expr -> bool

val is_idiv : Expr.expr -> bool

val is_remainder : Expr.expr -> bool

val is_modulus : Expr.expr -> bool

val is_int2real : Expr.expr -> bool

val is_real2int : Expr.expr -> bool

val is_real_is_int : Expr.expr -> bool

val is_real : Expr.expr -> bool

val is_int_numeral : Expr.expr -> bool

val is_rat_numeral : Expr.expr -> bool

val is_algebraic_number : Expr.expr -> bool

val mk_add : context -> Expr.expr list -> Expr.expr

val mk_mul : context -> Expr.expr list -> Expr.expr

val mk_sub : context -> Expr.expr list -> Expr.expr

val mk_unary_minus : context -> Expr.expr -> Expr.expr

val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_power : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_le : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_ge : context -> Expr.expr -> Expr.expr -> Expr.expr