Module Bdd.Cond

module Cond: sig .. end

Datatypes

type ('a, 'b, 'c, 'd) t = {

`symbol :'a Bdd.Env.symbol;`
`compare_cond :'c -> 'c -> int;`
`negate_cond :'b -> 'c -> 'c;`
`support_cond :'b -> 'c -> 'a PSette.t;`
`mutable print_cond :'b -> Format.formatter -> 'c -> unit;`
`mutable cudd :'d Cudd.Man.t;`	`(*`	CUDD manager	`*)`
`mutable bddindex0 :int;`	`(*`	First index for conditions	`*)`
`mutable bddsize :int;`	`(*`	Number of indices dedicated to conditions	`*)`
`mutable bddindex :int;`	`(*`	Next free index in BDDs used by `Bdd.Cond.idb_of_cond`.	`*)`
`mutable bddincr :int;`
`mutable condidb :('c, int * bool) PDMappe.t;`	`(*`	Two-way association between a condition and a pair of a BDD index and a polarity	`*)`
`mutable supp :'d Cudd.Bdd.t;`	`(*`	Support of conditions	`*)`
`mutable careset :'d Cudd.Bdd.t;`	`(*`	Boolean formula indicating which logical combination known as true could be exploited for simplification. For instance, `x>=1 => x>=0`.	`*)`

}

Printing

val print : 'b -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit

Constructors

val make : symbol:'a Bdd.Env.symbol ->
       compare_cond:('c -> 'c -> int) ->
       negate_cond:('b -> 'c -> 'c) ->
       support_cond:('b -> 'c -> 'a PSette.t) ->
       print_cond:('b -> Format.formatter -> 'c -> unit) ->
       ?bddindex0:int ->
       ?bddsize:int -> 'd Cudd.Man.t -> ('a, 'b, 'c, 'd) t

val copy : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t

Internal functions

val permutation : ('a, 'b, 'c, 'd) t -> int array

Compute the permutation for normalizing the environment

val permute_with : ('a, 'b, 'c, 'd) t -> int array -> unit

Apply the given permutation to the environment

val normalize_with : ('a, 'b, 'c, 'd) t -> int array

Combine the two previous functions, and return the permutation

val reduce_with : ('a, 'b, 'c, 'd) t -> 'd Cudd.Bdd.t -> unit

Remove from the environment all conditions that do not belong to the given support. Does not perform normalization (so there may be "holes" in the allocation of indices

val clear : ('a, 'b, 'c, 'd) t -> unit

Clear all the conditions (results in a normalized environments)

val check_normalized : 'b -> ('a, 'b, 'c, 'd) t -> bool

Operations

val cond_of_idb : ('a, 'b, 'c, 'd) t -> int * bool -> 'c

val idb_of_cond : 'a -> ('b, 'a, 'c, 'd) t -> 'c -> int * bool

val compute_careset : ('a, 'b, 'c, 'd) t -> normalized:bool -> unit

val is_leq : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> bool

val is_eq : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> bool

val shift : ('a, 'b, 'c, 'd) t -> int -> ('a, 'b, 'c, 'd) t

val lce : ('a, 'b, 'c, 'd) t ->
       ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t

val permutation12 : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> int array

val permutation21 : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> int array

Level 2

type ('a, 'b) value = {

	`cond :'a;`
	`val1 :'b;`

}

val make_value : 'a -> 'b -> ('a, 'b) value

val get_cond : ('a, 'b) value -> 'a

val get_val1 : ('a, 'b) value -> 'b

val get_env : ('a, ('b, 'c) Bdd.Env.value) value -> 'b

val get_val0 : ('a, ('b, 'c) Bdd.Env.value) value -> 'c