Module Bdd.Expr0.O.Expr

module Expr: sig .. end

Syntax tree for printing

type 'a atom =

`\|`	`Tbool of 'a * bool`	`(*`	variable name and sign	`*)`
`\|`	`Tint of 'a * int list`	`(*`	variable name and list of possible values	`*)`
`\|`	`Tenum of 'a * 'a list`	`(*`	variable name, possibly primed, and list of possible labels	`*)`

Atom

type 'a term =

`\|`	`Tatom of 'a atom`
`\|`	`Texternal of (int * bool)`	`(*`	Unregistered BDD identifier and a Boolean for possible negation	`*)`
`\|`	`Tcst of bool`	`(*`	Boolean constant	`*)`

Basic term

val map_atom : ('a -> 'b) -> 'a atom -> 'b atom

val map_term : ('a -> 'b) -> 'a term -> 'b term

val term_of_vint : 'a -> 'd Bdd.Int.t -> Bdd.Reg.Minterm.t -> 'a term

val term_of_venum : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a -> 'd Bdd.Enum.t -> Bdd.Reg.Minterm.t -> 'a term

val term_of_idcondb : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       int * bool -> 'a term

val bool_of_tbool : Cudd.Man.tbool -> bool

val mand : 'a term list Pervasives.ref ->
       'a term -> unit

val conjunction_of_minterm : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Cudd.Man.tbool array -> 'a term Bdd.Normalform.conjunction

val dnf_of_bdd : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Cudd.Bdd.t -> 'a term Bdd.Normalform.dnf

val print_term : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> 'a term -> unit

val print_conjunction : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter ->
       'a term Bdd.Normalform.conjunction -> unit

val print_dnf : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> 'a term Bdd.Normalform.dnf -> unit