sig
  type key
  type value
  type mvbdu
  type handler =
      (Boolean_mvbdu.memo_tables, Boolean_mvbdu.mvbdu_dic,
       Boolean_mvbdu.association_list_dic, Boolean_mvbdu.range_list_dic,
       Boolean_mvbdu.variables_list_dic, bool, int)
      Memo_sig.handler
  type hconsed_range_list
  type hconsed_association_list
  type hconsed_variables_list
  type hconsed_renaming_list
  val init : Remanent_parameters_sig.parameters -> unit
  val import_handler : Mvbdu_wrapper.Internalized_mvbdu.handler -> unit
  val export_handler :
    Exception.method_handler ->
    Exception.method_handler *
    Mvbdu_wrapper.Internalized_mvbdu.handler option
  val is_init : unit -> bool
  val equal :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu -> bool
  val mvbdu_false : unit -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_true : unit -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_not :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_id :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_unary_true :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_unary_false :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_and :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_or :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_xor :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nand :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nor :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_imply :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_rev_imply :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_equiv :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nimply :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nrev_imply :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_bi_true :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_bi_false :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_fst :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_snd :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nfst :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_nsnd :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_redefine :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_redefine_range :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_subseteq :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu -> bool
  val mvbdu_of_hconsed_asso :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_sorted_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_reverse_sorted_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_hconsed_range :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_sorted_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_of_reverse_sorted_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_rename :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_renaming_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_project_abstract_away :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_project_keep_only :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu
  val mvbdu_cartesian_abstraction :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu list
  val mvbdu_cartesian_decomposition_depth :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    int ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu option *
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu list
  val mvbdu_full_cartesian_decomposition :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu list
  val build_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list
  val build_sorted_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list
  val build_reverse_sorted_association_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list
  val empty_association_list :
    unit -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list
  val build_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list
  val build_sorted_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list
  val build_reverse_sorted_range_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     (Mvbdu_wrapper.Internalized_mvbdu.value *
      Mvbdu_wrapper.Internalized_mvbdu.value))
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list
  val empty_range_list :
    unit -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_range_list
  val build_variables_list :
    Mvbdu_wrapper.Internalized_mvbdu.key list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val build_sorted_variables_list :
    Mvbdu_wrapper.Internalized_mvbdu.key list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val build_reverse_sorted_variables_list :
    Mvbdu_wrapper.Internalized_mvbdu.key list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val empty_variables_list :
    unit -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val build_renaming_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.key)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_renaming_list
  val build_sorted_renaming_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.key)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_renaming_list
  val build_reverse_sorted_renaming_list :
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.key)
    list -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_renaming_list
  val empty_renaming_list :
    unit -> Mvbdu_wrapper.Internalized_mvbdu.hconsed_renaming_list
  val overwrite_association_lists :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list
  val merge_variables_lists :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val nbr_variables :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list -> int
  val extensional_of_variables_list :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list ->
    Mvbdu_wrapper.Internalized_mvbdu.key list
  val extensional_of_association_list :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list ->
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list
  val extensional_of_mvbdu :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    (Mvbdu_wrapper.Internalized_mvbdu.key *
     Mvbdu_wrapper.Internalized_mvbdu.value)
    list list
  val variables_list_of_mvbdu :
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list
  val print :
    Remanent_parameters_sig.parameters ->
    Mvbdu_wrapper.Internalized_mvbdu.mvbdu -> unit
  val print_association_list :
    Remanent_parameters_sig.parameters ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list -> unit
  val print_variables_list :
    Remanent_parameters_sig.parameters ->
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list -> unit
  val hash_of_association_list :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_association_list -> int
  val hash_of_variables_list :
    Mvbdu_wrapper.Internalized_mvbdu.hconsed_variables_list -> int
end