Up  

Module Bdd.Domain1.O

module O: sig .. end
val check_value : ('a -> int array -> 'a) ->
       (('b, [> 'b Bdd.Env.typ ] as 'c, [> 'b Bdd.Env.typdef ] as 'd, 'e, 'f)
        Bdd.Env.O.t, 'a)
       Bdd.Env.value -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a
val check_lvalue : ('a -> int array -> 'a) ->
       (('b, [> 'b Bdd.Env.typ ] as 'c, [> 'b Bdd.Env.typdef ] as 'd, 'e, 'f)
        Bdd.Env.O.t, 'a)
       Bdd.Env.value list -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a list
type ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t, 'c) t = ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'd, [> 'a Bdd.Env.typdef ] as 'e, 'c, 'b)
        Bdd.Env.O.t, 'c)
       Bdd.Expr1.O.Bool.t 
type ('a
       , ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], Cudd.Man.d, 'b)
         Bdd.Env.O.t) dt = ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.d,
         'b)
        Bdd.Env.O.t, Cudd.Man.d)
       t 
type ('a
       , ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], Cudd.Man.v, 'b)
         Bdd.Env.O.t) vt = ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.v,
         'b)
        Bdd.Env.O.t, Cudd.Man.v)
       t 
val of_domain0 : ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
       Bdd.Env.O.t ->
       'c Bdd.Domain0.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val get_env : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_domain0 : ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> 'c Bdd.Domain0.t
val of_expr1 : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       Bdd.Expr1.O.Bool.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val to_expr1 : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val size : ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> int
val print : Format.formatter ->
       ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> unit
val bottom : ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
       Bdd.Env.O.t -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val top : ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
       Bdd.Env.O.t -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
Constructors
val is_bottom : ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> bool
val is_top : ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> bool
val is_leq : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t -> bool
val is_eq : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t -> bool
val is_variable_unconstrained : ('a, ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
        'c)
       t -> 'a -> bool
Tests
val meet : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val join : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val meet_condition : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
Lattice operations
val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       'a list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val assign_listexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       'a list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) 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 Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       'a list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val substitute_listexpr : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       'a list ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
Substitution
val forget_list : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       'a list -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
Eliminating variables
val change_environment : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
       ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
val rename : ('a,
        ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
        Bdd.Env.O.t, 'c)
       t ->
       ('a * 'a) list -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) t
Change of environments