package z3

  1. Overview
  2. Docs
val mk_sort : context -> Sort.sort -> Sort.sort
val is_union : Expr.expr -> bool
val is_intersect : Expr.expr -> bool
val is_difference : Expr.expr -> bool
val is_complement : Expr.expr -> bool
val is_subset : Expr.expr -> bool
val mk_empty : context -> Sort.sort -> Expr.expr
val mk_full : context -> Sort.sort -> Expr.expr
val mk_set_add : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_del : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_union : context -> Expr.expr list -> Expr.expr
val mk_intersection : context -> Expr.expr list -> Expr.expr
val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_complement : context -> Expr.expr -> Expr.expr
val mk_membership : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr