sig
  type t = private {
    vars : Variable.t list;
    litterals : Types.SAtom.t;
    array : Types.ArrayAtom.t;
  }
  val create : Variable.t list -> Types.SAtom.t -> Cube.t
  val normal_form : Cube.t -> Cube.t
  val create_normal : Types.SAtom.t -> Cube.t
  val subst : Variable.subst -> Cube.t -> Cube.t
  val dim : Cube.t -> int
  val size : Cube.t -> int
  val inconsistent : ?use_sets:bool -> Cube.t -> bool
  val inconsistent_2 : ?use_sets:bool -> Cube.t -> Cube.t -> bool
  val inconsistent_set : Types.SAtom.t -> bool
  val inconsistent_array : Types.ArrayAtom.t -> bool
  val inconsistent_2arrays : Types.ArrayAtom.t -> Types.ArrayAtom.t -> bool
  val simplify_atoms_base : Types.SAtom.t -> Types.SAtom.t -> Types.SAtom.t
  val simplify_atoms : Types.SAtom.t -> Types.SAtom.t
  val simplify : Cube.t -> Cube.t
  val elim_ite_simplify_atoms : Types.SAtom.t -> Types.SAtom.t list
  val elim_ite_simplify : Cube.t -> Cube.t list
  val resolve_two : Cube.t -> Cube.t -> Cube.t option
  val satom_globs : Types.SAtom.t -> Types.Term.Set.t
  val print : Format.formatter -> Cube.t -> unit
end