sig
module Output :
sig
type bnode = BIte of int * int * bool * int | BTrue
type 'a bdd = {
cond : int PSette.t Pervasives.ref;
mutable bdef : (int, Bdd.Output.bnode) PMappe.t;
bhash : ('a Cudd.Bdd.t, int) Hashhe.t;
mutable blastid : int;
}
type 'a vnode = VIte of int * int * int | VCst of 'a
type 'a vdd = {
cond : int PSette.t Pervasives.ref;
mutable vdef : (int, 'a Bdd.Output.vnode) PMappe.t;
lhash : ('a, unit) PHashhe.t;
vhash : ('a Cudd.Vdd.t, int) Hashhe.t;
mutable vlastid : int;
}
type anode = AIte of int * int * int | ACst of float
type add = {
cond : int PSette.t Pervasives.ref;
mutable adef : (int, Bdd.Output.anode) PMappe.t;
mutable lset : float Sette.t;
ahash : (Cudd.Add.t, int) Hashhe.t;
mutable alastid : int;
}
val make_bdd : cond:int PSette.t Pervasives.ref -> 'a Bdd.Output.bdd
val signid_of_bdd : 'a Bdd.Output.bdd -> 'a Cudd.Bdd.t -> bool * int
val make_vdd :
compare:'a Cudd.PWeakke.compare ->
cond:int PSette.t Pervasives.ref -> 'a Bdd.Output.vdd
val make_mtbdd :
table:'a Cudd.Mtbdd.table ->
cond:int PSette.t Pervasives.ref ->
'a Cudd.Mtbdd.unique Bdd.Output.vdd
val make_mtbddc :
table:'a Cudd.Mtbddc.table ->
cond:int PSette.t Pervasives.ref ->
'a Cudd.Mtbddc.unique Bdd.Output.vdd
val id_of_vdd : 'a Bdd.Output.vdd -> 'a Cudd.Vdd.t -> int
val iter_cond_ordered :
int PSette.t -> 'a Cudd.Man.t -> (int -> unit) -> unit
val iter_bdef_ordered :
'a Bdd.Output.bdd -> (int -> Bdd.Output.bnode -> unit) -> unit
val iter_vdef_ordered :
'a Bdd.Output.vdd -> (int -> 'a Bdd.Output.vnode -> unit) -> unit
end
module Normalform :
sig
type 'a conjunction = Conjunction of 'a list | Cfalse
type 'a disjunction = Disjunction of 'a list | Dtrue
type 'a cnf = 'a Bdd.Normalform.disjunction Bdd.Normalform.conjunction
type 'a dnf = 'a Bdd.Normalform.conjunction Bdd.Normalform.disjunction
type ('a, 'b) tree =
('a * bool) list * ('a, 'b) Bdd.Normalform.decision
and ('a, 'b) decision =
Leaf of 'b
| Ite of 'a * ('a, 'b) Bdd.Normalform.tree *
('a, 'b) Bdd.Normalform.tree
val conjunction_false : 'a Bdd.Normalform.conjunction
val conjunction_true : 'a Bdd.Normalform.conjunction
val disjunction_false : 'a Bdd.Normalform.disjunction
val disjunction_true : 'a Bdd.Normalform.disjunction
val cnf_false : 'a Bdd.Normalform.cnf
val cnf_true : 'a Bdd.Normalform.cnf
val dnf_false : 'a Bdd.Normalform.dnf
val dnf_true : 'a Bdd.Normalform.dnf
val conjunction_and :
?merge:('a list -> 'a list -> 'a list) ->
'a Bdd.Normalform.conjunction ->
'a Bdd.Normalform.conjunction -> 'a Bdd.Normalform.conjunction
val disjunction_or :
?merge:('a list -> 'a list -> 'a list) ->
'a Bdd.Normalform.disjunction ->
'a Bdd.Normalform.disjunction -> 'a Bdd.Normalform.disjunction
val conjunction_and_term :
'a Bdd.Normalform.conjunction -> 'a -> 'a Bdd.Normalform.conjunction
val disjunction_or_term :
'a Bdd.Normalform.disjunction -> 'a -> 'a Bdd.Normalform.disjunction
val minterm_of_tree :
?compare:'b PHashhe.compare ->
('a, 'b) Bdd.Normalform.tree ->
(('a * bool) Bdd.Normalform.dnf * 'b) list
val rev_map_conjunction :
('a -> 'b) ->
'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
val rev_map_disjunction :
('a -> 'b) ->
'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
val rev_map2_conjunction :
('a -> 'b -> 'c) ->
'a Bdd.Normalform.conjunction ->
'b Bdd.Normalform.conjunction -> 'c Bdd.Normalform.conjunction
val rev_map2_disjunction :
('a -> 'b -> 'c) ->
'a Bdd.Normalform.disjunction ->
'b Bdd.Normalform.disjunction -> 'c Bdd.Normalform.disjunction
val map_conjunction :
('a -> 'b) ->
'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
val map_disjunction :
('a -> 'b) ->
'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
val map_cnf :
('a -> 'b) -> 'a Bdd.Normalform.cnf -> 'b Bdd.Normalform.cnf
val map_dnf :
('a -> 'b) -> 'a Bdd.Normalform.dnf -> 'b Bdd.Normalform.dnf
val map_tree :
('a -> 'c) ->
('b -> 'd) ->
('a, 'b) Bdd.Normalform.tree -> ('c, 'd) Bdd.Normalform.tree
val print_conjunction :
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.conjunction -> unit
val print_disjunction :
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.disjunction -> unit
val print_cnf :
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.cnf -> unit
val print_dnf :
?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Bdd.Normalform.dnf -> unit
val print_tree_minterm :
?compare:'a PHashhe.compare ->
(Format.formatter -> ('b * bool) Bdd.Normalform.dnf -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> ('b, 'a) Bdd.Normalform.tree -> unit
val print_tree :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) Bdd.Normalform.tree -> unit
end
module Reg :
sig
type 'a t = 'a Cudd.Bdd.t array
type dt = Cudd.Man.d Bdd.Reg.t
type vt = Cudd.Man.v Bdd.Reg.t
val lnot : 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val shift_left :
'a Cudd.Man.t -> int -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t
val shift_right :
'a Cudd.Man.t -> int -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t
val shift_right_logical :
'a Cudd.Man.t -> int -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t
val extend :
'a Cudd.Man.t -> signed:bool -> int -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val succ :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t
val pred :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t
val add :
'a Cudd.Man.t ->
'a Bdd.Reg.t ->
'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
val sub :
'a Cudd.Man.t ->
'a Bdd.Reg.t ->
'a Bdd.Reg.t -> 'a Bdd.Reg.t * 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
val neg : 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val scale : int -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val mul : 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val ite : 'a Cudd.Bdd.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val is_cst : 'a Bdd.Reg.t -> bool
val zero : 'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val equal :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val greatereq :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val greater :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val highereq :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val higher :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t -> 'a Cudd.Bdd.t
val min_size : int -> int
val of_int : 'a Cudd.Man.t -> int -> int -> 'a Bdd.Reg.t
val to_int : signed:bool -> 'a Bdd.Reg.t -> int
val equal_int : 'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
val greatereq_int :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
val greater_int : 'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
val highereq_int :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
val higher_int : 'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
module Minterm :
sig
type t = Cudd.Man.tbool array
val is_indet : Bdd.Reg.Minterm.t -> bool
val of_int : int -> int -> Bdd.Reg.Minterm.t
val to_int : signed:bool -> Bdd.Reg.Minterm.t -> int
val iter : (Bdd.Reg.Minterm.t -> unit) -> Bdd.Reg.Minterm.t -> unit
val map : (Bdd.Reg.Minterm.t -> 'a) -> Bdd.Reg.Minterm.t -> 'a list
end
val guard_of_minterm :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> Bdd.Reg.Minterm.t -> 'a Cudd.Bdd.t
val guard_of_int :
'a Cudd.Man.t -> 'a Bdd.Reg.t -> int -> 'a Cudd.Bdd.t
val guardints :
'a Cudd.Man.t ->
signed:bool -> 'a Bdd.Reg.t -> ('a Cudd.Bdd.t * int) list
val cofactor : 'a Bdd.Reg.t -> 'a Cudd.Bdd.t -> 'a Bdd.Reg.t
val restrict : 'a Bdd.Reg.t -> 'a Cudd.Bdd.t -> 'a Bdd.Reg.t
val tdrestrict : 'a Bdd.Reg.t -> 'a Cudd.Bdd.t -> 'a Bdd.Reg.t
val print :
(Format.formatter -> int -> unit) ->
Format.formatter -> 'a Bdd.Reg.t -> unit
val print_minterm :
signed:bool ->
(Format.formatter -> 'a Cudd.Bdd.t -> unit) ->
Format.formatter -> 'a Bdd.Reg.t -> unit
val permute :
?memo:Cudd.Memo.t -> 'a Bdd.Reg.t -> int array -> 'a Bdd.Reg.t
val varmap : 'a Bdd.Reg.t -> 'a Bdd.Reg.t
val vectorcompose :
?memo:Cudd.Memo.t ->
'a Cudd.Bdd.t array -> 'a Bdd.Reg.t -> 'a Bdd.Reg.t
end
module Env :
sig
exception Bddindex
type 'a typdef = [ `Benum of 'a array ]
type 'a typ = [ `Benum of 'a | `Bint of bool * int | `Bool ]
type 'a symbol = {
compare : 'a -> 'a -> int;
marshal : 'a -> string;
unmarshal : string -> 'a;
mutable print : Format.formatter -> 'a -> unit;
}
type ('a, 'b, 'c, 'd, 'e) t0 = {
mutable cudd : 'd Cudd.Man.t;
mutable typdef : ('a, 'c) PMappe.t;
mutable vartyp : ('a, 'b) PMappe.t;
mutable bddindex0 : int;
mutable bddsize : int;
mutable bddindex : int;
mutable bddincr : int;
mutable idcondvar : (int, 'a) PMappe.t;
mutable vartid : ('a, int array) PMappe.t;
mutable varset : ('a, 'd Cudd.Bdd.t) PMappe.t;
mutable print_external_idcondb :
Format.formatter -> int * bool -> unit;
mutable ext : 'e;
symbol : 'a Bdd.Env.symbol;
copy_ext : 'e -> 'e;
}
module O :
sig
type ('a, 'b, 'c, 'd, 'e) t = ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0
constraint 'b = [> 'a Bdd.Env.typ ]
constraint 'c = [> 'a Bdd.Env.typdef ]
val make :
symbol:'a Bdd.Env.symbol ->
copy_ext:('e -> 'e) ->
?bddindex0:int ->
?bddsize:int ->
?relational:bool ->
'd Cudd.Man.t ->
'e ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t
val print :
(Format.formatter -> ([> 'a Bdd.Env.typ ] as 'b) -> unit) ->
(Format.formatter -> ([> 'a Bdd.Env.typdef ] as 'c) -> unit) ->
(Format.formatter -> 'e -> unit) ->
Format.formatter -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> unit
end
type ('a, 'd) t =
('a, 'a Bdd.Env.typ, 'a Bdd.Env.typdef, 'd, unit) Bdd.Env.O.t
val print_typ :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> [> 'a Bdd.Env.typ ] -> unit
val print_typdef :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> [> 'a Bdd.Env.typdef ] -> unit
val print_tid : Format.formatter -> int array -> unit
val print_idcondb :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
Format.formatter -> int * bool -> unit
val print_order :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
Format.formatter -> unit
val print :
Format.formatter ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
unit
val marshal : 'a -> string
val unmarshal : string -> 'a
val make_symbol :
?compare:('a -> 'a -> int) ->
?marshal:('a -> string) ->
?unmarshal:(string -> 'a) ->
(Format.formatter -> 'a -> unit) -> 'a Bdd.Env.symbol
val string_symbol : string Bdd.Env.symbol
val make :
symbol:'a Bdd.Env.symbol ->
?bddindex0:int ->
?bddsize:int ->
?relational:bool -> 'd Cudd.Man.t -> ('a, 'd) Bdd.Env.t
val make_string :
?bddindex0:int ->
?bddsize:int ->
?relational:bool -> 'd Cudd.Man.t -> (string, 'd) Bdd.Env.t
val copy :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val mem_typ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> bool
val mem_var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> bool
val mem_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> bool
val typdef_of_typ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ] as 'b, 'd, 'e)
Bdd.Env.O.t -> 'a -> 'b
val typ_of_var :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'b
val vars :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a PSette.t
val labels :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a PSette.t
val add_typ_with :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ] as 'b, 'd, 'e)
Bdd.Env.O.t -> 'a -> 'b -> unit
val add_vars_with :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> ('a * 'b) list -> int array option
val remove_vars_with :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a list -> int array option
val rename_vars_with :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
('a * 'a) list -> int array option
val add_typ :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val add_vars :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val remove_vars :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> 'a list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val rename_vars :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val add_var_with :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'b -> unit
val iter_ordered :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
('a -> int array -> unit) -> unit
val is_leq :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
val is_eq :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
val shift :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> int -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val lce :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
val permutation12 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
val permutation21 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
type 'a change = {
intro : int array option;
remove : ('a Cudd.Bdd.t * int array) option;
}
val compute_change :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> 'd Bdd.Env.change
val notfound :
('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
type ('a, 'b) value = { env : 'a; val0 : 'b; }
val make_value :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
'f -> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
val get_env : ('a, 'b) Bdd.Env.value -> 'a
val get_val0 : ('a, 'b) Bdd.Env.value -> 'b
val extend_environment :
('f -> int array -> 'f) ->
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value ->
('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
val compare_idb : int * bool -> int * bool -> int
val permutation :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
int array
val permute_with :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
int array -> unit
val normalize_with :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
int array
val check_normalized :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
bool
val compose_permutation : int array -> int array -> int array
val compose_opermutation :
int array option -> int array option -> int array option
val permutation_of_offset : int -> int -> int array
val check_var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> unit
val check_lvar :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a list -> unit
val check_value :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value -> unit
val check_value2 :
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value -> unit
val check_value3 :
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value -> unit
val check_lvarvalue :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
('a * (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value) list ->
('a * 'f) list
val check_lvalue :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value list -> 'f list
val check_ovalue :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
Bdd.Env.O.t ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value option ->
'f option
val mapunop :
('f -> 'g) ->
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value -> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value
val mapbinop :
('f -> 'g -> 'h) ->
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
val mapbinope :
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t -> 'f -> 'g -> 'h) ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
val mapterop :
('f -> 'g -> 'h -> 'i) ->
(('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd,
'e)
Bdd.Env.O.t, 'f)
Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value ->
(('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'i) Bdd.Env.value
end
module Int :
sig
type 'a t = { signed : bool; reg : 'a Cudd.Bdd.t array; }
type dt = Cudd.Man.d Bdd.Int.t
type vt = Cudd.Man.v Bdd.Int.t
exception Typing of string
val extend : 'a Cudd.Man.t -> int -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val neg : 'a Bdd.Int.t -> 'a Bdd.Int.t
val succ : 'a Bdd.Int.t -> 'a Bdd.Int.t
val pred : 'a Bdd.Int.t -> 'a Bdd.Int.t
val add : 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val sub : 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val mul : 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val shift_left : int -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val shift_right : int -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val scale : int -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val ite : 'a Cudd.Bdd.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t
val is_cst : 'a Bdd.Int.t -> bool
val zero : 'a Cudd.Man.t -> 'a Bdd.Int.t -> 'a Cudd.Bdd.t
val equal :
'a Cudd.Man.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Cudd.Bdd.t
val greatereq :
'a Cudd.Man.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Cudd.Bdd.t
val greater :
'a Cudd.Man.t -> 'a Bdd.Int.t -> 'a Bdd.Int.t -> 'a Cudd.Bdd.t
val of_int : 'a Cudd.Man.t -> bool -> int -> int -> 'a Bdd.Int.t
val to_int : 'a Bdd.Int.t -> int
val equal_int : 'a Cudd.Man.t -> 'a Bdd.Int.t -> int -> 'a Cudd.Bdd.t
val greatereq_int :
'a Cudd.Man.t -> 'a Bdd.Int.t -> int -> 'a Cudd.Bdd.t
val greater_int : 'a Cudd.Man.t -> 'a Bdd.Int.t -> int -> 'a Cudd.Bdd.t
module Minterm :
sig
val iter :
signed:bool -> (int -> unit) -> Bdd.Reg.Minterm.t -> unit
val map :
signed:bool -> (int -> 'a) -> Bdd.Reg.Minterm.t -> 'a list
end
val guard_of_int :
'a Cudd.Man.t -> 'a Bdd.Int.t -> int -> 'a Cudd.Bdd.t
val guardints :
'a Cudd.Man.t -> 'a Bdd.Int.t -> ('a Cudd.Bdd.t * int) list
val cofactor : 'a Bdd.Int.t -> 'a Cudd.Bdd.t -> 'a Bdd.Int.t
val restrict : 'a Bdd.Int.t -> 'a Cudd.Bdd.t -> 'a Bdd.Int.t
val tdrestrict : 'a Bdd.Int.t -> 'a Cudd.Bdd.t -> 'a Bdd.Int.t
val print :
(Format.formatter -> int -> unit) ->
Format.formatter -> 'a Bdd.Int.t -> unit
val print_minterm :
(Format.formatter -> 'a Cudd.Bdd.t -> unit) ->
Format.formatter -> 'a Bdd.Int.t -> unit
val permute :
?memo:Cudd.Memo.t -> 'a Bdd.Int.t -> int array -> 'a Bdd.Int.t
val varmap : 'a Bdd.Int.t -> 'a Bdd.Int.t
val vectorcompose :
?memo:Cudd.Memo.t ->
'a Cudd.Bdd.t array -> 'a Bdd.Int.t -> 'a Bdd.Int.t
end
module Enum :
sig
type 'a typ = [ `Benum of 'a ]
type 'a typdef = [ `Benum of 'a array ]
type 'a t = { typ : string; reg : 'a Bdd.Reg.t; }
type dt = Cudd.Man.d Bdd.Enum.t
type vt = Cudd.Man.v Bdd.Enum.t
val of_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> 'd Bdd.Enum.t
val is_cst : 'd Bdd.Enum.t -> bool
val to_code : 'd Bdd.Enum.t -> int
val to_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'd Bdd.Enum.t -> 'a
val equal_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'd Bdd.Enum.t -> 'a -> 'd Cudd.Bdd.t
val equal :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'd Bdd.Enum.t -> 'd Bdd.Enum.t -> 'd Cudd.Bdd.t
val ite :
'd Cudd.Bdd.t -> 'd Bdd.Enum.t -> 'd Bdd.Enum.t -> 'd Bdd.Enum.t
val guard_of_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'd Bdd.Enum.t -> 'a -> 'd Cudd.Bdd.t
val guardlabels :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'd Bdd.Enum.t -> ('d Cudd.Bdd.t * 'a) list
val cofactor : 'd Bdd.Enum.t -> 'd Cudd.Bdd.t -> 'd Bdd.Enum.t
val restrict : 'd Bdd.Enum.t -> 'd Cudd.Bdd.t -> 'd Bdd.Enum.t
val tdrestrict : 'd Bdd.Enum.t -> 'd Cudd.Bdd.t -> 'd Bdd.Enum.t
val print :
(Format.formatter -> int -> unit) ->
Format.formatter -> 'd Bdd.Enum.t -> unit
val print_minterm :
(Format.formatter -> 'd Cudd.Bdd.t -> unit) ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
Format.formatter -> 'd Bdd.Enum.t -> unit
val size_of_typ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> int
val maxcode_of_typ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> int
val mem_typcode :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> int -> bool
val labels_of_typ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> 'a array
val code_of_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> int
val label_of_typcode :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
'a -> int -> 'a
module Minterm :
sig
val iter :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> ('a -> unit) -> Bdd.Reg.Minterm.t -> unit
val map :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> ('a -> 'f) -> Bdd.Reg.Minterm.t -> 'f list
end
val permute :
?memo:Cudd.Memo.t -> 'a Bdd.Enum.t -> int array -> 'a Bdd.Enum.t
val varmap : 'a Bdd.Enum.t -> 'a Bdd.Enum.t
val vectorcompose :
?memo:Cudd.Memo.t ->
'a Cudd.Bdd.t array -> 'a Bdd.Enum.t -> 'a Bdd.Enum.t
end
module Cond :
sig
type ('a, 'b, 'c, 'd) t = {
symbol : 'a Bdd.Env.symbol;
compare_cond : 'c -> 'c -> int;
negate_cond : 'b -> 'c -> 'c;
support_cond : 'b -> 'c -> 'a PSette.t;
mutable print_cond : 'b -> Format.formatter -> 'c -> unit;
mutable cudd : 'd Cudd.Man.t;
mutable bddindex0 : int;
mutable bddsize : int;
mutable bddindex : int;
mutable bddincr : int;
mutable condidb : ('c, int * bool) PDMappe.t;
mutable supp : 'd Cudd.Bdd.t;
mutable careset : 'd Cudd.Bdd.t;
}
val print :
'b -> Format.formatter -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> unit
val make :
symbol:'a Bdd.Env.symbol ->
compare_cond:('c -> 'c -> int) ->
negate_cond:('b -> 'c -> 'c) ->
support_cond:('b -> 'c -> 'a PSette.t) ->
print_cond:('b -> Format.formatter -> 'c -> unit) ->
?bddindex0:int ->
?bddsize:int -> 'd Cudd.Man.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
val copy : ('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
val permutation : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
val permute_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array -> unit
val normalize_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
val reduce_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> 'd Cudd.Bdd.t -> unit
val clear : ('a, 'b, 'c, 'd) Bdd.Cond.t -> unit
val check_normalized : 'b -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
val cond_of_idb : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int * bool -> 'c
val idb_of_cond : 'a -> ('b, 'a, 'c, 'd) Bdd.Cond.t -> 'c -> int * bool
val compute_careset :
('a, 'b, 'c, 'd) Bdd.Cond.t -> normalized:bool -> unit
val is_leq :
('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
val is_eq :
('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
val shift :
('a, 'b, 'c, 'd) Bdd.Cond.t -> int -> ('a, 'b, 'c, 'd) Bdd.Cond.t
val lce :
('a, 'b, 'c, 'd) Bdd.Cond.t ->
('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
val permutation12 :
('a, 'b, 'c, 'd) Bdd.Cond.t ->
('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
val permutation21 :
('a, 'b, 'c, 'd) Bdd.Cond.t ->
('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
type ('a, 'b) value = { cond : 'a; val1 : 'b; }
val make_value : 'a -> 'b -> ('a, 'b) Bdd.Cond.value
val get_cond : ('a, 'b) Bdd.Cond.value -> 'a
val get_val1 : ('a, 'b) Bdd.Cond.value -> 'b
val get_env : ('a, ('b, 'c) Bdd.Env.value) Bdd.Cond.value -> 'b
val get_val0 : ('a, ('b, 'c) Bdd.Env.value) Bdd.Cond.value -> 'c
end
module Decompose :
sig
type vdd = bool Cudd.Vdd.t
val vdd_of_bdd : Cudd.Bdd.vt -> bool Cudd.Vdd.t
val bdd_of_vdd : bool Cudd.Vdd.t -> Cudd.Bdd.vt
type typ = Bool | Cond | Other
type info = {
mutable minlevelbool : int;
mutable maxlevelbool : int;
mutable minlevelcond : int;
mutable maxlevelcond : int;
varlevel : int array;
levelvar : int array;
vartyp : Bdd.Decompose.typ array;
leveltyp : Bdd.Decompose.typ array;
}
val make_info :
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, 'i) Bdd.Cond.t -> Bdd.Decompose.info
val split_level :
Cudd.Bdd.vt -> int -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val splitpermutation_of_envcond :
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, 'i) Bdd.Cond.t ->
[ `BoolCond | `CondBool ] -> int * (int array * int array) option
val split_bdd :
?memo1:Cudd.Memo.t ->
?memo2:Cudd.Memo.t ->
int * (int array * int array) option ->
Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val cube_split :
('a, 'b, 'c, 'd) Bdd.Cond.t ->
'd Cudd.Bdd.t -> 'd Cudd.Bdd.t * 'd Cudd.Bdd.t
val decompose_bdd_boolcond :
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, 'i) Bdd.Cond.t ->
Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val decompose_bdd_condbool :
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, 'i) Bdd.Cond.t ->
Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val decompose_dd_treecondbool :
?careset:'a Cudd.Bdd.t ->
topvar:('b -> int) ->
support:('b -> 'c Cudd.Bdd.t) ->
cofactor:('b -> 'a Cudd.Bdd.t -> 'b) ->
('d, 'e, 'f, 'g, 'h) Bdd.Env.t0 ->
('i, 'j, 'k, 'a) Bdd.Cond.t -> 'b -> (int, 'b) Bdd.Normalform.tree
val decompose_bdd_treecondbool :
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, 'i) Bdd.Cond.t ->
'i Cudd.Bdd.t -> (int, 'i Cudd.Bdd.t) Bdd.Normalform.tree
val decompose_vdd_treecondbool :
?careset:Cudd.Bdd.vt ->
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
'i Cudd.Vdd.t -> (int, 'i Cudd.Vdd.t) Bdd.Normalform.tree
val decompose_tbdd_tvdd_treecondbool :
?careset:Cudd.Bdd.vt ->
('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
Cudd.Bdd.vt array * 'i Cudd.Vdd.t array ->
(int, Cudd.Bdd.vt array * 'i Cudd.Vdd.t array) Bdd.Normalform.tree
val conjunction_of_minterm :
?first:int ->
?last:int ->
(int * bool -> 'a) ->
Cudd.Man.tbool array -> 'a Bdd.Normalform.conjunction
val dnf_of_bdd :
?first:int ->
?last:int ->
(int * bool -> 'a) -> 'b Cudd.Bdd.t -> 'a Bdd.Normalform.dnf
val descend :
cudd:'c Cudd.Man.t ->
maxdepth:int ->
nocare:('a -> bool) ->
cube_of_down:('a -> 'c Cudd.Bdd.t) ->
cofactor:('a -> 'c Cudd.Bdd.t -> 'a) ->
select:('a -> int) ->
terminal:(depth:int ->
newcube:'c Cudd.Bdd.t ->
cube:'c Cudd.Bdd.t -> down:'a -> 'b option) ->
ite:(depth:int ->
newcube:'c Cudd.Bdd.t ->
cond:int -> dthen:'b option -> delse:'b option -> 'b option) ->
down:'a -> 'b option
val select_cond : 'd Cudd.Bdd.t -> int
val select_cond_bdd :
('a, 'b, 'c, 'd) Bdd.Cond.t -> 'd Cudd.Bdd.t -> int
val bdd_support_cond :
('a, 'b, 'c, 'd) Bdd.Cond.t -> 'd Cudd.Bdd.t -> 'd Cudd.Bdd.t
val vdd_support_cond :
('a, 'b, 'c, Cudd.Man.v) Bdd.Cond.t -> 'd Cudd.Vdd.t -> Cudd.Bdd.vt
val tbdd_tvdd_support_cond :
('a, 'b, 'c, Cudd.Man.v) Bdd.Cond.t ->
Cudd.Bdd.vt array * 'd Cudd.Vdd.t array -> Cudd.Bdd.vt
val tbdd_tvdd_cofactor :
Cudd.Bdd.vt array * 'a Cudd.Vdd.t array ->
Cudd.Bdd.vt -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array
end
module Expr0 :
sig
type 'a t =
[ `Benum of 'a Bdd.Enum.t
| `Bint of 'a Bdd.Int.t
| `Bool of 'a Cudd.Bdd.t ]
type 'a expr = 'a Bdd.Expr0.t
type dt = Cudd.Man.d Bdd.Expr0.t
type vt = Cudd.Man.v Bdd.Expr0.t
module Bool :
sig
type 'a t = 'a Cudd.Bdd.t
type dt = Cudd.Man.d Bdd.Expr0.Bool.t
type vt = Cudd.Man.v Bdd.Expr0.Bool.t
val of_expr : 'a Bdd.Expr0.expr -> 'a Bdd.Expr0.Bool.t
val to_expr : 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.expr
val dtrue : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t
val dfalse : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t
val of_bool : ('a, 'b) Bdd.Env.t -> bool -> 'b Bdd.Expr0.Bool.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> 'b Bdd.Expr0.Bool.t
val dnot :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val dand :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val dor :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val xor :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val nand :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val nor :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val nxor :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val leq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val eq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val ite :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val is_true : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t -> bool
val is_false : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t -> bool
val is_cst : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bool.t -> bool
val is_eq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> bool
val is_leq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> bool
val is_and_false :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t -> bool
val exist :
('a, 'b) Bdd.Env.t ->
'a list -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val forall :
('a, 'b) Bdd.Env.t ->
'a list -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Expr0.Bool.t
val cofactor :
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t
val restrict :
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t
val tdrestrict :
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t
val permute :
?memo:Cudd.Memo.t ->
'a Bdd.Expr0.Bool.t -> int array -> 'a Bdd.Expr0.Bool.t
val varmap : 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> ('a * 'a) list -> 'b Bdd.Expr0.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t ->
('a * 'b Bdd.Expr0.expr) list -> 'b Bdd.Expr0.Bool.t
val print :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t ->
Format.formatter -> 'b Bdd.Expr0.Bool.t -> unit
end
module Bint :
sig
type 'a t = 'a Bdd.Int.t
type dt = Cudd.Man.d Bdd.Expr0.Bint.t
type vt = Cudd.Man.v Bdd.Expr0.Bint.t
val of_expr : 'a Bdd.Expr0.expr -> 'a Bdd.Expr0.Bint.t
val to_expr : 'a Bdd.Expr0.Bint.t -> 'a Bdd.Expr0.expr
val of_int :
('a, 'b) Bdd.Env.t ->
[ `Bint of bool * int ] -> int -> 'b Bdd.Expr0.Bint.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> 'b Bdd.Expr0.Bint.t
val ite :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val neg :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val succ :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val pred :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val add :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val sub :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val mul :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val shift_left :
('a, 'b) Bdd.Env.t ->
int -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val shift_right :
('a, 'b) Bdd.Env.t ->
int -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val scale :
('a, 'b) Bdd.Env.t ->
int -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t
val zero :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bool.t
val eq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bool.t
val eq_int :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> int -> 'b Bdd.Expr0.Bool.t
val supeq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bool.t
val supeq_int :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> int -> 'b Bdd.Expr0.Bool.t
val sup :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bint.t -> 'b Bdd.Expr0.Bool.t
val sup_int :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> int -> 'b Bdd.Expr0.Bool.t
val cofactor :
'a Bdd.Expr0.Bint.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bint.t
val restrict :
'a Bdd.Expr0.Bint.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bint.t
val tdrestrict :
'a Bdd.Expr0.Bint.t -> 'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Bint.t
val permute :
?memo:Cudd.Memo.t ->
'a Bdd.Expr0.Bint.t -> int array -> 'a Bdd.Expr0.Bint.t
val varmap : 'a Bdd.Expr0.Bint.t -> 'a Bdd.Expr0.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> ('a * 'a) list -> 'b Bdd.Expr0.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t ->
('a * 'b Bdd.Expr0.expr) list -> 'b Bdd.Expr0.Bint.t
val guard_of_int :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> int -> 'b Bdd.Expr0.Bool.t
val guardints :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> ('b Bdd.Expr0.Bool.t * int) list
val print :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t ->
Format.formatter -> 'b Bdd.Expr0.Bint.t -> unit
end
module Benum :
sig
type 'a t = 'a Bdd.Enum.t
type dt = Cudd.Man.d Bdd.Expr0.Benum.t
type vt = Cudd.Man.v Bdd.Expr0.Benum.t
val of_expr : 'a Bdd.Expr0.expr -> 'a Bdd.Expr0.Benum.t
val to_expr : 'a Bdd.Expr0.Benum.t -> 'a Bdd.Expr0.expr
val var : ('a, 'b) Bdd.Env.t -> 'a -> 'b Bdd.Expr0.Benum.t
val ite :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t ->
'b Bdd.Expr0.Benum.t ->
'b Bdd.Expr0.Benum.t -> 'b Bdd.Expr0.Benum.t
val eq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t ->
'b Bdd.Expr0.Benum.t -> 'b Bdd.Expr0.Bool.t
val eq_label :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t -> 'a -> 'b Bdd.Expr0.Bool.t
val cofactor :
'a Bdd.Expr0.Benum.t ->
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Benum.t
val restrict :
'a Bdd.Expr0.Benum.t ->
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Benum.t
val tdrestrict :
'a Bdd.Expr0.Benum.t ->
'a Bdd.Expr0.Bool.t -> 'a Bdd.Expr0.Benum.t
val permute :
?memo:Cudd.Memo.t ->
'a Bdd.Expr0.Benum.t -> int array -> 'a Bdd.Expr0.Benum.t
val varmap : 'a Bdd.Expr0.Benum.t -> 'a Bdd.Expr0.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t -> ('a * 'a) list -> 'b Bdd.Expr0.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t ->
('a * 'b Bdd.Expr0.expr) list -> 'b Bdd.Expr0.Benum.t
val guard_of_label :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t -> 'a -> 'b Bdd.Expr0.Bool.t
val guardlabels :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t -> ('b Bdd.Expr0.Bool.t * 'a) list
val print :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t ->
Format.formatter -> 'b Bdd.Expr0.Benum.t -> unit
end
val typ_of_expr :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> 'a Bdd.Env.typ
val var : ('a, 'b) Bdd.Env.t -> 'a -> 'b Bdd.Expr0.t
val ite :
'a Bdd.Expr0.Bool.t ->
'a Bdd.Expr0.t -> 'a Bdd.Expr0.t -> 'a Bdd.Expr0.t
val eq :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t -> 'b Bdd.Expr0.t -> 'b Bdd.Expr0.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t -> ('a * 'a) list -> 'b Bdd.Expr0.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t list -> ('a * 'a) list -> 'b Bdd.Expr0.t list
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t -> ('a * 'b Bdd.Expr0.t) list -> 'b Bdd.Expr0.t
val substitute_list :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t list ->
('a * 'b Bdd.Expr0.t) list -> 'b Bdd.Expr0.t list
val cofactor : 'a Bdd.Expr0.t -> 'a Cudd.Bdd.t -> 'a Bdd.Expr0.t
val restrict : 'a Bdd.Expr0.t -> 'a Cudd.Bdd.t -> 'a Bdd.Expr0.t
val tdrestrict : 'a Bdd.Expr0.t -> 'a Cudd.Bdd.t -> 'a Bdd.Expr0.t
val support : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> 'a PSette.t
val support_cond : 'a Cudd.Man.t -> 'a Bdd.Expr0.t -> 'a Cudd.Bdd.t
val cube_of_bdd : ('a, 'b) Bdd.Env.t -> 'b Cudd.Bdd.t -> 'b Cudd.Bdd.t
val print :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b Bdd.Expr0.t -> unit
val print_minterm :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t ->
Format.formatter -> Cudd.Man.tbool array -> unit
val print_bdd :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b Cudd.Bdd.t -> unit
val print_idcondb :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> int * bool -> unit
val print_idcond :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> int -> unit
module O :
sig
val tid_of_var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> int array
val reg_of_expr : 'd Bdd.Expr0.expr -> 'd Cudd.Bdd.t array
module Bool :
sig
type 'd t = 'd Cudd.Bdd.t
type dt = Cudd.Man.d Bdd.Expr0.O.Bool.t
type vt = Cudd.Man.v Bdd.Expr0.O.Bool.t
val of_expr :
[> `Bool of 'd Bdd.Expr0.O.Bool.t ] -> 'd Bdd.Expr0.O.Bool.t
val to_expr :
'd Bdd.Expr0.O.Bool.t -> [> `Bool of 'd Bdd.Expr0.O.Bool.t ]
val dtrue :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t
val dfalse :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t
val of_bool :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> bool -> 'd Bdd.Expr0.O.Bool.t
val var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'd Bdd.Expr0.O.Bool.t
val dnot :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val dand :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val dor :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val xor :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val nand :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val nor :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val nxor :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val leq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val eq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val ite :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val is_true :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val is_false :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val is_cst :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val is_eq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val is_leq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val is_and_false :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
val exist :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'a list -> 'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val forall :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'a list -> 'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val cofactor :
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val restrict :
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val tdrestrict :
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
val permute :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.O.Bool.t -> int array -> 'd Bdd.Expr0.O.Bool.t
val varmap : 'a Bdd.Expr0.O.Bool.t -> 'a Bdd.Expr0.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
('a * 'a) list -> 'd Bdd.Expr0.O.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Bool.t
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.Expr0.O.Bool.t -> unit
end
module Bint :
sig
type 'd t = 'd Bdd.Int.t
type dt = Cudd.Man.d Bdd.Expr0.O.Bint.t
type vt = Cudd.Man.v Bdd.Expr0.O.Bint.t
val of_expr :
[> `Bint of 'd Bdd.Expr0.O.Bint.t ] -> 'd Bdd.Expr0.O.Bint.t
val to_expr :
'd Bdd.Expr0.O.Bint.t -> [> `Bint of 'd Bdd.Expr0.O.Bint.t ]
val of_int :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
[> `Bint of bool * int ] -> int -> 'd Bdd.Expr0.O.Bint.t
val var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'd Bdd.Expr0.O.Bint.t
val ite :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val neg :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val succ :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val pred :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val add :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val sub :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val mul :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val shift_left :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val shift_right :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val scale :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
val zero :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
val eq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
val eq_int :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
val supeq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
val supeq_int :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
val sup :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
val sup_int :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
val cofactor :
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
val restrict :
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
val tdrestrict :
'd Bdd.Expr0.O.Bint.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
val permute :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.O.Bint.t -> int array -> 'd Bdd.Expr0.O.Bint.t
val varmap : 'a Bdd.Expr0.O.Bint.t -> 'a Bdd.Expr0.O.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
('a * 'a) list -> 'd Bdd.Expr0.O.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t ->
('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Bint.t
val guard_of_int :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
val guardints :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bint.t -> ('d Bdd.Expr0.O.Bool.t * int) list
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.Expr0.O.Bint.t -> unit
end
module Benum :
sig
type 'd t = 'd Bdd.Enum.t
type dt = Cudd.Man.d Bdd.Expr0.O.Benum.t
type vt = Cudd.Man.v Bdd.Expr0.O.Benum.t
val of_expr :
[> `Benum of 'd Bdd.Expr0.O.Benum.t ] ->
'd Bdd.Expr0.O.Benum.t
val to_expr :
'd Bdd.Expr0.O.Benum.t ->
[> `Benum of 'd Bdd.Expr0.O.Benum.t ]
val var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'd Bdd.Expr0.O.Benum.t
val ite :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.O.Benum.t ->
'd Bdd.Expr0.O.Benum.t -> 'd Bdd.Expr0.O.Benum.t
val eq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t ->
'd Bdd.Expr0.O.Benum.t -> 'd Bdd.Expr0.O.Bool.t
val eq_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t -> 'a -> 'd Bdd.Expr0.O.Bool.t
val cofactor :
'd Bdd.Expr0.O.Benum.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
val restrict :
'd Bdd.Expr0.O.Benum.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
val tdrestrict :
'd Bdd.Expr0.O.Benum.t ->
'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
val permute :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.O.Benum.t -> int array -> 'd Bdd.Expr0.O.Benum.t
val varmap : 'a Bdd.Expr0.O.Benum.t -> 'a Bdd.Expr0.O.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t ->
('a * 'a) list -> 'd Bdd.Expr0.O.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t ->
('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Benum.t
val guard_of_label :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t -> 'a -> 'd Bdd.Expr0.O.Bool.t
val guardlabels :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.O.Benum.t -> ('d Bdd.Expr0.O.Bool.t * 'a) list
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.Expr0.O.Benum.t -> unit
end
val typ_of_expr :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.t -> [> 'a Bdd.Env.typ ]
val var :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a -> 'd Bdd.Expr0.t
val ite :
'd Bdd.Expr0.O.Bool.t ->
'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.t
val eq :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.t -> ('a * 'a) list -> 'd Bdd.Expr0.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.t list -> ('a * 'a) list -> 'd Bdd.Expr0.t list
val substitute :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.t -> ('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t
val substitute_list :
?memo:Cudd.Memo.t ->
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Bdd.Expr0.t list ->
('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t list
val support :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Bdd.Expr0.t -> 'a PSette.t
val support_cond : 'd Cudd.Man.t -> 'd Bdd.Expr0.t -> 'd Cudd.Bdd.t
val cube_of_bdd :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'd Cudd.Bdd.t -> 'd Cudd.Bdd.t
val tbdd_of_texpr : 'd Bdd.Expr0.t array -> 'd Cudd.Bdd.t array
val texpr_of_tbdd :
'd Bdd.Expr0.t array ->
'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t array
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.Expr0.t ] -> unit
val print_minterm :
?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 -> Cudd.Man.tbool array -> unit
val print_bdd :
?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 Cudd.Bdd.t -> unit
val print_idcondb :
?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 -> int * bool -> unit
val print_idcond :
?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 -> int -> unit
val permutation_of_rename :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> ('a * 'a) list -> int array
val composition_of_lvarexpr :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> ('a * 'd Bdd.Expr0.t) list -> 'd Cudd.Bdd.t array
val composition_of_lvarlexpr :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'a list -> 'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array
val bddsupport :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> 'a list -> 'd Cudd.Bdd.t
val varmap : 'a Bdd.Expr0.t -> 'a Bdd.Expr0.t
val permute :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.t -> int array -> 'd Bdd.Expr0.t
val compose :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.t -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t
val permute_list :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.t list -> int array -> 'd Bdd.Expr0.t list
val compose_list :
?memo:Cudd.Memo.t ->
'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t list
module Expr :
sig
type 'a atom =
Tbool of 'a * bool
| Tint of 'a * int list
| Tenum of 'a * 'a list
type 'a term =
Tatom of 'a Bdd.Expr0.O.Expr.atom
| Texternal of (int * bool)
| Tcst of bool
val map_atom :
('a -> 'b) ->
'a Bdd.Expr0.O.Expr.atom -> 'b Bdd.Expr0.O.Expr.atom
val map_term :
('a -> 'b) ->
'a Bdd.Expr0.O.Expr.term -> 'b Bdd.Expr0.O.Expr.term
val term_of_vint :
'a ->
'd Bdd.Int.t -> Bdd.Reg.Minterm.t -> 'a Bdd.Expr0.O.Expr.term
val term_of_venum :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'a ->
'd Bdd.Enum.t ->
Bdd.Reg.Minterm.t -> 'a Bdd.Expr0.O.Expr.term
val term_of_idcondb :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t -> int * bool -> 'a Bdd.Expr0.O.Expr.term
val bool_of_tbool : Cudd.Man.tbool -> bool
val mand :
'a Bdd.Expr0.O.Expr.term list Pervasives.ref ->
'a Bdd.Expr0.O.Expr.term -> unit
val conjunction_of_minterm :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
Cudd.Man.tbool array ->
'a Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction
val dnf_of_bdd :
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e)
Bdd.Env.O.t ->
'd Cudd.Bdd.t -> 'a Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf
val print_term :
?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 -> 'a Bdd.Expr0.O.Expr.term -> unit
val print_conjunction :
?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 ->
'a Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction -> unit
val print_dnf :
?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 ->
'a Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf -> unit
end
end
end
module Expr1 :
sig
type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'b Bdd.Expr0.t) Bdd.Env.value
type ('a, 'b) expr = ('a, 'b) Bdd.Expr1.t
type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.t
module Bool :
sig
type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'b Cudd.Bdd.t) Bdd.Env.value
type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Bool.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Bool.t
val of_expr0 :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val get_env : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Env.t
val to_expr0 : ('a, 'b) Bdd.Expr1.Bool.t -> 'b Bdd.Expr0.Bool.t
val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Bool.t
val to_expr : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.expr
val extend_environment :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
val dtrue : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
val dfalse : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
val of_bool :
('a, 'b) Bdd.Env.t -> bool -> ('a, 'b) Bdd.Expr1.Bool.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> ('a, 'b) Bdd.Expr1.Bool.t
val dnot : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val dand :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val dor :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val xor :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val nand :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val nor :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val nxor :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val eq :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val leq :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val ite :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val is_true : ('a, 'b) Bdd.Expr1.Bool.t -> bool
val is_false : ('a, 'b) Bdd.Expr1.Bool.t -> bool
val is_cst : ('a, 'b) Bdd.Expr1.Bool.t -> bool
val is_eq :
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
val is_leq :
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
val is_inter_false :
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
val exist :
'a list -> ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val forall :
'a list -> ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val cofactor :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val restrict :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val tdrestrict :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Bool.t ->
('a * 'a) list -> ('a, 'b) Bdd.Expr1.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Bool.t ->
('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Bool.t
val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Bool.t -> unit
end
module Bint :
sig
type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'b Bdd.Int.t) Bdd.Env.value
type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Bint.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Bint.t
val of_expr0 :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val get_env : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Env.t
val to_expr0 : ('a, 'b) Bdd.Expr1.Bint.t -> 'b Bdd.Expr0.Bint.t
val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Bint.t
val to_expr : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.expr
val extend_environment :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bint.t
val of_int :
('a, 'b) Bdd.Env.t ->
[ `Bint of bool * int ] -> int -> ('a, 'b) Bdd.Expr1.Bint.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> ('a, 'b) Bdd.Expr1.Bint.t
val neg : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val succ : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val pred : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val add :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val sub :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val mul :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val shift_left :
int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val shift_right :
int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val scale :
int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val ite :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
val zero : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
val eq :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
val supeq :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
val sup :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
val eq_int :
('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
val supeq_int :
('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
val sup_int :
('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
val cofactor :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
val restrict :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
val tdrestrict :
('a, 'b) Bdd.Expr1.Bint.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Bint.t ->
('a * 'a) list -> ('a, 'b) Bdd.Expr1.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Bint.t ->
('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Bint.t
val guard_of_int :
('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
val guardints :
('a, 'b) Bdd.Expr1.Bint.t ->
(('a, 'b) Bdd.Expr1.Bool.t * int) list
val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Bint.t -> unit
end
module Benum :
sig
type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'b Bdd.Enum.t) Bdd.Env.value
type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Benum.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Benum.t
val of_expr0 :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.Benum.t -> ('a, 'b) Bdd.Expr1.Benum.t
val get_env : ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Env.t
val to_expr0 : ('a, 'b) Bdd.Expr1.Benum.t -> 'b Bdd.Expr0.Benum.t
val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Benum.t
val to_expr : ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.expr
val extend_environment :
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Benum.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> ('a, 'b) Bdd.Expr1.Benum.t
val ite :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.Benum.t
val eq :
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.Bool.t
val eq_label :
('a, 'b) Bdd.Expr1.Benum.t -> 'a -> ('a, 'b) Bdd.Expr1.Bool.t
val cofactor :
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
val restrict :
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
val tdrestrict :
('a, 'b) Bdd.Expr1.Benum.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Benum.t ->
('a * 'a) list -> ('a, 'b) Bdd.Expr1.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.Benum.t ->
('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Benum.t
val guard_of_label :
('a, 'b) Bdd.Expr1.Benum.t -> 'a -> ('a, 'b) Bdd.Expr1.Bool.t
val guardlabels :
('a, 'b) Bdd.Expr1.Benum.t ->
(('a, 'b) Bdd.Expr1.Bool.t * 'a) list
val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Benum.t -> unit
end
val typ_of_expr : ('a, 'b) Bdd.Expr1.t -> 'a Bdd.Env.typ
val make : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> ('a, 'b) Bdd.Expr1.t
val of_expr0 :
('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> ('a, 'b) Bdd.Expr1.t
val get_env : ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Env.t
val to_expr0 : ('a, 'b) Bdd.Expr1.t -> 'b Bdd.Expr0.t
val extend_environment :
('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.t
val var : ('a, 'b) Bdd.Env.t -> 'a -> ('a, 'b) Bdd.Expr1.t
val ite :
('a, 'b) Bdd.Expr1.Bool.t ->
('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.t
val eq :
('a, 'b) Bdd.Expr1.t ->
('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.t -> ('a * 'a) list -> ('a, 'b) Bdd.Expr1.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.t list ->
('a * 'a) list -> ('a, 'b) Bdd.Expr1.t list
val substitute :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.t ->
('a * ('a, 'b) Bdd.Expr1.t) list -> ('a, 'b) Bdd.Expr1.t
val substitute_list :
?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Expr1.t list ->
('a * ('a, 'b) Bdd.Expr1.t) list -> ('a, 'b) Bdd.Expr1.t list
val support : ('a, 'b) Bdd.Expr1.t -> 'a PSette.t
val support_cond : ('a, 'b) Bdd.Expr1.t -> 'b Cudd.Bdd.t
val cofactor :
('a, 'b) Bdd.Expr1.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
val restrict :
('a, 'b) Bdd.Expr1.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
val tdrestrict :
('a, 'b) Bdd.Expr1.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
val print : Format.formatter -> ('a, 'b) Bdd.Expr1.t -> unit
module List :
sig
type ('a, 'b) t =
(('a, 'b) Bdd.Env.t, 'b Bdd.Expr0.t list) Bdd.Env.value
type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.List.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.List.t
val of_lexpr0 :
('a, 'b) Bdd.Env.t ->
'b Bdd.Expr0.t list -> ('a, 'b) Bdd.Expr1.List.t
val get_env : ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Env.t
val to_lexpr0 : ('a, 'b) Bdd.Expr1.List.t -> 'b Bdd.Expr0.t list
val of_lexpr :
('a, 'b) Bdd.Env.t ->
('a, 'b) Bdd.Expr1.expr list -> ('a, 'b) Bdd.Expr1.List.t
val to_lexpr :
('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Expr1.expr list
val extend_environment :
('a, 'b) Bdd.Expr1.List.t ->
('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.List.t
val print :
?first:(unit, Format.formatter, unit) Pervasives.format ->
?sep:(unit, Format.formatter, unit) Pervasives.format ->
?last:(unit, Format.formatter, unit) Pervasives.format ->
Format.formatter -> ('a, 'b) Bdd.Expr1.List.t -> unit
end
module O :
sig
type ('a, 'b, 'c) t = ('b, 'c Bdd.Expr0.t) Bdd.Env.value
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd, [> 'a Bdd.Env.typdef ] as 'e,
'c, 'f)
Bdd.Env.O.t
type ('a, 'b, 'c) expr = ('a, 'b, 'c) Bdd.Expr1.O.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd, [> 'a Bdd.Env.typdef ] as 'e,
'c, 'f)
Bdd.Env.O.t
type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
Cudd.Man.d, 'e)
Bdd.Env.O.t
type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
Cudd.Man.v, 'e)
Bdd.Env.O.t
module Bool :
sig
type ('a, 'b, 'c) t = ('b, 'c Cudd.Bdd.t) Bdd.Env.value
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, 'c, 'f)
Bdd.Env.O.t
type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Bool.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
Bdd.Env.O.t
type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Bool.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
Bdd.Env.O.t
val of_expr0 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.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)
Bdd.Expr1.O.Bool.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_expr0 :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t -> 'c Bdd.Expr0.Bool.t
val of_expr :
(('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, [> `Bool of 'c Cudd.Bdd.t ])
Bdd.Env.value ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val to_expr :
('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, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
[> `Bool of 'c Cudd.Bdd.t ])
Bdd.Env.value
val extend_environment :
('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, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val dtrue :
('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) Bdd.Expr1.O.Bool.t
val dfalse :
('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) Bdd.Expr1.O.Bool.t
val of_bool :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
bool ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val var :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'a ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val dnot :
('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) Bdd.Expr1.O.Bool.t
val dand :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val dor :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val xor :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val nand :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val nor :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val nxor :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val eq :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val leq :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val ite :
('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) Bdd.Expr1.O.Bool.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) Bdd.Expr1.O.Bool.t
val is_true :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t -> bool
val is_false :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t -> bool
val is_cst :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.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)
Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.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)
Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
bool
val is_inter_false :
('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) Bdd.Expr1.O.Bool.t ->
bool
val exist :
'a list ->
('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) Bdd.Expr1.O.Bool.t
val forall :
'a list ->
('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) Bdd.Expr1.O.Bool.t
val cofactor :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val restrict :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val tdrestrict :
('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) Bdd.Expr1.O.Bool.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('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) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
('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, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val print :
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t -> unit
end
module Bint :
sig
type ('a, 'b, 'c) t = ('b, 'c Bdd.Int.t) Bdd.Env.value
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, 'c, 'f)
Bdd.Env.O.t
type ('a, 'b, 'c) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Bint.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, Cudd.Man.d, 'f)
Bdd.Env.O.t
type ('a, 'b, 'c) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Bint.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, Cudd.Man.v, 'f)
Bdd.Env.O.t
val of_expr0 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.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)
Bdd.Expr1.O.Bint.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_expr0 :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t -> 'c Bdd.Expr0.Bint.t
val of_expr :
(('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, [> `Bint of 'c Bdd.Int.t ])
Bdd.Env.value ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val to_expr :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
(('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
[> `Bint of 'c Bdd.Int.t ])
Bdd.Env.value
val extend_environment :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val of_int :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
[ `Bint of bool * int ] ->
int ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val var :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'a ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val neg :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val succ :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val pred :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val add :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val sub :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val mul :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val shift_left :
int ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val shift_right :
int ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val scale :
int ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val ite :
('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) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val zero :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val eq :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val supeq :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val sup :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val eq_int :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val supeq_int :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val sup_int :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.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) Bdd.Expr1.O.Bint.t
val restrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.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) Bdd.Expr1.O.Bint.t
val tdrestrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.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) Bdd.Expr1.O.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a * 'a) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
('a *
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
val guard_of_int :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val guardints :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t ->
(('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t * int)
list
val print :
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bint.t -> unit
end
module Benum :
sig
type ('a, 'b, 'c) t = ('b, 'c Bdd.Enum.t) Bdd.Env.value
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, 'c, 'f)
Bdd.Env.O.t
type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Benum.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
Bdd.Env.O.t
type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Benum.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
Bdd.Env.O.t
val of_expr0 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.Benum.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.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)
Bdd.Expr1.O.Benum.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_expr0 :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t -> 'c Bdd.Expr0.Benum.t
val of_expr :
(('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, [> `Benum of 'c Bdd.Enum.t ])
Bdd.Env.value ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val to_expr :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
(('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
[> `Benum of 'c Bdd.Enum.t ])
Bdd.Env.value
val extend_environment :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val var :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'a ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val ite :
('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)
Bdd.Expr1.O.Benum.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val eq :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val eq_label :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
'a ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.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)
Bdd.Expr1.O.Benum.t
val restrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.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)
Bdd.Expr1.O.Benum.t
val tdrestrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.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)
Bdd.Expr1.O.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a * 'a) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
('a *
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t
val guard_of_label :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
'a ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val guardlabels :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t ->
(('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Bool.t * 'a)
list
val print :
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.Benum.t -> unit
end
val typ_of_expr :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> 'a Bdd.Env.typ
val make :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c,
'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
val of_expr0 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c,
'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
val get_env :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_expr0 :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> 'c Bdd.Expr0.t
val extend_environment :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t ->
('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
val var :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c,
'e)
Bdd.Env.O.t ->
'a -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
val ite :
('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) Bdd.Expr1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
val eq :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t ->
('a * 'a) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t list ->
('a * 'a) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t ->
('a * ('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) Bdd.Expr1.O.t
val substitute_list :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t list ->
('a * ('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) Bdd.Expr1.O.t list
val support :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> 'a PSette.t
val support_cond :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> 'c Cudd.Bdd.t
val cofactor :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.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) Bdd.Expr1.O.t
val restrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.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) Bdd.Expr1.O.t
val tdrestrict :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.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) Bdd.Expr1.O.t
val print :
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.t -> unit
module List :
sig
type ('a, 'b, 'c) t = ('b, 'c Bdd.Expr0.t list) Bdd.Env.value
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd,
[> 'a Bdd.Env.typdef ] as 'e, 'c, 'f)
Bdd.Env.O.t
type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.List.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
Bdd.Env.O.t
type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.List.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c,
[> 'a Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
Bdd.Env.O.t
val of_lexpr0 :
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t ->
'c Bdd.Expr0.t list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.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)
Bdd.Expr1.O.List.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
val to_lexpr0 :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.List.t -> 'c Bdd.Expr0.t list
val of_lexpr :
('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) Bdd.Expr1.O.expr
list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t
val to_lexpr :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.List.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
list
val extend_environment :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b,
[> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.List.t ->
('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t
val print :
?first:(unit, Format.formatter, unit) Pervasives.format ->
?sep:(unit, Format.formatter, unit) Pervasives.format ->
?last:(unit, Format.formatter, unit) Pervasives.format ->
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Expr1.O.List.t -> unit
end
end
end
module Domain0 :
sig
type 'a t = 'a Bdd.Expr0.Bool.t
type dt = Cudd.Man.d Bdd.Domain0.t
type vt = Cudd.Man.v Bdd.Domain0.t
val size : 'a Bdd.Domain0.t -> int
val print :
?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b Bdd.Domain0.t -> unit
val bottom : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t
val top : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t
val is_bottom : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> bool
val is_top : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> bool
val is_leq :
('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> bool
val is_eq :
('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> bool
val is_variable_unconstrained :
('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'a -> bool
val meet :
('a, 'b) Bdd.Env.t ->
'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t
val join :
('a, 'b) Bdd.Env.t ->
'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t
val meet_condition :
('a, 'b) Bdd.Env.t ->
'b Bdd.Domain0.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Domain0.t
val assign_lexpr :
?relational:bool ->
?nodependency:bool ->
('a, 'b) Bdd.Env.t ->
'b Bdd.Domain0.t ->
'a list -> 'b Bdd.Expr0.expr list -> 'b Bdd.Domain0.t
val substitute_lexpr :
('a, 'b) Bdd.Env.t ->
'b Bdd.Domain0.t ->
'a list -> 'b Bdd.Expr0.expr list -> 'b Bdd.Domain0.t
val forget_list :
('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'a list -> 'b Bdd.Domain0.t
module O :
sig
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
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
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
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
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
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
module Asssub :
sig
val sort :
int array ->
'a Cudd.Bdd.t array -> int array * 'a Cudd.Bdd.t array
val is_equal :
'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t array -> bool
val post :
'a Cudd.Bdd.t ->
int array -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
val postcondition :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
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
end
end
module Domain1 :
sig
type ('a, 'b) t = ('a, 'b) Bdd.Expr1.Bool.t
type 'a dt = ('a, Cudd.Man.d) Bdd.Domain1.t
type 'a vt = ('a, Cudd.Man.v) Bdd.Domain1.t
val of_domain0 :
('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> ('a, 'b) Bdd.Domain1.t
val get_env : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Env.t
val to_domain0 : ('a, 'b) Bdd.Domain1.t -> 'b Bdd.Domain0.t
val of_expr1 : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
val to_expr1 : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Expr1.Bool.t
val size : ('a, 'b) Bdd.Domain1.t -> int
val print : Format.formatter -> ('a, 'b) Bdd.Domain1.t -> unit
val bottom : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
val top : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
val is_bottom : ('a, 'b) Bdd.Domain1.t -> bool
val is_top : ('a, 'b) Bdd.Domain1.t -> bool
val is_leq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
val is_eq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
val is_variable_unconstrained : ('a, 'b) Bdd.Domain1.t -> 'a -> bool
val meet :
('a, 'b) Bdd.Domain1.t ->
('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
val join :
('a, 'b) Bdd.Domain1.t ->
('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
val meet_condition :
('a, 'b) Bdd.Domain1.t ->
('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
val assign_lexpr :
?relational:bool ->
?nodependency:bool ->
('a, 'b) Bdd.Domain1.t ->
'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
val assign_listexpr :
?relational:bool ->
?nodependency:bool ->
('a, 'b) Bdd.Domain1.t ->
'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
val substitute_lexpr :
('a, 'b) Bdd.Domain1.t ->
'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
val substitute_listexpr :
('a, 'b) Bdd.Domain1.t ->
'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
val forget_list :
('a, 'b) Bdd.Domain1.t -> 'a list -> ('a, 'b) Bdd.Domain1.t
val change_environment :
('a, 'b) Bdd.Domain1.t ->
('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
val rename :
('a, 'b) Bdd.Domain1.t -> ('a * 'a) list -> ('a, 'b) Bdd.Domain1.t
module O :
sig
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, 'b, 'c) t = ('a, 'b, 'c) Bdd.Expr1.O.Bool.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'd, [> 'a Bdd.Env.typdef ] as 'e,
'c, 'f)
Bdd.Env.O.t
type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Domain1.O.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
Cudd.Man.d, 'e)
Bdd.Env.O.t
type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Domain1.O.t
constraint 'b =
('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
Cudd.Man.v, 'e)
Bdd.Env.O.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) Bdd.Domain1.O.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)
Bdd.Domain1.O.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)
Bdd.Domain1.O.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) Bdd.Domain1.O.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)
Bdd.Domain1.O.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)
Bdd.Domain1.O.t -> int
val print :
Format.formatter ->
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.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) Bdd.Domain1.O.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) Bdd.Domain1.O.t
val is_bottom :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t -> bool
val is_top :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.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)
Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.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)
Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
bool
val is_variable_unconstrained :
('a,
('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t -> 'a -> bool
val meet :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
val join :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.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)
Bdd.Domain1.O.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) Bdd.Domain1.O.t
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)
Bdd.Domain1.O.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) Bdd.Domain1.O.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)
Bdd.Domain1.O.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) Bdd.Domain1.O.t
val substitute_lexpr :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.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) Bdd.Domain1.O.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)
Bdd.Domain1.O.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) Bdd.Domain1.O.t
val forget_list :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t ->
'a list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
val change_environment :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t ->
('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
val rename :
('a,
('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd,
'c, 'e)
Bdd.Env.O.t, 'c)
Bdd.Domain1.O.t ->
('a * 'a) list ->
('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
end
end
end