Module Bdd.Domain1

module Domain1: sig .. end

Abstract domain

type ('a, 'b) t = ('a, 'b) Bdd.Expr1.Bool.t

Abstract value

type 'a dt = ('a, Cudd.Man.d) t

type 'a vt = ('a, Cudd.Man.v) t

val of_domain0 : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> ('a, 'b) t

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

val to_domain0 : ('a, 'b) t -> 'b Bdd.Domain0.t

Conversion operations

val of_expr1 : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) t

val to_expr1 : ('a, 'b) t -> ('a, 'b) Bdd.Expr1.Bool.t

Conversion operations

val size : ('a, 'b) t -> int

Size of an abstract value (number of nodes)

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

val bottom : ('a, 'b) Bdd.Env.t -> ('a, 'b) t

val top : ('a, 'b) Bdd.Env.t -> ('a, 'b) t

Constructors

val is_bottom : ('a, 'b) t -> bool

val is_top : ('a, 'b) t -> bool

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

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

val is_variable_unconstrained : ('a, 'b) t -> 'a -> bool

Tests

val meet : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val join : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val meet_condition : ('a, 'b) t -> ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) t

Lattice operations

val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b) t ->
       'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) t

val assign_listexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b) t ->
       'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) t

Assignement

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

If rel=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) t ->
       'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) t

val substitute_listexpr : ('a, 'b) t ->
       'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) t

Substitution

val forget_list : ('a, 'b) t -> 'a list -> ('a, 'b) t

Eliminating variables

val change_environment : ('a, 'b) t -> ('a, 'b) Bdd.Env.t -> ('a, 'b) t

val rename : ('a, 'b) t -> ('a * 'a) list -> ('a, 'b) t

Change of environments

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