Commit 56ef7cac authored by Pascal Raymond's avatar Pascal Raymond
Browse files

Start LutExe based algo (not yet operationnal)

parent 561ba995
(* NON RECURSIVE partial eval of Exp.t
Tries to simplify the TOP-LEVEL operation ONLY
*)
open Exp
open Value
let bval b = if b then True else False
let exp_to_ezdl_arg e = (
match e with
| Numer (Ival i) -> Ezdl.Int_carg i
| Numer (Fval f) -> Ezdl.Double_carg f
| Formu (True) -> Ezdl.Int_carg 1
| Formu (False) -> Ezdl.Int_carg 0
| _ -> raise Not_found
)
let rec simp_num it = (
match it with
| Sum (Ival i1, Ival i2) -> Ival (i1 + i2)
| Sum (Fval r1, Fval r2) -> Fval (r1 +. r2)
| Diff ( Ival i1, Ival i2) -> Ival (i1 - i2)
| Diff ( Fval r1, Fval r2) -> Fval (r1 +. r2)
| Prod ( Ival i1, Ival i2) -> Ival (i1 * i2)
| Prod ( Fval r1, Fval r2) -> Fval (r1 *. r2)
| Quot ( Ival i1, Ival i2) -> Ival (i1 / i2)
| Quot ( Fval r1, Fval r2) -> Fval (r1 /. r2)
| Mod ( Ival i1, Ival i2) -> Ival (i1 mod i2)
| Div ( Ival i1, Ival i2) -> Ival (i1 / i2)
| Uminus (Ival i1) -> Ival (- i1)
| Uminus (Fval r1) -> Fval (-. r1)
| FFC (s,cfunc,ftype,flib,al) -> (
try (
let dlargs = List.map exp_to_ezdl_arg al in
let res_call = Ezdl.cargs2f cfunc dlargs in
Fval (res_call)
) with Not_found -> it
)
| IFC (s,cfunc,ftype,flib,al) -> (
try (
let dlargs = List.map exp_to_ezdl_arg al in
let res_call = Ezdl.cargs2i cfunc dlargs in
Ival (res_call)
) with Not_found -> it
)
| Gcont (Ival i1, Ival i2, Ival i3) -> (
let i = Liblutin.gauss_continue i1 i2 i3 in
Ival i
)
| Gstop (Ival i1, Ival i2, Ival i3) -> (
let i = Liblutin.gauss_stop i1 i2 i3 in
Ival i
)
| Icont (Ival i1, Ival i2, Ival i3) -> (
let i = Liblutin.interval_continue i1 i2 i3 in
Ival i
)
| Istop (Ival i1, Ival i2, Ival i3) -> (
let i = Liblutin.interval_stop i1 i2 i3 in
Ival i
)
| Ite (True, a2, _) -> a2
| Ite (False, _, a3) -> a3
| _ -> it
) and simp_formula it = (
match it with
| And (False, _) | And (_, False) -> False
| And (True, a) | And (a, True) -> a
| Or (False, a) | Or (a, False) -> a
| Or (True, _) | Or (_, True) -> True
| Xor (False, a) | Xor (a, False) -> a
| Xor (True , a) | Xor (a, True ) -> simp_formula (Not a)
| Impl (False, _) | Impl ( _, True ) -> True
| Impl (True, a) -> a
| Impl (a, False ) -> simp_formula (Not a)
| IteB (True , a , _ )
| IteB (False, _ , a ) -> a
| IteB ( a , True , b ) -> simp_formula (Or (a , b))
| IteB ( a , False , b ) -> simp_formula (And (simp_formula (Not a), b))
| IteB ( a , b , True ) -> simp_formula (Or (simp_formula (Not a), b))
| IteB ( a , b , False ) -> simp_formula (And (a,b))
| Not True -> False
| Not False -> True
| EqB (True, a) | EqB (a, True) -> a
| EqB (False, a) | EqB (a, False) -> simp_formula (Not a)
| Eq ( Ival i1, Ival i2) -> bval (i1 = i2)
| Eq ( Fval r1, Fval r2) -> bval (r1 = r2)
| Sup ( Ival i1, Ival i2) -> bval (i1 > i2)
| Sup ( Fval r1, Fval r2) -> bval (r1 > r2)
| SupEq ( Ival i1, Ival i2) -> bval (i1 >= i2)
| SupEq ( Fval r1, Fval r2) -> bval (r1 >= r2)
| Inf ( Ival i1, Ival i2) -> bval (i1 < i2)
| Inf ( Fval r1, Fval r2) -> bval (r1 < r2)
| InfEq ( Ival i1, Ival i2) -> bval (i1 <= i2)
| InfEq ( Fval r1, Fval r2) -> bval (r1 <= r2)
| _ -> it
) and simp_exp e = (
match e with
| Formu f -> Formu (simp_formula f)
| Numer n -> Numer (simp_num n)
| _ -> assert false
)
(*
NON RECURSIVE Partial eval of exp,
i.e. ONLY THE TOP-LEVEL operation is evaluated
*)
val simp_exp : Exp.t -> Exp.t
val simp_num : Exp.num -> Exp.num
val simp_formula : Exp.formula -> Exp.formula
(*
Glue between lutin (CoAlgExp, CoIdent etc) and lucky ( Type Var Exp)
Necessary to reuse the lucky solver
*)
let dbg = Verbose.get_flag "Glue"
(* CONVERSION TYPE LUTIN -> TYPE LUCKY (CkTypeEff.t -> Type.t) *)
let lucky_type_of teff = (
if (teff = CkTypeEff.boolean) then Type.BoolT
else if (teff = CkTypeEff.integer) then Type.IntT
else if (teff = CkTypeEff.real) then Type.FloatT
else (raise (Errors.Internal_error (
"LutProg.lucky_type_of",
"Unexpected type"^(CkTypeEff.to_string teff)
)))
)
(* Utiles *)
let lucky_exp_zero = Exp.Numer (Exp.Ival 0)
let lucky_exp_of_int i = Exp.Numer (Exp.Ival i)
let lucky_exp_of_float f = Exp.Numer (Exp.Fval f)
let lucky_exp_of_value = function
| Value.B true -> Exp.Formu Exp.True
| Value.B false -> Exp.Formu Exp.False
| Value.N (Value.I i) -> Exp.Numer (Exp.Ival i)
| Value.N (Value.F f) -> Exp.Numer (Exp.Fval f)
let lucky_exp_var_ref (x: Exp.var) = (
match Var.typ x with
| Type.BoolT -> Exp.Formu (Exp.Bvar x)
| Type.IntT -> Exp.Numer (Exp.Ivar x)
| Type.FloatT -> Exp.Numer (Exp.Fvar x)
| _ -> assert false
)
(* CONVERSION EXP LUTIN -> EXP LUCKY (CkTypeEff.t -> Type.t) *)
(* Translators CoAlgExp to Exp take as argument
the function in charge of translating ident refs:
the argument MUST be a id ref (AE_pre, AE_support, AE_alias)
If "eval", constant are propagated, in particular, an exp
that contains NO vars if fully evaluated
N.B. partial eval is defined in another module
*)
type id2exp = CoAlgExp.node -> Exp.t
let lucky_exp_of (eval:bool) (id2exp:id2exp) (e: CoAlgExp.t) = (
(* recursive any type translator *)
let rec _lucky_exp_of e = (
let t = CoAlgExp.get_type e in
if t = CkTypeEff.boolean then
Exp.Formu (_lucky_formula_of e)
else if t = CkTypeEff.integer then
Exp.Numer (_lucky_numexp_of e)
else if t = CkTypeEff.real then
Exp.Numer (_lucky_numexp_of e)
else failwith ("XXX :"^(CkTypeEff.to_string t)^":"^(CoAlgExp.lus_dumps e)^"\n")
)
(* recursive bool translator *)
and _lucky_formula_of e = (
let raw_res = (
let nat = e.CoAlgExp.ae_val in
match nat with
| CoAlgExp.AE_true -> Exp.True
| CoAlgExp.AE_false -> Exp.False
| CoAlgExp.AE_pre id
| CoAlgExp.AE_support id
| CoAlgExp.AE_alias id -> (
match id2exp nat with
| Exp.Formu f -> f
| _ -> (
raise (
Errors.Internal_error (
"LutProg.lucky_formula_of",
"unexpected type for var \""^(CoIdent.to_string id)^"\""
)
)
)
)
| CoAlgExp.AE_call (id, ops) -> (
match (id, ops) with
| ("not", [o]) -> Exp.Not (_lucky_formula_of o)
| ("and", [o1;o2]) -> Exp.And (_lucky_formula_of o1, _lucky_formula_of o2)
| ("or", [o1;o2]) -> Exp.Or (_lucky_formula_of o1, _lucky_formula_of o2)
| ("xor", [o1;o2]) -> Exp.Xor (_lucky_formula_of o1, _lucky_formula_of o2)
| ("impl", [o1;o2]) -> Exp.Impl (_lucky_formula_of o1, _lucky_formula_of o2)
| ("ite", [o1;o2;o3]) -> Exp.IteB (_lucky_formula_of o1, _lucky_formula_of o2, _lucky_formula_of o3)
| ("lt", [o1;o2]) -> Exp.Inf (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("lte", [o1;o2]) -> Exp.InfEq (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("gt", [o1;o2]) -> Exp.Sup (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("gte", [o1;o2]) -> Exp.SupEq (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("neq", [o1;o2])
| ("eq", [o1;o2]) -> (
let ty = CoAlgExp.get_type o1 in
let eqexp = if (ty = CkTypeEff.boolean ) then
Exp.EqB (_lucky_formula_of o1, _lucky_formula_of o2)
else if ((ty = CkTypeEff.integer) || (ty = CkTypeEff.real)) then (
Exp.Eq (_lucky_numexp_of o1, _lucky_numexp_of o2)
) else (
assert false
) in
if (id = "neq") then Exp.Not eqexp else eqexp
)
| _ -> assert false
)
| CoAlgExp.AE_rconst x ->
raise (Errors.Internal_error ( "lucky_formula_of", "unexpected AE_rconst "^x^" CoAlgExp.t" ))
| CoAlgExp.AE_iconst x ->
raise (Errors.Internal_error ( "lucky_formula_of", "unexpected AE_iconst "^x^" CoAlgExp.t" ))
| CoAlgExp.AE_rval x ->
raise (Errors.Internal_error ( "lucky_formula_of", "unexpected AE_rval "^(string_of_float x)^" CoAlgExp.t" ))
| CoAlgExp.AE_ival x ->
raise (Errors.Internal_error ( "lucky_formula_of", "unexpected AE_ival "^(string_of_int x)^" CoAlgExp.t" ))
| CoAlgExp.AE_const x ->
raise (Errors.Internal_error ( "lucky_formula_of", "unexpected AE_const "^x^" CoAlgExp.t" ))
| CoAlgExp.AE_external_call (id, ei, prof, ops) -> (
raise ( Errors.Internal_error (
"LutProg.lucky_formula_of",
"sorry, bool type in external function not yet implemented"))
)
) in if eval then ExpEval.simp_formula raw_res else raw_res
)
(* recursive num translator *)
and _lucky_numexp_of e = (
let raw_res = (
let nat = e.CoAlgExp.ae_val in
match nat with
| CoAlgExp.AE_iconst s -> Exp.Ival (int_of_string s)
| CoAlgExp.AE_rconst s -> Exp.Fval (float_of_string s)
| CoAlgExp.AE_ival i -> Exp.Ival i
| CoAlgExp.AE_rval r -> Exp.Fval r
| CoAlgExp.AE_pre id
| CoAlgExp.AE_support id
| CoAlgExp.AE_alias id -> (
match id2exp nat with
| Exp.Numer n -> n
| _ -> (
print_string (
"LutProg.lucky_formula_of " ^
"unexpected type for var \""^(CoIdent.to_string id)^"\"");
flush stdout;
assert false;
)
)
| CoAlgExp.AE_call (id, ops) -> (
match (id, ops) with
| ("uminus", [o]) -> Exp.Uminus (_lucky_numexp_of o)
| ("plus", [o1;o2]) -> Exp.Sum (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("minus", [o1;o2]) -> Exp.Diff (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("times", [o1;o2]) -> Exp.Prod (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("slash", [o1;o2]) -> Exp.Quot (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("mod", [o1;o2]) -> Exp.Mod (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("div", [o1;o2]) -> Exp.Div (_lucky_numexp_of o1, _lucky_numexp_of o2)
| ("ite", [o1;o2;o3]) -> Exp.Ite (_lucky_formula_of o1, _lucky_numexp_of o2, _lucky_numexp_of o3)
| ("interval_continue", [o1;o2;o3]) ->
Exp.Icont (_lucky_numexp_of o1, _lucky_numexp_of o2, _lucky_numexp_of o3)
| ("interval_stop", [o1;o2;o3]) ->
Exp.Istop (_lucky_numexp_of o1, _lucky_numexp_of o2, _lucky_numexp_of o3)
| ("gauss_continue", [o1;o2;o3]) ->
Exp.Gcont (_lucky_numexp_of o1, _lucky_numexp_of o2, _lucky_numexp_of o3)
| ("gauss_stop", [o1;o2;o3]) ->
Exp.Gstop (_lucky_numexp_of o1, _lucky_numexp_of o2, _lucky_numexp_of o3)
| _ -> raise ( Errors.Internal_error (
"LutProg.lucky_numexp_of",
"Unexpected expression \""^(CoAlgExp.lus_dumps e)^"\""
))
)
| CoAlgExp.AE_external_call (id, ei, prof, ops) -> (
(* HERE: common/Exp currently only implements 2 kinds of external calls :
FFC and IFC, both taking func_call_arg as arg :
func_call_arg = string * Ezdl.cfunc * ext_func_type * ext_lib_name * t list
ext_func_type = Type.t list
ext_lib_name = string
*)
let args = List.map _lucky_exp_of ops in
let atypes = List.map lucky_type_of (CkTypeEff.params_of_prof prof) in
let fcargs = (id, ei.CkIdentInfo.ed_sym, atypes, ei.CkIdentInfo.ed_lib_name, args) in
let rtype = lucky_type_of (CkTypeEff.res_of_prof prof) in
match rtype with
| Type.IntT -> Exp.IFC fcargs
| Type.FloatT -> Exp.FFC fcargs
| Type.BoolT -> raise ( Errors.Internal_error (
"lucky_num_exp_of",
"sorry, bool type in external function not yet implemented"))
| _ -> (
assert false
)
)
| _ -> assert false
) in if eval then ExpEval.simp_num raw_res else raw_res
) in
(**** MAIN CALL of lucky_exp_of *)
_lucky_exp_of e
)
(*
let lucky_formula_of_list (id2exp:id2exp) (el: CoAlgExp.t list) = (
(* liste -> and *)
let make_and cin e = (
Utils.time_C "lucky_formula_of";
let fe = lucky_formula_of id2exp e in
Utils.time_R "lucky_formula_of";
match cin with
| Exp.True -> fe
| _ -> Exp.And (cin, fe)
) in
List.fold_left make_and Exp.True el
)
*)
let lucky_var_of (si : Expand.support_info) = (
let nme = CoIdent.to_string si.Expand.si_ident in
let ty = lucky_type_of si.Expand.si_type in
let mode = match si.Expand.si_nature with
| Expand.Input -> Var.Input
| Expand.Output -> Var.Output
| Expand.Local -> Var.Local
in
let res = Var.make "" nme ty mode in
(* HERE: store it ??? *)
res
)
(* check FULL satisfiability
of a formula CONTAINING ONLY CONTROLABLE VARS
for the time being, just a simplified version of Solver.solve_formula
*)
let check_satisfiablity (f:Exp.formula) = (
(* builds the bdd ... *)
let bdd = Formula_to_bdd.f
Value.OfIdent.empty (* no input needed *)
Value.OfIdent.empty (* no pres needed *)
"check_satisfiablity" (* message *)
0 (* no verbose *)
f (* THE FORMULA *)
in
(* *)
if (Bdd.is_false bdd) then false
else (
(* search at least one num sol *)
(* Solver.draw requires the "and"
of all bool vars to gen *)
let sols = Solver.draw
Value.OfIdent.empty (* no input needed *)
Value.OfIdent.empty (* no pres needed *)
0 (* no verbose *)
"check_satisfiablity" (* message *)
[] (* don't care of which vars are outs or locs *)
(1,0,Thickness.AtMost 0) (* Thickness.numeric: (inside, edges, vertices) *)
[] (* bool_vars_to_gen: Var.name list *)
[] (* num_vnt_to_gen: var list *)
(Bdd.support bdd) (* comb: Bdd.t *)
bdd (* ze bdd to draw in *)
in
(sols <> [])
)
)
(*
Glue between lutin (CoAlgExp, CoIdent etc) and lucky ( Type Var Exp)
Necessary to reuse the lucky solver
*)
(* Conversion type lutin -> type lucky *)
val lucky_type_of : CkTypeEff.t -> Type.t
(* lucky Exp.t utils *)
val lucky_exp_zero : Exp.t
val lucky_exp_of_int : int -> Exp.t
val lucky_exp_of_float : float -> Exp.t
val lucky_exp_of_value : Value.t -> Exp.t
(* lutin support var to lucky var *)
val lucky_var_of : Expand.support_info -> Exp.var
(* lucky var to its reference exp *)
val lucky_exp_var_ref : Exp.var -> Exp.t
(* translators CoAlgExp to Exp take as argument
the function in charge of translating ident refs:
the argument MUST be a id ref (AE_pre, AE_support, AE_alias)
*)
type id2exp = CoAlgExp.node -> Exp.t
(* translator lutin exp -> lucky exp *)
val lucky_exp_of : bool -> id2exp -> CoAlgExp.t -> Exp.t
val check_satisfiablity : Exp.formula -> bool
This diff is collapsed.
(*
A) Tout ce qu'il faut pour intégrer facilement Lutin à Lurette
--------------------------------------------------------------
- création/initialisation à partir d'un Expand.t
(ou directement d'un fichier Lutin)
résultat : le control_state initial
- (1) génération de contraintes satisfiables, avec :
une valeur des ins * une valeur des pres * un control state
-> un comportement REALISABLE (goto, vanish, raise programmé)
+ une fonction pour obtenir d'autres comportements satisfiables alternatifs
(test épais du contrôle)
-> plus/pas de comportements
N.B. c'est un peu une liste "lazzy" des comportements possibles
- (2) pour les comportements REALISABLES de type "Goto",
(i.e. un couple contrainte réalisable * control_state suivant) :
génération d'une (liste) de solutions concrètes :
(valeur des sorties, valeur des locales)
N.B. pourrait être lazzy ? ce qui n'est pas le cas pour lucky, où
on demande explicitement "n" solutions.
- pour rappeler (1), un utilitaire qui "merge" (en élagant) :
valeur des ins * valeur des outs * valeur des locales
-> valeur des pres
B) Pour faire un Lutin "réactif" simple
---------------------------------------
C'est juste une version simplifiée où on fournit juste
un step qui fait une réaction complète :
valeur des ins * prg -> valeur des outs * prg suivant
N.B. dans un premier temps, c'est un step simple qu'on
utilisera pour les appels interne "exist outs = node(ins)",
On verra plus tard pour la version Lurette récursive !
*)
type t
val make: ?libs:string list option -> string -> string -> t
type control_state
type guard
type behavior =
| Goto of guard * control_state
| Raise of string
| Vanish
(* lazzy-like list *)
type behavior_gen =
| NoMoreBehavior
| SomeBehavior of behavior * (unit -> behavior_gen)
val get_init_state: t -> control_state
val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> (unit -> behavior_gen)
val solve_guard : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list
(* the "t" is given in order to filter necessary pres, not really necessary *)
val make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
(* version step unique *)
(* val step: t -> Var.env_in -> t * Var.env_out *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment