Up  

Module LuckyDraw


module LuckyDraw: sig .. end
Time-stamp: <modified the 11/12/2006 (at 15:25) by Erwan Jahier>

LuckyDraw is a Boolean and numeric solver and drawer.

The Boolean part is based on BDDS and the numeric part on convex Polyhedron (Polka, by B. Jeannet).

Example of use:

List.iter print_solution (draw (solve (make_bool_expr ["x",Float] "x > 10.0 and x <= 20.0"))) ;;

List.iter print_solution (draw (solve (make_bool_expr ["x",Bool; "y",Bool; "Z",Bool] "true"))) ;;

A parser for Lustre-like formula


type var_name = string

type var_type =
| Float
| Int
| Bool

type value =
| F of float
| I of int
| B of bool 
type bool_expr 
val make_bool_expr : (var_name * var_type) list ->
       string -> bool_expr

The String should be a Boolean expression in Lustre syntax, i.e., made of the following operators: and, or, not, xor, =>, =, true, false, if then else, <, <=, >, >=, +, *, -, /, div, mod as well as variable identifiers and numeric (integer, float) litterals.

e.g., make_bool_expr ["x", Bool; y, Int] "0 < y and y < 10"

An alternative way to build bool_expr



One can also build bool_expr using the following functions, with obvious semantics.

bool_expr constructors
val and_b : bool_expr -> bool_expr -> bool_expr
val or_b : bool_expr -> bool_expr -> bool_expr
val xor_b : bool_expr -> bool_expr -> bool_expr
val impl_b : bool_expr -> bool_expr -> bool_expr
val eq_b : bool_expr -> bool_expr -> bool_expr
val not_b : bool_expr -> bool_expr
val true_b : bool_expr
val false_b : bool_expr
val ite_b : bool_expr ->
       bool_expr -> bool_expr -> bool_expr
val var_b : string -> bool_expr

Integer constructors
type int_expr 
val var_i : string -> int_expr
val val_i : int -> int_expr
val eq_i : int_expr -> int_expr -> bool_expr
val sup_i : int_expr -> int_expr -> bool_expr
val supeq_i : int_expr -> int_expr -> bool_expr
val inf_i : int_expr -> int_expr -> bool_expr
val infeq_i : int_expr -> int_expr -> bool_expr
val ite_i : bool_expr ->
       int_expr -> int_expr -> int_expr
val sum_i : int_expr -> int_expr -> int_expr
val diff_i : int_expr -> int_expr -> int_expr
val prod_i : int_expr -> int_expr -> int_expr
val quot_i : int_expr -> int_expr -> int_expr
val mod_i : int_expr -> int_expr -> int_expr
val div_i : int_expr -> int_expr -> int_expr
val uminus_i : int_expr -> int_expr

Float constructors
type float_expr 
val var_f : string -> float_expr
val val_f : float -> float_expr
val eq_f : float_expr -> float_expr -> bool_expr
val sup_f : float_expr -> float_expr -> bool_expr
val supeq_f : float_expr -> float_expr -> bool_expr
val inf_f : float_expr -> float_expr -> bool_expr
val infeq_f : float_expr -> float_expr -> bool_expr
val ite_f : bool_expr ->
       float_expr -> float_expr -> float_expr
val sum_f : float_expr -> float_expr -> float_expr
val diff_f : float_expr -> float_expr -> float_expr
val prod_f : float_expr -> float_expr -> float_expr
val quot_f : float_expr -> float_expr -> float_expr
val uminus_f : float_expr -> float_expr

Constraints solver and drawer


type subst = var_name * value 
type solution = subst list 
type solutions_set 
val solve : bool_expr -> solutions_set
type draw_mode = int * int * int
To indicate the number of solutions to draw respectively inside, at edges, and at vertices of the convex hull of numeric solutions. The default draw mode is (1,0,0).
val draw : ?mode:draw_mode ->
       ?verbose:int -> solutions_set -> solution list

Drawing heuristics


val set_efficient_mode : unit -> unit
Default mode. The draw in the set of solutions is not fair w.r.t numeric variables.
val set_fair_mode : unit -> unit
In that mode, we take into account the number of numeric solutions by computing (an approx.) of the volume of polyhedra to perform the draw. It is therefore more expensive. Moreover, some of the sharing of the BDDs is lost.

Pretty-printing


val string_of_value : value -> string
val bool_expr_to_string : bool_expr -> string
val print_solution : solution -> unit

Misc.


val set_seed : int -> unit
In order to change the seed used by the pseudo-random engine.
val set_default_max_int : int -> unit
val set_default_min_int : int -> unit
val set_default_max_float : float -> unit
val set_default_min_float : float -> unit