sig
  type key
  type value
  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 mvbdu
  type hconsed_range_list
  type hconsed_association_list
  type hconsed_variables_list
  type hconsed_renaming_list
  type 'output constant =
      Remanent_parameters_sig.parameters ->
      Mvbdu_wrapper.Mvbdu.handler ->
      Exception.method_handler ->
      Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler * 'output
  type ('input, 'output) unary =
      Remanent_parameters_sig.parameters ->
      Mvbdu_wrapper.Mvbdu.handler ->
      Exception.method_handler ->
      'input ->
      Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler * 'output
  type ('input1, 'input2, 'output) binary =
      Remanent_parameters_sig.parameters ->
      Mvbdu_wrapper.Mvbdu.handler ->
      Exception.method_handler ->
      'input1 ->
      'input2 ->
      Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler * 'output
  type ('input1, 'input2, 'input3, 'output) ternary =
      Remanent_parameters_sig.parameters ->
      Mvbdu_wrapper.Mvbdu.handler ->
      Exception.method_handler ->
      'input1 ->
      'input2 ->
      'input3 ->
      Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler * 'output
  val init :
    Remanent_parameters_sig.parameters ->
    Exception.method_handler ->
    Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler
  val is_init : unit -> bool
  val get_handler :
    Remanent_parameters_sig.parameters ->
    Exception.method_handler ->
    Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler
  val reset :
    Remanent_parameters_sig.parameters ->
    Exception.method_handler ->
    Exception.method_handler * Mvbdu_wrapper.Mvbdu.handler
  val equal : Mvbdu_wrapper.Mvbdu.mvbdu -> Mvbdu_wrapper.Mvbdu.mvbdu -> bool
  val equal_with_logs :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu, bool)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_false : Mvbdu_wrapper.Mvbdu.mvbdu Mvbdu_wrapper.Mvbdu.constant
  val mvbdu_true : Mvbdu_wrapper.Mvbdu.mvbdu Mvbdu_wrapper.Mvbdu.constant
  val mvbdu_not :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_id :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_unary_true :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_unary_false :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_and :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_or :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_xor :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nand :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nor :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_imply :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_rev_imply :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_equiv :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nimply :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nrev_imply :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_bi_true :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_bi_false :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_fst :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_snd :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nfst :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_nsnd :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_redefine :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_association_list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_redefine_range :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_range_list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_subseteq :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu, bool)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_of_hconsed_asso :
    (Mvbdu_wrapper.Mvbdu.hconsed_association_list, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_sorted_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_reverse_sorted_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_hconsed_range :
    (Mvbdu_wrapper.Mvbdu.hconsed_range_list, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_sorted_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_of_reverse_sorted_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_rename :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_renaming_list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_project_keep_only :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_variables_list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_project_abstract_away :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_variables_list,
     Mvbdu_wrapper.Mvbdu.mvbdu)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_cartesian_decomposition_depth :
    (Mvbdu_wrapper.Mvbdu.mvbdu, int,
     Mvbdu_wrapper.Mvbdu.mvbdu option * Mvbdu_wrapper.Mvbdu.mvbdu list)
    Mvbdu_wrapper.Mvbdu.binary
  val mvbdu_full_cartesian_decomposition :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu list)
    Mvbdu_wrapper.Mvbdu.unary
  val mvbdu_cartesian_abstraction :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.mvbdu list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.hconsed_association_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_sorted_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.hconsed_association_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_reverse_sorted_association_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list,
     Mvbdu_wrapper.Mvbdu.hconsed_association_list)
    Mvbdu_wrapper.Mvbdu.unary
  val empty_association_list :
    Mvbdu_wrapper.Mvbdu.hconsed_association_list Mvbdu_wrapper.Mvbdu.constant
  val build_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.hconsed_range_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_sorted_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.hconsed_range_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_reverse_sorted_range_list :
    ((Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list, Mvbdu_wrapper.Mvbdu.hconsed_range_list)
    Mvbdu_wrapper.Mvbdu.unary
  val empty_range_list :
    Mvbdu_wrapper.Mvbdu.hconsed_range_list Mvbdu_wrapper.Mvbdu.constant
  val build_variables_list :
    (Mvbdu_wrapper.Mvbdu.key list,
     Mvbdu_wrapper.Mvbdu.hconsed_variables_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_sorted_variables_list :
    (Mvbdu_wrapper.Mvbdu.key list,
     Mvbdu_wrapper.Mvbdu.hconsed_variables_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_reverse_sorted_variables_list :
    (Mvbdu_wrapper.Mvbdu.key list,
     Mvbdu_wrapper.Mvbdu.hconsed_variables_list)
    Mvbdu_wrapper.Mvbdu.unary
  val empty_variables_list :
    Mvbdu_wrapper.Mvbdu.hconsed_variables_list Mvbdu_wrapper.Mvbdu.constant
  val build_renaming_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.key) list,
     Mvbdu_wrapper.Mvbdu.hconsed_renaming_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_sorted_renaming_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.key) list,
     Mvbdu_wrapper.Mvbdu.hconsed_renaming_list)
    Mvbdu_wrapper.Mvbdu.unary
  val build_reverse_sorted_renaming_list :
    ((Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.key) list,
     Mvbdu_wrapper.Mvbdu.hconsed_renaming_list)
    Mvbdu_wrapper.Mvbdu.unary
  val empty_renaming_list :
    Mvbdu_wrapper.Mvbdu.hconsed_renaming_list Mvbdu_wrapper.Mvbdu.constant
  val overwrite_association_lists :
    (Mvbdu_wrapper.Mvbdu.hconsed_association_list,
     Mvbdu_wrapper.Mvbdu.hconsed_association_list,
     Mvbdu_wrapper.Mvbdu.hconsed_association_list)
    Mvbdu_wrapper.Mvbdu.binary
  val merge_variables_lists :
    (Mvbdu_wrapper.Mvbdu.hconsed_variables_list,
     Mvbdu_wrapper.Mvbdu.hconsed_variables_list,
     Mvbdu_wrapper.Mvbdu.hconsed_variables_list)
    Mvbdu_wrapper.Mvbdu.binary
  val nbr_variables :
    (Mvbdu_wrapper.Mvbdu.hconsed_variables_list, int)
    Mvbdu_wrapper.Mvbdu.unary
  val extensional_of_variables_list :
    (Mvbdu_wrapper.Mvbdu.hconsed_variables_list,
     Mvbdu_wrapper.Mvbdu.key list)
    Mvbdu_wrapper.Mvbdu.unary
  val extensional_of_association_list :
    (Mvbdu_wrapper.Mvbdu.hconsed_association_list,
     (Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list)
    Mvbdu_wrapper.Mvbdu.unary
  val extensional_of_range_list :
    (Mvbdu_wrapper.Mvbdu.hconsed_range_list,
     (Mvbdu_wrapper.Mvbdu.key *
      (Mvbdu_wrapper.Mvbdu.value * Mvbdu_wrapper.Mvbdu.value))
     list)
    Mvbdu_wrapper.Mvbdu.unary
  val extensional_of_mvbdu :
    (Mvbdu_wrapper.Mvbdu.mvbdu,
     (Mvbdu_wrapper.Mvbdu.key * Mvbdu_wrapper.Mvbdu.value) list list)
    Mvbdu_wrapper.Mvbdu.unary
  val variables_list_of_mvbdu :
    (Mvbdu_wrapper.Mvbdu.mvbdu, Mvbdu_wrapper.Mvbdu.hconsed_variables_list)
    Mvbdu_wrapper.Mvbdu.unary
  val print :
    Remanent_parameters_sig.parameters -> Mvbdu_wrapper.Mvbdu.mvbdu -> unit
  val print_association_list :
    Remanent_parameters_sig.parameters ->
    Mvbdu_wrapper.Mvbdu.hconsed_association_list -> unit
  val print_variables_list :
    Remanent_parameters_sig.parameters ->
    Mvbdu_wrapper.Mvbdu.hconsed_variables_list -> unit
  val store_by_variables_list :
    (Remanent_parameters_sig.parameters ->
     Exception.method_handler ->
     'data -> List_sig.hash_key -> 'map -> Exception.method_handler * 'data) ->
    (Remanent_parameters_sig.parameters ->
     Exception.method_handler ->
     List_sig.hash_key -> 'data -> 'map -> Exception.method_handler * 'map) ->
    'data ->
    ('data, 'data, 'data) Mvbdu_wrapper.Mvbdu.binary ->
    (Mvbdu_wrapper.Mvbdu.hconsed_variables_list, 'data, 'map, 'map)
    Mvbdu_wrapper.Mvbdu.ternary
  val store_by_mvbdu :
    (Remanent_parameters_sig.parameters ->
     Exception.method_handler ->
     'data -> Mvbdu_sig.hash_key -> 'map -> Exception.method_handler * 'data) ->
    (Remanent_parameters_sig.parameters ->
     Exception.method_handler ->
     Mvbdu_sig.hash_key -> 'data -> 'map -> Exception.method_handler * 'map) ->
    'data ->
    ('data, 'data, 'data) Mvbdu_wrapper.Mvbdu.binary ->
    (Mvbdu_wrapper.Mvbdu.mvbdu, 'data, 'map, 'map)
    Mvbdu_wrapper.Mvbdu.ternary
  val last_entry : (unit, int) Mvbdu_wrapper.Mvbdu.unary
  val hash_of_range_list : Mvbdu_wrapper.Mvbdu.hconsed_range_list -> int
  val hash_of_association_list :
    Mvbdu_wrapper.Mvbdu.hconsed_association_list -> int
  val hash_of_variables_list :
    Mvbdu_wrapper.Mvbdu.hconsed_variables_list -> int
end