sig
type 'a t = ('a Bddapron.Env.t, 'a Bddapron.Expr0.t) Bddapron.Env.value
type 'a expr = 'a Bddapron.Expr1.t
module Bool :
sig
type 'a t =
('a Bddapron.Env.t, Cudd.Man.v Bddapron.Expr0.Bool.t)
Bddapron.Env.value
val of_expr0 :
'a Bddapron.Env.t ->
'a Bddapron.Expr0.Bool.t -> 'a Bddapron.Expr1.Bool.t
val get_env : 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Env.t
val to_expr0 : 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr0.Bool.t
val of_expr : 'a Bddapron.Expr1.expr -> 'a Bddapron.Expr1.Bool.t
val to_expr : 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.expr
val extend_environment :
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Env.t -> 'a Bddapron.Expr1.Bool.t
val dtrue :
'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.Bool.t
val dfalse :
'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.Bool.t
val of_bool :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> bool -> 'a Bddapron.Expr1.Bool.t
val var :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'a -> 'a Bddapron.Expr1.Bool.t
val dnot :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val dand :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val dor :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val xor :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val nand :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val nor :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val nxor :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val leq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val ite :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val is_true : 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.Bool.t -> bool
val is_false : 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.Bool.t -> bool
val is_cst : 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.Bool.t -> bool
val is_eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t -> bool
val is_leq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t -> bool
val is_inter_false :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t -> bool
val exist :
'a Bddapron.Cond.t ->
'a list -> 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val forall :
'a Bddapron.Cond.t ->
'a list -> 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val cofactor :
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val restrict :
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val tdrestrict :
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
('a * 'a) list -> 'a Bddapron.Expr1.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
('a * 'a Bddapron.Expr1.expr) list -> 'a Bddapron.Expr1.Bool.t
val print :
'a Bddapron.Cond.t ->
Format.formatter -> 'a Bddapron.Expr1.Bool.t -> unit
end
module Bint :
sig
type 'a t =
('a Bddapron.Env.t, Cudd.Man.v Bdd.Int.t) Bddapron.Env.value
val of_expr0 :
'a Bddapron.Env.t ->
'a Bddapron.Expr0.Bint.t -> 'a Bddapron.Expr1.Bint.t
val get_env : 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Env.t
val to_expr0 : 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr0.Bint.t
val of_expr : 'a Bddapron.Expr1.expr -> 'a Bddapron.Expr1.Bint.t
val to_expr : 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.expr
val extend_environment :
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Env.t -> 'a Bddapron.Expr1.Bint.t
val of_int :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
[ `Bint of bool * int ] -> int -> 'a Bddapron.Expr1.Bint.t
val var :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'a -> 'a Bddapron.Expr1.Bint.t
val neg :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val succ :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val pred :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val add :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val sub :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val mul :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val shift_left :
'a Bddapron.Cond.t ->
int -> 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val shift_right :
'a Bddapron.Cond.t ->
int -> 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val scale :
'a Bddapron.Cond.t ->
int -> 'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val ite :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bint.t
val zero :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bool.t
val eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bool.t
val supeq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bool.t
val sup :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bint.t -> 'a Bddapron.Expr1.Bool.t
val eq_int :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> int -> 'a Bddapron.Expr1.Bool.t
val supeq_int :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> int -> 'a Bddapron.Expr1.Bool.t
val sup_int :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> int -> 'a Bddapron.Expr1.Bool.t
val cofactor :
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bint.t
val restrict :
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bint.t
val tdrestrict :
'a Bddapron.Expr1.Bint.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
('a * 'a) list -> 'a Bddapron.Expr1.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t ->
('a * 'a Bddapron.Expr1.expr) list -> 'a Bddapron.Expr1.Bint.t
val guard_of_int :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> int -> 'a Bddapron.Expr1.Bool.t
val guardints :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bint.t -> ('a Bddapron.Expr1.Bool.t * int) list
val print :
'a Bddapron.Cond.t ->
Format.formatter -> 'a Bddapron.Expr1.Bint.t -> unit
end
module Benum :
sig
type 'a t =
('a Bddapron.Env.t, Cudd.Man.v Bdd.Enum.t) Bddapron.Env.value
val of_expr0 :
'a Bddapron.Env.t ->
'a Bddapron.Expr0.Benum.t -> 'a Bddapron.Expr1.Benum.t
val get_env : 'a Bddapron.Expr1.Benum.t -> 'a Bddapron.Env.t
val to_expr0 : 'a Bddapron.Expr1.Benum.t -> 'a Bddapron.Expr0.Benum.t
val of_expr : 'a Bddapron.Expr1.expr -> 'a Bddapron.Expr1.Benum.t
val to_expr : 'a Bddapron.Expr1.Benum.t -> 'a Bddapron.Expr1.expr
val extend_environment :
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Env.t -> 'a Bddapron.Expr1.Benum.t
val var :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'a -> 'a Bddapron.Expr1.Benum.t
val ite :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Expr1.Benum.t -> 'a Bddapron.Expr1.Benum.t
val eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Expr1.Benum.t -> 'a Bddapron.Expr1.Bool.t
val eq_label :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t -> 'a -> 'a Bddapron.Expr1.Bool.t
val cofactor :
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Benum.t
val restrict :
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Benum.t
val tdrestrict :
'a Bddapron.Expr1.Benum.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t ->
('a * 'a) list -> 'a Bddapron.Expr1.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t ->
('a * 'a Bddapron.Expr1.expr) list -> 'a Bddapron.Expr1.Benum.t
val guard_of_label :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t -> 'a -> 'a Bddapron.Expr1.Bool.t
val guardlabels :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Benum.t -> ('a Bddapron.Expr1.Bool.t * 'a) list
val print :
'a Bddapron.Cond.t ->
Format.formatter -> 'a Bddapron.Expr1.Benum.t -> unit
end
type apron_coeff = Apron.Coeff.t
type apron_typ = Apron.Texpr1.typ
type apron_round = Apron.Texpr1.round
type apron_cons_typ = Apron.Tcons1.typ
module Apron :
sig
type 'a t =
('a Bddapron.Env.t, 'a Bddapron.Expr0.Apron.t) Bddapron.Env.value
val of_expr0 :
'a Bddapron.Env.t ->
'a Bddapron.Expr0.Apron.t -> 'a Bddapron.Expr1.Apron.t
val get_env : 'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Env.t
val to_expr0 : 'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr0.Apron.t
val of_expr : 'a Bddapron.Expr1.expr -> 'a Bddapron.Expr1.Apron.t
val to_expr : 'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.expr
val extend_environment :
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Env.t -> 'a Bddapron.Expr1.Apron.t
val var :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'a -> 'a Bddapron.Expr1.Apron.t
val cst :
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> Apron.Coeff.t -> 'a Bddapron.Expr1.Apron.t
val add :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val mul :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val sub :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val div :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val gmod :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val negate :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val sqrt :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val cast :
'a Bddapron.Cond.t ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val ite :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Apron.t
val condition :
'a Bddapron.Cond.t ->
Apron.Tcons1.typ ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Bool.t
val supeq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Bool.t
val sup :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Bool.t
val eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t -> 'a Bddapron.Expr1.Bool.t
val cofactor :
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Apron.t
val restrict :
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Apron.t
val tdrestrict :
'a Bddapron.Expr1.Apron.t ->
'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.Apron.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t ->
('a * 'a) list -> 'a Bddapron.Expr1.Apron.t
val substitute :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Apron.t ->
('a * 'a Bddapron.Expr1.expr) list -> 'a Bddapron.Expr1.Apron.t
val print :
'a Bddapron.Cond.t ->
Format.formatter -> 'a Bddapron.Expr1.Apron.t -> unit
end
val typ_of_expr : 'a Bddapron.Expr1.t -> 'a Bddapron.Env.typ
val make : 'a Bddapron.Env.t -> 'a Bddapron.Expr0.t -> 'a Bddapron.Expr1.t
val of_expr0 :
'a Bddapron.Env.t -> 'a Bddapron.Expr0.t -> 'a Bddapron.Expr1.t
val get_env : 'a Bddapron.Expr1.t -> 'a Bddapron.Env.t
val to_expr0 : 'a Bddapron.Expr1.t -> 'a Bddapron.Expr0.t
val extend_environment :
'a Bddapron.Expr1.t -> 'a Bddapron.Env.t -> 'a Bddapron.Expr1.t
val var :
'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a -> 'a Bddapron.Expr1.t
val ite :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.Bool.t ->
'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.t
val eq :
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.t -> ('a * 'a) list -> 'a Bddapron.Expr1.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.t list -> ('a * 'a) list -> 'a Bddapron.Expr1.t list
val substitute :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.t ->
('a * 'a Bddapron.Expr1.t) list -> 'a Bddapron.Expr1.t
val substitute_list :
?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a Bddapron.Expr1.t list ->
('a * 'a Bddapron.Expr1.t) list -> 'a Bddapron.Expr1.t list
val support : 'a Bddapron.Cond.t -> 'a Bddapron.Expr1.t -> 'a PSette.t
val support_cond : Cudd.Man.vt -> 'a Bddapron.Expr1.t -> Cudd.Bdd.vt
val cofactor :
'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.t
val restrict :
'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.t
val tdrestrict :
'a Bddapron.Expr1.t -> 'a Bddapron.Expr1.Bool.t -> 'a Bddapron.Expr1.t
val print :
'a Bddapron.Cond.t -> Format.formatter -> 'a Bddapron.Expr1.t -> unit
val normalize :
?reduce:bool ->
?careset:bool ->
'a Bddapron.Cond.t * 'a Bddapron.Expr1.t list ->
'a Bddapron.Cond.t * 'a Bddapron.Expr1.t list
module List :
sig
type 'a t =
('a Bddapron.Env.t, 'a Bddapron.Expr0.t list) Bddapron.Env.value
val of_lexpr0 :
'a Bddapron.Env.t ->
'a Bddapron.Expr0.t list -> 'a Bddapron.Expr1.List.t
val get_env : 'a Bddapron.Expr1.List.t -> 'a Bddapron.Env.t
val to_lexpr0 : 'a Bddapron.Expr1.List.t -> 'a Bddapron.Expr0.t list
val of_lexpr :
'a Bddapron.Env.t ->
'a Bddapron.Expr1.expr list -> 'a Bddapron.Expr1.List.t
val to_lexpr : 'a Bddapron.Expr1.List.t -> 'a Bddapron.Expr1.expr list
val extend_environment :
'a Bddapron.Expr1.List.t ->
'a Bddapron.Env.t -> 'a Bddapron.Expr1.List.t
val normalize :
?reduce:bool ->
?careset:bool ->
'a Bddapron.Cond.t * 'a Bddapron.Expr1.List.t ->
'a Bddapron.Cond.t * 'a Bddapron.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 ->
'a Bddapron.Cond.t ->
Format.formatter -> 'a Bddapron.Expr1.List.t -> unit
end
module O :
sig
type ('a, 'b) t = ('b, 'a Bddapron.Expr0.t) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
type ('a, 'b) expr = ('a, 'b) Bddapron.Expr1.O.t
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
module Bool :
sig
type ('a, 'b) t = ('b, 'a Bddapron.Expr0.Bool.t) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
val of_expr :
(('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t, [> `Bool of 'a Bddapron.Expr0.Bool.t ])
Bddapron.Env.value ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val to_expr :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bool.t ->
(('a, 'b, 'c, 'd) Bddapron.Env.O.t,
[> `Bool of 'a Bddapron.Expr0.Bool.t ])
Bddapron.Env.value
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bool.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val dtrue :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val dfalse :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val of_bool :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
bool ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val var :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val dnot :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val dand :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val dor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val xor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val nand :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val nor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val nxor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val leq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val ite :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val is_true :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val is_false :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val is_cst :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val is_eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val is_leq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val is_inter_false :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
bool
val exist :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
'a list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val forall :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
'a list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val restrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val tdrestrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr)
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val print :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
unit
end
module Bint :
sig
type ('a, 'b) t = ('b, Cudd.Man.v Bdd.Int.t) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
val of_expr :
(('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t, [> `Bint of 'a Bddapron.Expr0.Bint.t ])
Bddapron.Env.value ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val to_expr :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bint.t ->
(('a, 'b, 'c, 'd) Bddapron.Env.O.t,
[> `Bint of 'a Bddapron.Expr0.Bint.t ])
Bddapron.Env.value
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bint.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val of_int :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
[ `Bint of bool * int ] ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val var :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val neg :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val succ :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val pred :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val add :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val sub :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val mul :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val shift_left :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val shift_right :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val scale :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val ite :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val zero :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val supeq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val sup :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val eq_int :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val supeq_int :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val sup_int :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val restrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val tdrestrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Bint.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
('a *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr)
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t
val guard_of_int :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
int ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val guardints :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
(('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t *
int)
list
val print :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bint.t ->
unit
end
module Benum :
sig
type ('a, 'b) t = ('b, Cudd.Man.v Bdd.Enum.t) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
val of_expr :
(('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t, [> `Benum of 'a Bddapron.Expr0.Benum.t ])
Bddapron.Env.value ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val to_expr :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Benum.t ->
(('a, 'b, 'c, 'd) Bddapron.Env.O.t,
[> `Benum of 'a Bddapron.Expr0.Benum.t ])
Bddapron.Env.value
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Benum.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val var :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val ite :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val eq_label :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val restrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val tdrestrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Benum.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
('a *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr)
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t
val guard_of_label :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val guardlabels :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
(('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t *
'a)
list
val print :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Benum.t ->
unit
end
module Apron :
sig
type ('a, 'b) t =
('b, 'a Bddapron.Expr0.Apron.t) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
val of_expr :
(('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t, [> `Apron of 'a Bddapron.Expr0.Apron.t ])
Bddapron.Env.value ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val to_expr :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Apron.t ->
(('a, 'b, 'c, 'd) Bddapron.Env.O.t,
[> `Apron of 'a Bddapron.Expr0.Apron.t ])
Bddapron.Env.value
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Apron.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val var :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val cst :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
Bddapron.Expr1.apron_coeff ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val add :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val mul :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val sub :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val div :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val gmod :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val negate :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val sqrt :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val cast :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
?typ:Bddapron.Expr1.apron_typ ->
?round:Bddapron.Expr1.apron_round ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val ite :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val condition :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Bddapron.Expr1.apron_cons_typ ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val supeq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val sup :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val cofactor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val restrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val tdrestrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.Apron.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
('a *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr)
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t
val print :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Apron.t ->
unit
end
val typ_of_expr :
('a,
('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t -> 'a Bddapron.Env.typ
val make :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
'a Bddapron.Expr0.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val var :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a -> ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val ite :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val eq :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t
val substitute_by_var :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val substitute_by_var_list :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list ->
('a * 'a) list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list
val substitute :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
('a * ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t)
list -> ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val substitute_list :
?memo:Cudd.Memo.t ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list ->
('a * ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t)
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list
val support :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t ->
'a PSette.t
val support_cond :
Cudd.Man.vt ->
('a,
('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t -> Cudd.Bdd.vt
val cofactor :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val restrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val tdrestrict :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.Bool.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t
val print :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t -> unit
val normalize :
?reduce:bool ->
?careset:bool ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.t list
module List :
sig
type ('a, 'b) t = ('b, 'a Bddapron.Expr0.t list) Bddapron.Env.value
constraint 'b =
('a, [> 'a Bddapron.Env.typ ] as 'c,
[> 'a Bddapron.Env.typdef ] as 'd, 'e)
Bddapron.Env.O.t
val of_lexpr0 :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
'a Bddapron.Expr0.t list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.List.t
val get_env :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.List.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
val to_lexpr0 :
('a,
('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
Bddapron.Env.O.t)
Bddapron.Expr1.O.List.t -> 'a Bddapron.Expr0.t list
val of_lexpr :
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr
list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.List.t
val to_lexpr :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.List.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.expr
list
val extend_environment :
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Expr1.O.List.t ->
('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.List.t
val normalize :
?reduce:bool ->
?careset:bool ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.List.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t *
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.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 ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b,
[> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t ->
Format.formatter ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Expr1.O.List.t ->
unit
end
end
end