Module 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

type 'a conjunction =

`\|`	`Conjunction of 'a term list`	`(*`	Conjunction of terms. Empty list means true.	`*)`
`\|`	`Cfalse`

Conjunction

type 'a disjunction =

`\|`	`Disjunction of 'a conjunction list`	`(*`	Disjunction of conjunctions. Empty list means false	`*)`
`\|`	`Dtrue`

Disjunction

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

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

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

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

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

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

val term_of_idcondb : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) 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 Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       Cudd.Man.tbool array -> 'a conjunction

val disjunction_of_bdd : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b Cudd.Bdd.t -> 'a disjunction

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

val print_conjunction : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       Format.formatter -> 'a conjunction -> unit

val print_disjunction : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       Format.formatter -> 'a disjunction -> unit