sig
val smallSIZE : int
val bigSIZE : int
val hashSIZE : int Pervasives.ref
type 'a diag_raw =
Empty
| Unit
| And of 'a * 'a Diagram.diag * 'a Diagram.diag * 'a Diagram.diag
and 'a diag = 'a Diagram.diag_raw HashCons.hc
module type Variables =
sig
type t
val compare : Diagram.Variables.t -> Diagram.Variables.t -> int
val hash : Diagram.Variables.t -> int
val neg : Diagram.Variables.t -> Diagram.Variables.t
val is_pos : Diagram.Variables.t -> bool
val str : Diagram.Variables.t -> string
val max : Diagram.Variables.t
val to_int : Diagram.Variables.t -> int
end
module type S =
sig
type var
type t_raw =
Empty
| Unit
| And of Diagram.S.var * Diagram.S.t * Diagram.S.t * Diagram.S.t
and t = Diagram.S.t_raw HashCons.hc
module DiagCons :
sig
type data = t_raw
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = var list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
val get : Diagram.S.t -> Diagram.S.var Diagram.diag
val build : Diagram.S.var Diagram.diag -> Diagram.S.t
val clear : unit -> unit
val cEmpty : Diagram.S.t
val cUnit : Diagram.S.t
val cAnd :
Diagram.S.var * Diagram.S.t * Diagram.S.t * Diagram.S.t ->
Diagram.S.t
val diag_of_cnf : Diagram.S.var list list -> Diagram.S.t
val diag_str : ?vars:bool -> Diagram.S.t -> string
val log :
string -> Diagram.S.var -> Diagram.S.t -> Diagram.S.var list -> unit
val size : Diagram.S.t -> int * int
val vars : Diagram.S.t -> (Diagram.S.var * int) list
val singletons : Diagram.S.t -> Diagram.S.var list
val mk_and : Diagram.S.t -> Diagram.S.t -> Diagram.S.t
val mk_or : Diagram.S.t -> Diagram.S.t -> Diagram.S.t
val propagate_once : Diagram.S.var list -> Diagram.S.t -> Diagram.S.t
val propagate : Diagram.S.var list -> Diagram.S.t -> Diagram.S.t
val remove : Diagram.S.var -> Diagram.S.t -> Diagram.S.t
val elim_var :
?log:bool ->
?bound:int option ->
?sat:bool ->
?universal:bool -> Diagram.S.var -> Diagram.S.t -> Diagram.S.t
val elim_top_until : ?log:bool -> int -> Diagram.S.t -> Diagram.S.t
val top_reduce : ?log:bool -> int -> Diagram.S.t -> Diagram.S.t
val top_sat : ?log:bool -> Diagram.S.t -> bool
val elim_sat : Diagram.S.t -> bool
val mixed_sat : ?log:bool -> Diagram.S.t -> bool
val elim_bounded :
?universal:bool ->
?until:(Diagram.S.var -> bool) ->
?sat:bool -> int -> Diagram.S.t -> Diagram.S.t
val elim_bounded_sat : Diagram.S.t -> bool
val formula : Diagram.S.t -> QBF.bool_formula
end
module Make :
functor (V : Variables) ->
sig
type var = V.t
type t_raw = Empty | Unit | And of var * t * t * t
and t = t_raw HashCons.hc
module DiagCons :
sig
type data = t_raw
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = var list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
val get : t -> var diag
val build : var diag -> t
val clear : unit -> unit
val cEmpty : t
val cUnit : t
val cAnd : var * t * t * t -> t
val diag_of_cnf : var list list -> t
val diag_str : ?vars:bool -> t -> string
val log : string -> var -> t -> var list -> unit
val size : t -> int * int
val vars : t -> (var * int) list
val singletons : t -> var list
val mk_and : t -> t -> t
val mk_or : t -> t -> t
val propagate_once : var list -> t -> t
val propagate : var list -> t -> t
val remove : var -> t -> t
val elim_var :
?log:bool ->
?bound:int option -> ?sat:bool -> ?universal:bool -> var -> t -> t
val elim_top_until : ?log:bool -> int -> t -> t
val top_reduce : ?log:bool -> int -> t -> t
val top_sat : ?log:bool -> t -> bool
val elim_sat : t -> bool
val mixed_sat : ?log:bool -> t -> bool
val elim_bounded :
?universal:bool ->
?until:(var -> bool) -> ?sat:bool -> int -> t -> t
val elim_bounded_sat : t -> bool
val formula : t -> QBF.bool_formula
end
val weights_array : int array Pervasives.ref
val cmp_weight : int -> int -> int
module WeightIntOrd :
sig
type t = int
val compare : t -> t -> int
val hash : t -> int
val neg : t -> t
val is_pos : t -> bool
val str : t -> string
val max : t
val to_int : t -> int
end
module WeightDiags :
sig
type var = int
type t_raw = Empty | Unit | And of var * t * t * t
and t = t_raw HashCons.hc
module DiagCons :
sig
type data = t_raw
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = var list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
val get : t -> var diag
val build : var diag -> t
val clear : unit -> unit
val cEmpty : t
val cUnit : t
val cAnd : var * t * t * t -> t
val diag_of_cnf : var list list -> t
val diag_str : ?vars:bool -> t -> string
val log : string -> var -> t -> var list -> unit
val size : t -> int * int
val vars : t -> (var * int) list
val singletons : t -> var list
val mk_and : t -> t -> t
val mk_or : t -> t -> t
val propagate_once : var list -> t -> t
val propagate : var list -> t -> t
val remove : var -> t -> t
val elim_var :
?log:bool ->
?bound:int option -> ?sat:bool -> ?universal:bool -> var -> t -> t
val elim_top_until : ?log:bool -> int -> t -> t
val top_reduce : ?log:bool -> int -> t -> t
val top_sat : ?log:bool -> t -> bool
val elim_sat : t -> bool
val mixed_sat : ?log:bool -> t -> bool
val elim_bounded :
?universal:bool -> ?until:(var -> bool) -> ?sat:bool -> int -> t -> t
val elim_bounded_sat : t -> bool
val formula : t -> QBF.bool_formula
end
val diag_of_qbf :
?reverse:bool ->
?elim_quant:bool ->
?weights:int array -> QBF.qbf -> Diagram.WeightDiags.t
module BigIntOrd :
sig
type t = int
val compare : t -> t -> int
val hash : t -> int
val neg : t -> t
val is_pos : t -> bool
val str : t -> string
val max : t
val to_int : t -> int
end
module BigIntDiags :
sig
type var = int
type t_raw = Empty | Unit | And of var * t * t * t
and t = t_raw HashCons.hc
module DiagCons :
sig
type data = t_raw
type t
val create : int -> t
val clear : t -> unit
val hashcons : ?log:bool -> t -> data -> data HashCons.hc
module H1 :
sig
type key = data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module H2 :
sig
type key = data HashCons.hc * data HashCons.hc
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
type other_value = var list
module HV :
sig
type key = data HashCons.hc * other_value
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val get_h1 : t -> data HashCons.hc H1.t
val get_h2 : t -> data HashCons.hc H2.t
val get_hv : t -> data HashCons.hc HV.t
val get_h1_alpha :
(module HashCons.Type with type t = 'a) -> t -> 'a H1.t
end
val get : t -> var diag
val build : var diag -> t
val clear : unit -> unit
val cEmpty : t
val cUnit : t
val cAnd : var * t * t * t -> t
val diag_of_cnf : var list list -> t
val diag_str : ?vars:bool -> t -> string
val log : string -> var -> t -> var list -> unit
val size : t -> int * int
val vars : t -> (var * int) list
val singletons : t -> var list
val mk_and : t -> t -> t
val mk_or : t -> t -> t
val propagate_once : var list -> t -> t
val propagate : var list -> t -> t
val remove : var -> t -> t
val elim_var :
?log:bool ->
?bound:int option -> ?sat:bool -> ?universal:bool -> var -> t -> t
val elim_top_until : ?log:bool -> int -> t -> t
val top_reduce : ?log:bool -> int -> t -> t
val top_sat : ?log:bool -> t -> bool
val elim_sat : t -> bool
val mixed_sat : ?log:bool -> t -> bool
val elim_bounded :
?universal:bool -> ?until:(var -> bool) -> ?sat:bool -> int -> t -> t
val elim_bounded_sat : t -> bool
val formula : t -> QBF.bool_formula
end
val shape : Diagram.WeightDiags.t -> Diagram.BigIntDiags.t
end