sig
  type atom_name = ID.t
  type sub_universe = { su_name : FO_rel.atom_name; su_card : int option; }
  type atom = { a_sub_universe : FO_rel.sub_universe; a_index : int; }
  type tuple = FO_rel.atom list
  type tuple_set = private
      TS_list of FO_rel.tuple list
    | TS_product of FO_rel.tuple_set list
    | TS_all of FO_rel.sub_universe
  type unop = Flip | Trans
  type binop = Union | Inter | Diff | Join | Product
  type mult = M_no | M_one | M_lone | M_some
  type expr =
      None_
    | Const of ID.t
    | Tuple_set of FO_rel.tuple_set
    | Var of FO_rel.var
    | Unop of FO_rel.unop * FO_rel.expr
    | Binop of FO_rel.binop * FO_rel.expr * FO_rel.expr
    | If of FO_rel.form * FO_rel.expr * FO_rel.expr
    | Comprehension of FO_rel.var * FO_rel.form
    | Let of FO_rel.var * FO_rel.expr * FO_rel.expr
  and var_ty = FO_rel.sub_universe
  and var = FO_rel.var_ty Var.t
  and form =
      True
    | False
    | Eq of FO_rel.expr * FO_rel.expr
    | In of FO_rel.expr * FO_rel.expr
    | Mult of FO_rel.mult * FO_rel.expr
    | Not of FO_rel.form
    | And of FO_rel.form list
    | Or of FO_rel.form list
    | Imply of FO_rel.form * FO_rel.form
    | Equiv of FO_rel.form * FO_rel.form
    | Forall of FO_rel.var * FO_rel.form
    | Exists of FO_rel.var * FO_rel.form
    | F_let of FO_rel.var * FO_rel.expr * FO_rel.form
    | F_if of FO_rel.form * FO_rel.form * FO_rel.form
    | Int_op of FO_rel.int_op * FO_rel.int_expr * FO_rel.int_expr
  and int_op = IO_leq
  and int_expr =
      IE_card of FO_rel.expr
    | IE_sum of FO_rel.expr
    | IE_cst of int
  type decl = {
    decl_id : ID.t;
    decl_arity : int;
    decl_dom : FO_rel.sub_universe list;
    decl_low : FO_rel.tuple_set;
    decl_high : FO_rel.tuple_set;
  }
  type universe = {
    univ_prop : FO_rel.sub_universe;
    univ_l : FO_rel.sub_universe list;
  }
  type problem = private {
    pb_univ : FO_rel.universe;
    pb_decls : FO_rel.decl ID.Map.t;
    pb_goal : FO_rel.form list;
    pb_meta : ProblemMetadata.t;
  }
  val unop : FO_rel.unop -> FO_rel.expr -> FO_rel.expr
  val binop : FO_rel.binop -> FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val mult : FO_rel.mult -> FO_rel.expr -> FO_rel.form
  val su_make : ?card:int -> ID.t -> FO_rel.sub_universe
  val su_equal : FO_rel.sub_universe -> FO_rel.sub_universe -> bool
  val su_hash : FO_rel.sub_universe -> int
  val su_compare : FO_rel.sub_universe -> FO_rel.sub_universe -> int
  val ts_list : FO_rel.tuple list -> FO_rel.tuple_set
  val ts_all : FO_rel.sub_universe -> FO_rel.tuple_set
  val ts_product : FO_rel.tuple_set list -> FO_rel.tuple_set
  val flip : FO_rel.expr -> FO_rel.expr
  val trans : FO_rel.expr -> FO_rel.expr
  val const : ID.t -> FO_rel.expr
  val var : FO_rel.var -> FO_rel.expr
  val tuple_set : FO_rel.tuple_set -> FO_rel.expr
  val union : FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val inter : FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val diff : FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val join : FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val product : FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val if_ : FO_rel.form -> FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val comprehension : FO_rel.var -> FO_rel.form -> FO_rel.expr
  val let_ : FO_rel.var -> FO_rel.expr -> FO_rel.expr -> FO_rel.expr
  val true_ : FO_rel.form
  val false_ : FO_rel.form
  val eq : FO_rel.expr -> FO_rel.expr -> FO_rel.form
  val in_ : FO_rel.expr -> FO_rel.expr -> FO_rel.form
  val no : FO_rel.expr -> FO_rel.form
  val one : FO_rel.expr -> FO_rel.form
  val some : FO_rel.expr -> FO_rel.form
  val not_ : FO_rel.form -> FO_rel.form
  val and_ : FO_rel.form -> FO_rel.form -> FO_rel.form
  val and_l : FO_rel.form list -> FO_rel.form
  val or_ : FO_rel.form -> FO_rel.form -> FO_rel.form
  val or_l : FO_rel.form list -> FO_rel.form
  val imply : FO_rel.form -> FO_rel.form -> FO_rel.form
  val equiv : FO_rel.form -> FO_rel.form -> FO_rel.form
  val for_all : FO_rel.var -> FO_rel.form -> FO_rel.form
  val for_all_l : FO_rel.var list -> FO_rel.form -> FO_rel.form
  val exists : FO_rel.var -> FO_rel.form -> FO_rel.form
  val exists_l : FO_rel.var list -> FO_rel.form -> FO_rel.form
  val f_let : FO_rel.var -> FO_rel.expr -> FO_rel.form -> FO_rel.form
  val f_if : FO_rel.form -> FO_rel.form -> FO_rel.form -> FO_rel.form
  val int_op :
    FO_rel.int_op -> FO_rel.int_expr -> FO_rel.int_expr -> FO_rel.form
  val int_leq : FO_rel.int_expr -> FO_rel.int_expr -> FO_rel.form
  val int_sum : FO_rel.expr -> FO_rel.int_expr
  val int_card : FO_rel.expr -> FO_rel.int_expr
  val int_const : int -> FO_rel.int_expr
  val atom : FO_rel.sub_universe -> int -> FO_rel.atom
  val atom_cmp : FO_rel.atom -> FO_rel.atom -> int
  val atom_eq : FO_rel.atom -> FO_rel.atom -> bool
  val mk_problem :
    meta:ProblemMetadata.t ->
    univ:FO_rel.universe ->
    decls:FO_rel.decl ID.Map.t -> goal:FO_rel.form list -> FO_rel.problem
  val print_atom : FO_rel.atom CCFormat.printer
  val print_tuple : FO_rel.tuple CCFormat.printer
  val print_tuple_set : FO_rel.tuple_set CCFormat.printer
  val print_sub_universe : FO_rel.sub_universe CCFormat.printer
  val print_var_ty : FO_rel.var_ty CCFormat.printer
  val print_universe : FO_rel.universe CCFormat.printer
  val print_expr : FO_rel.expr CCFormat.printer
  val print_int_expr : FO_rel.int_expr CCFormat.printer
  val print_form : FO_rel.form CCFormat.printer
  val print_decl : FO_rel.decl CCFormat.printer
  val print_problem : FO_rel.problem CCFormat.printer
end