package lutin

  1. Overview
  2. Docs

Garded normal expressions.

They are Ne.t expressions garded by formula (a Bdd.t actually). The interpretation of (e1 -> bdd1 ; ... ; en -> bddn) is that it is equal to ei iff bddi is true. By construction, the set {bddi, i=1,n} ougth to be a partition (namely, exactly one bdd among the bddi is true).

type t
val add : t -> t -> t

Respectively adds, substracts, multiplies, divides, and computes the modulo, the opposite of garded normal expressions.

val diff : t -> t -> t
val mult : t -> t -> t
val modulo : t -> t -> t
val div : t -> t -> t
val opposite : t -> t
val quot : t -> t -> t
val empty : unit -> t

empty () returns an empty gne.t

val make : Ne.t -> bool -> t

make ne bdd b returns the gne containing the expr ne guarded by (bdd_true, b).

val of_ite : Bdd.t -> bool -> t -> t -> t

of_ite cond flag gne_then gne_else

val fold : (Ne.t -> (Bdd.t * bool) -> 'acc -> 'acc) -> t -> 'acc -> 'acc

fold f gne applies f to every expr in gne.

val get_constant : t -> Value.num option

get_constant gne returns an Value.num iff gne is equal to the degenerated garded normal expression [(i, true)]. This function is useful to get dynamic weigths and default values.

val to_string : t -> string

Pretty-printing

val dump : t -> unit