simplification of double-negation (except in FreshState)

main.ml

@@ -547,7 +547,9 @@ let rec simpl_formula f lv lk =
       | PropUn(op, f) -> simpl_propop1 op f lv lk
       | PropBin(op, f1, f2) -> simpl_propop2 op f1 f2 lv lk
       | Rel(op, e1, e2) -> simpl_exprop2 op e1 e2 lv lk
-      | FreshState(f) -> FreshState(f) and  (* TODO: Réfléchir à la simplification de FreshState : simplification des paramètres ? *)
+      | FreshState(f) -> FreshState(f) and
+  (* TODO: Propager la simplification dans les FreshState (déjà sans raffinement) *)
+  (* TODO: Réfléchir à la simplification de FreshState : simplification des paramètres ? *)
 (* Simplifications atomiques pour chaque forme de proposition *)
 (* Opérateur unaire *)
 simpl_propop1 op f lv lk =
@@ -555,7 +557,8 @@ simpl_propop1 op f lv lk =
     | Neg -> match simpl_formula f lv lk with
                | PropConst True -> PropConst False
                | PropConst False -> PropConst True
-               | fs -> PropUn(Neg, fs) and (* TODO: Simplification des double-négations *)
+               | PropUn(Neg, ffs) -> prerr_endline "!! Double-nég !!" ; ffs
+               | fs -> PropUn(Neg, fs) and
 (* Opérateurs binaires *)
 simpl_propop2 op f1 f2 lv lk =
   match op with
@@ -1040,7 +1043,29 @@ write_example pre1 "circlock1.lp" ;;
 
 
 
-(** Affichage des correspondances variable ASP / paramètre *)
+(*******************)
+(*** Bac à sable ***)
+(*******************)
+
+print_endline "*******************" ;;
+print_endline "*** Bac à sable ***" ;;
+print_endline "*******************" ;;
+
+let testf = PropUn(Neg, PropUn(Neg, Rel(LT, ExprVar "A", ExprConst 1))) ;;
+let testf_simpl = simplify testf [] [] ;;
+print_endline "*** Formule non simplifiée ***" ;;
+print_endline (string_of_formula testf) ;;
+print_endline "*** Formule simplifiée ***" ;;
+print_endline (string_of_formula testf_simpl) ;;
+
+print_endline "*** Formule 4b re-simplifiée ***" ;;
+print_endline (string_of_formula (simplify pre4b [] [])) ;;
+
+
+
+(************************************************)
+(*** Correspondances variable ASP / paramètre ***)
+(************************************************)
 (* Décommenter pour afficher la représentation ASP correspondant à chaque paramètre : *)
 (*
 print_endline "   *****" ; asp_params () ;;