Module Bdd.Domain0

module Domain0: sig .. end

Abstract domain

type 'a t = 'a Bdd.Expr0.Bool.t 
Abstract value
type dt = Cudd.Man.d t 
type vt = Cudd.Man.v t 
val size : 'a t -> int
Size of an abstract value (number of nodes)
val print : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b t -> unit
val bottom : ('a, 'b) Bdd.Env.t -> 'b t
val top : ('a, 'b) Bdd.Env.t -> 'b t
val is_bottom : ('a, 'b) Bdd.Env.t -> 'b t -> bool
val is_top : ('a, 'b) Bdd.Env.t -> 'b t -> bool
val is_leq : ('a, 'b) Bdd.Env.t -> 'b t -> 'b t -> bool
val is_eq : ('a, 'b) Bdd.Env.t -> 'b t -> 'b t -> bool
val is_variable_unconstrained : ('a, 'b) Bdd.Env.t -> 'b t -> 'a -> bool
val meet : ('a, 'b) Bdd.Env.t ->
'b t -> 'b t -> 'b t
val join : ('a, 'b) Bdd.Env.t ->
'b t -> 'b t -> 'b t
val meet_condition : ('a, 'b) Bdd.Env.t ->
'b t -> 'b Bdd.Expr0.Bool.t -> 'b t
Lattice operations
val assign_lexpr : ?relational:bool ->
?nodependency:bool ->
('a, 'b) Bdd.Env.t ->
'b t -> 'a list -> 'b Bdd.Expr0.expr list -> 'b t

If nodependency=true, which means that no expression depends on the assigned variables, it uses an optimized algorithm.

If relational=true, it is assumed that env#bddincr=2 (checked), starting from a pair index. It is also advised to have paired variables in groups.

rel=true is most probably much better for assignements of a few variables.

val substitute_lexpr : ('a, 'b) Bdd.Env.t ->
'b t -> 'a list -> 'b Bdd.Expr0.expr list -> 'b t
val forget_list : ('a, 'b) Bdd.Env.t -> 'b t -> 'a list -> 'b t
Eliminating variables

Opened signature and Internal functions

We provide here the same functions and modules as before, but with opened types (this allows etxensions). The functions above are axtually derived from the functions below by just constraining their types. We provide here also more internal functions
module O: sig .. end