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