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
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
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

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
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