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