bddapron 2.3.3 · OCaml Package

type !'a conjunction =

| Conjunction of 'a list
| Cfalse

type !'a disjunction =

| Disjunction of 'a list
| Dtrue

type !'a cnf = 'a disjunction conjunction

type !'a dnf = 'a conjunction disjunction

type (!'a, !'b) tree = ('a * bool) list * ('a, 'b) decision

and (!'a, !'b) decision =

| Leaf of 'b
| Ite of 'a * ('a, 'b) tree * ('a, 'b) tree

val conjunction_false : 'a conjunction

val conjunction_true : 'a conjunction

val disjunction_false : 'a disjunction

val disjunction_true : 'a disjunction

val cnf_false : 'a cnf

val cnf_true : 'a cnf

val dnf_false : 'a dnf

val dnf_true : 'a dnf

val conjunction_and : 
  ?merge:('a list -> 'a list -> 'a list) ->
  'a conjunction ->
  'a conjunction ->
  'a conjunction

val disjunction_or : 
  ?merge:('a list -> 'a list -> 'a list) ->
  'a disjunction ->
  'a disjunction ->
  'a disjunction

val conjunction_and_term : 'a conjunction -> 'a -> 'a conjunction

val disjunction_or_term : 'a disjunction -> 'a -> 'a disjunction

val minterm_of_tree : 
  ?compare:'b PHashhe.compare ->
  ('a, 'b) tree ->
  (('a * bool) dnf * 'b) list

val rev_map_conjunction : ('a -> 'b) -> 'a conjunction -> 'b conjunction

val rev_map_disjunction : ('a -> 'b) -> 'a disjunction -> 'b disjunction

val rev_map2_conjunction : 
  ('a -> 'b -> 'c) ->
  'a conjunction ->
  'b conjunction ->
  'c conjunction

val rev_map2_disjunction : 
  ('a -> 'b -> 'c) ->
  'a disjunction ->
  'b disjunction ->
  'c disjunction

val map_conjunction : ('a -> 'b) -> 'a conjunction -> 'b conjunction

val map_disjunction : ('a -> 'b) -> 'a disjunction -> 'b disjunction

val map_cnf : ('a -> 'b) -> 'a cnf -> 'b cnf

val map_dnf : ('a -> 'b) -> 'a dnf -> 'b dnf

val map_tree : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) tree -> ('c, 'd) tree

val print_conjunction : 
  ?firstconj:(unit, Format.formatter, unit) format ->
  ?sepconj:(unit, Format.formatter, unit) format ->
  ?lastconj:(unit, Format.formatter, unit) format ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a conjunction ->
  unit

val print_disjunction : 
  ?firstdisj:(unit, Format.formatter, unit) format ->
  ?sepdisj:(unit, Format.formatter, unit) format ->
  ?lastdisj:(unit, Format.formatter, unit) format ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a disjunction ->
  unit

val print_cnf : 
  ?firstconj:(unit, Format.formatter, unit) format ->
  ?sepconj:(unit, Format.formatter, unit) format ->
  ?lastconj:(unit, Format.formatter, unit) format ->
  ?firstdisj:(unit, Format.formatter, unit) format ->
  ?sepdisj:(unit, Format.formatter, unit) format ->
  ?lastdisj:(unit, Format.formatter, unit) format ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a cnf ->
  unit

val print_dnf : 
  ?firstdisj:(unit, Format.formatter, unit) format ->
  ?sepdisj:(unit, Format.formatter, unit) format ->
  ?lastdisj:(unit, Format.formatter, unit) format ->
  ?firstconj:(unit, Format.formatter, unit) format ->
  ?sepconj:(unit, Format.formatter, unit) format ->
  ?lastconj:(unit, Format.formatter, unit) format ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a dnf ->
  unit

val print_tree_minterm : 
  ?compare:'a PHashhe.compare ->
  (Format.formatter -> ('b * bool) dnf -> unit) ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  ('b, 'a) tree ->
  unit

val print_tree : 
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ('a, 'b) tree ->
  unit

package bddapron