sig
type 'a conjunction = Conjunction of 'a list | Cfalse
type 'a disjunction = Disjunction of 'a list | Dtrue
type 'a cnf = 'a Bdd.Normalform.disjunction Bdd.Normalform.conjunction
type 'a dnf = 'a Bdd.Normalform.conjunction Bdd.Normalform.disjunction
type ('a, 'b) tree = ('a * bool) list * ('a, 'b) Bdd.Normalform.decision
and ('a, 'b) decision =
Leaf of 'b
| Ite of 'a * ('a, 'b) Bdd.Normalform.tree * ('a, 'b) Bdd.Normalform.tree
val conjunction_false : 'a Bdd.Normalform.conjunction
val conjunction_true : 'a Bdd.Normalform.conjunction
val disjunction_false : 'a Bdd.Normalform.disjunction
val disjunction_true : 'a Bdd.Normalform.disjunction
val cnf_false : 'a Bdd.Normalform.cnf
val cnf_true : 'a Bdd.Normalform.cnf
val dnf_false : 'a Bdd.Normalform.dnf
val dnf_true : 'a Bdd.Normalform.dnf
val conjunction_and :
?merge:('a list -> 'a list -> 'a list) ->
'a Bdd.Normalform.conjunction ->
'a Bdd.Normalform.conjunction -> 'a Bdd.Normalform.conjunction
val disjunction_or :
?merge:('a list -> 'a list -> 'a list) ->
'a Bdd.Normalform.disjunction ->
'a Bdd.Normalform.disjunction -> 'a Bdd.Normalform.disjunction
val conjunction_and_term :
'a Bdd.Normalform.conjunction -> 'a -> 'a Bdd.Normalform.conjunction
val disjunction_or_term :
'a Bdd.Normalform.disjunction -> 'a -> 'a Bdd.Normalform.disjunction
val minterm_of_tree :
?compare:'b PHashhe.compare ->
('a, 'b) Bdd.Normalform.tree ->
(('a * bool) Bdd.Normalform.dnf * 'b) list
val rev_map_conjunction :
('a -> 'b) ->
'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
val rev_map_disjunction :
('a -> 'b) ->
'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
val rev_map2_conjunction :
('a -> 'b -> 'c) ->
'a Bdd.Normalform.conjunction ->
'b Bdd.Normalform.conjunction -> 'c Bdd.Normalform.conjunction
val rev_map2_disjunction :
('a -> 'b -> 'c) ->
'a Bdd.Normalform.disjunction ->
'b Bdd.Normalform.disjunction -> 'c Bdd.Normalform.disjunction
val map_conjunction :
('a -> 'b) ->
'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
val map_disjunction :
('a -> 'b) ->
'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
val map_cnf : ('a -> 'b) -> 'a Bdd.Normalform.cnf -> 'b Bdd.Normalform.cnf
val map_dnf : ('a -> 'b) -> 'a Bdd.Normalform.dnf -> 'b Bdd.Normalform.dnf
val map_tree :
('a -> 'c) ->
('b -> 'd) ->
('a, 'b) Bdd.Normalform.tree -> ('c, 'd) Bdd.Normalform.tree
val print_conjunction :
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.conjunction -> unit
val print_disjunction :
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.disjunction -> unit
val print_cnf :
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.cnf -> unit
val print_dnf :
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.dnf -> unit
val print_tree_minterm :
?compare:'a PHashhe.compare ->
(Format.formatter -> ('b * bool) Bdd.Normalform.dnf -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> ('b, 'a) Bdd.Normalform.tree -> unit
val print_tree :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) Bdd.Normalform.tree -> unit
end