Module GneSource

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).

Sourcetype t
Sourceval add : t -> t -> t

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

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

empty () returns an empty gne.t

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

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

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

of_ite cond flag gne_then gne_else

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

fold f gne applies f to every expr in gne.

Sourceval 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.

Sourceval to_string : t -> string

Pretty-printing

Sourceval dump : t -> unit