Module Domain1.O

module O: sig .. end

val check_value : ('a -> int array -> 'a) ->
       (('b, [> 'b Env.typ ] as 'c, [> 'b Env.typdef ] as 'd, 'e, 'f) Env.O.t, 'a)
       Env.value -> ('b, 'c, 'd, 'e, 'f) Env.O.t -> 'a

val check_lvalue : ('a -> int array -> 'a) ->
       (('b, [> 'b Env.typ ] as 'c, [> 'b Env.typdef ] as 'd, 'e, 'f) Env.O.t, 'a)
       Env.value list -> ('b, 'c, 'd, 'e, 'f) Env.O.t -> 'a list

type ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b) t = ('a, ('a, [> 'a Env.typ ] as 'd, [> 'a Env.typdef ] as 'e, 'b, 'c) Env.O.t,
        'b)
       Expr1.O.Bool.t

type ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], Cudd.Man.d, 'b) Env.O.t) dt = ('a,
        ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, Cudd.Man.d, 'b)
        Env.O.t, Cudd.Man.d)
       t

type ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], Cudd.Man.v, 'b) Env.O.t) vt = ('a,
        ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, Cudd.Man.v, 'b)
        Env.O.t, Cudd.Man.v)
       t

val of_domain0 : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
       'd Domain0.t -> ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

val get_env : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t -> ('a, 'b, 'c, 'd, 'e) Env.O.t

val to_domain0 : ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> 'b Domain0.t

val of_expr1 : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       Expr1.O.Bool.t -> ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

val to_expr1 : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t -> ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.Bool.t

val size : ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> int

val print : Format.formatter ->
       ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> unit

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

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

Constructors

val is_bottom : ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> bool

val is_top : ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> bool

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

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

val is_variable_unconstrained : ('a, ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t, 'b)
       t -> 'a -> bool

Tests

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

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

val meet_condition : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.Bool.t ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

Lattice operations

val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       'a list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.t list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

val assign_listexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       'a list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.List.t ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

Assignement

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, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       'a list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.t list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

val substitute_listexpr : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       'a list ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) Expr1.O.List.t ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

Substitution

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

Eliminating variables

val change_environment : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       ('a, 'b, 'c, 'd, 'e) Env.O.t ->
       ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

val rename : ('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
        'd)
       t ->
       ('a * 'a) list -> ('a, ('a, 'b, 'c, 'd, 'e) Env.O.t, 'd) t

Change of environments