Module Bddvar.Expr

module Expr: sig .. end

Syntax tree for printing

type atom =

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

Atom

type term =

`\|`	`Tatom of atom`	`(*`	A true boolean indicates a primed variable	`*)`
`\|`	`Texternal of int * bool`	`(*`	Unregistered BDD identifier and a Boolean for possible negation	`*)`
`\|`	`Tcst of bool`	`(*`	Boolean constant	`*)`

Basic term

type conjunction =

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

Conjunction

type disjunction =

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

Disjunction

val term_of_vint : Var.t -> Bddint.t -> Bddreg.Minterm.t -> term

val term_of_venum : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Var.t -> Bddenum.t -> Bddreg.Minterm.t -> term

val term_of_idcondb : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       MappeI.key * bool -> term

val bool_of_tbool : Manager.tbool -> bool

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

Raises Exit if false value

val conjunction_of_minterm : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Manager.tbool array -> conjunction

val disjunction_of_bdd : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Bdd.t -> disjunction

val print_term : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Format.formatter -> term -> unit

val print_conjunction : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Format.formatter -> conjunction -> unit

val print_disjunction : ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
       Format.formatter -> disjunction -> unit