Commit 66d7a2fc authored by Maxime Folschette's avatar Maxime Folschette
Browse files

working simplify

parent 7529a196
......@@ -572,6 +572,7 @@ struct
*)
(** Simplification d'une formule selon certains paramètres *)
(*
(* TODO : À optimiser ! *)
(* Supprimer l'évaluation (la fusionner à et la simplification) pour ne pas répéter le parcours de l'arbre *)
type evaluated_prop =
......@@ -580,10 +581,12 @@ struct
| Evaluated of int
| Unknown ;;
let evaluated_of_bool = function
| T -> true
| F -> false ;;
| true -> T
| false -> F ;;
*)
(*
(* Ancienne façon de faire : évaluations partout *)
let eval_propop0 op =
match op with
| True -> T
......@@ -643,13 +646,7 @@ struct
match (eval_expr e1), (eval_expr e2) with
| Evaluated val1, Evaluated val2 -> (evalfun_of_exprop2 op) val1 val2
| _, _ -> U ;;
*)
(* TODO *)
(* assoc_find *)
(* TODO *)
(* paramequals pour égaliser deux paramètres *)
let eval_expr e lv lk =
match e with
......@@ -669,62 +666,110 @@ struct
| PropBin(op, f1, f2) -> eval_propop2 op f1 f2
| Rel(op, e1, e2) -> eval_relop1 op e1 e2
| FreshState(f) -> U ;; (* TODO: Réfléchir à l'évaluation de FreshState *)
*)
(* TODO *)
(* TODO: Optimiser à grands coups de let ... in pour éviter les évaluations répétées *)
let simpl_propop2_And f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(False)
| _ -> match simpl_formula f2 lv lk with
| PropConst(True) -> simpl_formula f1 lv lk
| PropConst(False) -> PropConst(False)
| _ -> PropBin(And, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
let simpl_propop2_Or f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> simpl_formula f2 lv lk
| _ -> match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> simpl_formula f1 lv lk
| _ -> PropBin(Or, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
let simpl_propop2_Impl f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> PropConst(False)
| _ -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(True)
| _ -> PropBin(Impl, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
let simpl_propop2 op f1 f2 lv lk =
match op with
| And -> simpl_propop2_And f1 f2 lv lk
| Or -> simpl_propop2_Or f1 f2 lv lk
| Impl -> simpl_propop2_Impl f1 f2 lv lk ;;
type assoc_option =
| Found of int
| Not_found ;;
(* TODO: Transformer pour virer un maximum d'évaluations et les transformer en simplifications + simplifier si un seul membre peut être évalué *)
(* Simplification d'une expression *)
let rec simpl_expr e lv lk =
let rec assoc_find eq k1 l =
match l with
| [] -> Not_found
| (k2, v) :: t -> match eq k1 k2 with
| true -> Found v
| false -> assoc_find eq k1 t in
(* xFIXME? : Revoir la notion d'égalité : la fonction (=) propre à OCaml est-elle suffisante ? *)
let paramequals = (=) in
let evalfun_of_exprop2 = function
| Plus -> (+)
| Minus -> (-) ;;
let simpl_exprop2 op e1 e2 =
match (eval_expr e1), (eval_expr e2) with
| Evaluated val1, Evaluated val2 -> (evalfun_of_exprop2 op) val1 val2
| Evaluated val1, _ -> ...
| _, Evaluated val2 -> ...
| _, _ -> U ;;
let rec simpl_formula e lv lk =
match e with
| Minus -> (-) in
match e with
| ExprBin(op, e1, e2) -> (match simpl_expr e1 lv lk, simpl_expr e2 lv lk with
| ExprConst(i1), ExprConst(i2) -> ExprConst(evalfun_of_exprop2 op i1 i2)
| es1, es2 -> ExprBin(op, es1, es2))
| ExprVar(v) -> (match assoc_find BRN.varequals v lv with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprParam(v, l) -> (match assoc_find paramequals (v, l) lk with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprConst(i) -> ExprConst(i) ;;
let rec simpl_formula f lv lk =
let evalfun_of_relop2 = function
| LE -> (<=)
| LT -> (<)
| GE -> (>=)
| GT -> (>)
| Eq -> (=)
| NEq -> (!=) in
let simpl_exprop2 op e1 e2 lv lk =
match (simpl_expr e1 lv lk), (simpl_expr e2 lv lk) with
| ExprConst(i1), ExprConst(i2) -> (match (evalfun_of_relop2 op) i1 i2 with
| true -> PropConst(True)
| false -> PropConst(False))
| es1, es2 -> Rel(op, es1, es2) in
(* Simplification d'une formule *)
match f with
| PropConst(op) -> PropConst(op)
| PropUn(op, f) -> match simplify f lv lk with
| PropConst True -> PropConst False
| PropConst False -> PropConst True
| PropUn(op, f) -> simpl_propop1 op f lv lk
| PropBin(op, f1, f2) -> simpl_propop2 op f1 f2 lv lk
| Rel(op, e1, e2) -> match eval_exprop2 op e1 e2 with
| T -> ExprConst True
| F -> ExprConst False
| U -> e
| FreshState(f) -> FreshState(f) ;; (* TODO: Réfléchir à la simplification de FreshState *)
| Rel(op, e1, e2) -> simpl_exprop2 op e1 e2 lv lk
| FreshState(f) -> FreshState(f) and (* TODO: Réfléchir à la simplification de FreshState *)
(* Simplifications atomiques pour chaque forme de proposition *)
(* Opérateur unaire *)
simpl_propop1 op f lv lk =
match op with
| Neg -> match simpl_formula f lv lk with
| PropConst True -> PropConst False
| PropConst False -> PropConst True
| fs -> PropUn(Neg, fs) and
(* Opérateurs binaires *)
simpl_propop2 op f1 f2 lv lk =
match op with
| And -> simpl_propop2_And f1 f2 lv lk
| Or -> simpl_propop2_Or f1 f2 lv lk
| Impl -> simpl_propop2_Impl f1 f2 lv lk and
simpl_propop2_And f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(False)
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> fs1
| PropConst(False) -> PropConst(False)
| fs2 -> PropBin(And, fs1, fs2)) and
simpl_propop2_Or f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> simpl_formula f2 lv lk
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> fs1
| fs2 -> PropBin(Or, fs1, fs2)) and
simpl_propop2_Impl f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(True)
| fs1 -> (match simpl_formula f1 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> PropUn(Neg, fs1)
| fs2 -> PropBin(Impl, fs1, fs2)) ;;
let simplify f lv lk =
let rec iter_lv l =
match l with
| [] -> PropConst(True)
| (v, i) :: [] -> Rel(Eq, ExprVar(v), ExprConst(i))
| (v, i) :: t -> PropBin(And, Rel(Eq, ExprVar(v), ExprConst(i)), iter_lv t) in
let rec iter_lk l =
match l with
| [] -> PropConst(True)
| ((v, lm), i) :: [] -> Rel(Eq, ExprParam(v, lm), ExprConst(i))
| ((v, lm), i) :: t -> PropBin(And, Rel(Eq, ExprParam(v, lm), ExprConst(i)), iter_lk t) in
(simpl_formula (PropBin(And, iter_lv lv, iter_lk lk)) [] [], simpl_formula f lv lk) ;;
end ;;
......@@ -1037,10 +1082,15 @@ write_example pre3 "toyex-complex.lp" ;;
(** Exemple du papier *)
let and_simplify f lv lk =
let (a, b) = simplify f lv lk in
PropBin(And, a, b) ;;
let prog1 = Seq(Seq(Incr B, Incr C), Decr B) ;;
let post1 = Rel(Eq, ExprVar B, ExprConst 0) ;;
(* let pre1 = wp prog1 post1 ;; (* Sans raffinage *) *)
let pre1 = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar A, ExprConst 1)) ;; (* Avec raffinage *)
let pre1_nr = wp prog1 post1 ;; (* Sans raffinage *)
(* let pre1 = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar A, ExprConst 1)) ;; (* Avec raffinage, ancienne implémentation sans simplification *) *)
let pre1 = and_simplify pre1_nr [(A, 1) ; (C, 0) ; (B, 0)] [] ;; (* Avec raffinage et simplification *)
print_endline "***************************" ;;
print_endline "*** Exemple 1 du papier ***" ;;
print_endline "***************************" ;;
......
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