package lutin

You can search for identifiers within the package.

in-package search v0.2.0

package lutin

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

Bdd Drawer.

Machinery to perform a draw in a bdd.

ZZZ : To be used by Solver only !!

type t

val tbl_to_string : t -> string

exception No_numeric_solution of t

val draw_in_bdd : 
  t ->
  Var.env_in ->
  Var.env ->
  int ->
  string ->
  Exp.var list ->
  Bdd.t ->
  Bdd.t ->
  t * Var.env * Store.t' * Store.p

draw_in_bdd memory verbose_level ctx_msg state vars bdd comb returns a draw of the Boolean variables as well as a range based and a polyhedron based representation of numeric constraints (cf. the Store module).

Side effect: this is where the solution number tables is filled in.

Raises No_numeric_solution.

val formula_to_bdd : 
  t ->
  Var.env_in ->
  Var.env ->
  string ->
  int ->
  Exp.formula ->
  t * Bdd.t

val index_to_linear_constraint : t -> int -> Constraint.t

val get_index_from_linear_constraint : t -> Constraint.t -> int

val num_to_gne : 
  t ->
  Var.env_in ->
  Var.env ->
  string ->
  int ->
  Exp.num ->
  t * Gne.t

val eval_int_expr : 
  t ->
  Exp.num ->
  string ->
  Var.env_in ->
  Var.env ->
  int ->
  int option

val clear : t -> t

val sol_number : t -> Bdd.t -> Sol_nb.sol_nb * Sol_nb.sol_nb

sol_number bdd returns the solution number in the then and else branches of bdd.