bddapron 2.3.1 · OCaml Package

type (!'a, !'b) t = (('a, 'b) Env.t, 'b Int.t) Env.value

type !'a dt = ('a, Cudd.Man.d) t

type !'a vt = ('a, Cudd.Man.v) t

val of_expr0 : ('a, 'b) Env.t -> 'b Expr0.Bint.t -> ('a, 'b) t

val get_env : ('a, 'b) t -> ('a, 'b) Env.t

val to_expr0 : ('a, 'b) t -> 'b Expr0.Bint.t

val of_expr : ('a, 'b) expr -> ('a, 'b) t

val to_expr : ('a, 'b) t -> ('a, 'b) expr

val extend_environment : ('a, 'b) t -> ('a, 'b) Env.t -> ('a, 'b) t

val of_int : ('a, 'b) Env.t -> [ `Bint of bool * int ] -> int -> ('a, 'b) t

val var : ('a, 'b) Env.t -> 'a -> ('a, 'b) t

val neg : ('a, 'b) t -> ('a, 'b) t

val succ : ('a, 'b) t -> ('a, 'b) t

val pred : ('a, 'b) t -> ('a, 'b) t

val add : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val sub : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val mul : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val shift_left : int -> ('a, 'b) t -> ('a, 'b) t

val shift_right : int -> ('a, 'b) t -> ('a, 'b) t

val scale : int -> ('a, 'b) t -> ('a, 'b) t

val ite : ('a, 'b) Bool.t -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t

val zero : ('a, 'b) t -> ('a, 'b) Bool.t

val eq : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) Bool.t

val supeq : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) Bool.t

val sup : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) Bool.t

val eq_int : ('a, 'b) t -> int -> ('a, 'b) Bool.t

val supeq_int : ('a, 'b) t -> int -> ('a, 'b) Bool.t

val sup_int : ('a, 'b) t -> int -> ('a, 'b) Bool.t

val cofactor : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t

val restrict : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t

val tdrestrict : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t

val substitute_by_var : 
  ?memo:Cudd.Memo.t ->
  ('a, 'b) t ->
  ('a * 'a) list ->
  ('a, 'b) t

val substitute : 
  ?memo:Cudd.Memo.t ->
  ('a, 'b) t ->
  ('a * ('a, 'b) expr) list ->
  ('a, 'b) t

val guard_of_int : ('a, 'b) t -> int -> ('a, 'b) Bool.t

val guardints : ('a, 'b) t -> (('a, 'b) Bool.t * int) list

val print : Format.formatter -> ('a, 'b) t -> unit

package bddapron