Module Bdd.Domain0.O

module O: sig .. end

val print : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> 'd Bdd.Domain0.t -> unit

val bottom : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t

val top : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t

Constructors

val is_bottom : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> bool

val is_top : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> bool

val is_leq : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> bool

val is_eq : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> bool

val is_variable_unconstrained : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'a -> bool

Tests

val meet : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> 'd Bdd.Domain0.t

val join : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> 'd Bdd.Domain0.t

val meet_condition : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'd Bdd.Expr0.Bool.t -> 'd Bdd.Domain0.t

Lattice operations

val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Expr0.expr list -> 'd Bdd.Domain0.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, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Expr0.expr list -> 'd Bdd.Domain0.t

Substitution

val forget_list : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Domain0.t

Eliminating variables

module Asssub: sig .. end

val relation_supp_compose_of_lvarlexpr : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a list ->
       'd Bdd.Expr0.expr list -> 'd Cudd.Bdd.t * 'd Cudd.Bdd.t * 'd Cudd.Bdd.t array

val apply_change : 'a Bdd.Domain0.t -> 'a Bdd.Env.change -> 'a Bdd.Domain0.t