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

Constructors

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

Tests

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

Assignement

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

Substitution

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