package lutin

You can search for identifiers within the package.

in-package search v0.2.0

lutin
- Auto2Lucky
- AutoGen
- Bddd
- CheckEnv
- CheckType
- CkIdentInfo
- CkTypeEff
- CoAlgExp
- CoIdent
- CoTraceExp
- Constraint
- Draw
- Exp
- ExpEval
- Expand
- ExprUtil
- FGen
- Formula_to_bdd
- GenOcamlGlue
- Glue
- Gne
- Guard
- Lexeme
- LoopWeights
- Luc2alice
- Luc2c
- LucFGen
- Lucky
- LutErrors
- LutExe
- LutLexer
- LutParser
- LutPredef
- LutProg
- LutinRun
- LutinUtils
- MainArg
- Ne
- Parsers
- Poly_draw
- Polyhedron
- Prevar
- Prog
- Reactive
- Rif
- Sol_nb
- Solver
- Store
- Syntaxe
- SyntaxeDump
- Thickness
- Type
- Util
  - StringMap
- Utils
- Value
- Var
- Verbose
- Version

Legend:
Library
Module
Module type
Parameter
Class
Class type

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