Transformation : Correction et optim pour split_conjunction

Makefile.in

@@ -601,7 +601,7 @@ config.status: configure
 configure: configure.in
 	autoconf 
 
-src/util/dynlink_compat.ml: src/util/dynlink_compat.ml.in config.status
+src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status
 	./config.status
 
 # clean and depend

lib/drivers/alt_ergo.drv

@@ -15,7 +15,7 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 (* À discuter *)
 transformations
   "simplify_recursive_definition"      
-  "split_conjunction" (*"split_to_cnf"*)
+  (*"split_goal_pos"*) "split_goal_pos_neg"
   "inline_trivial"
 end
 

src/main.ml

@@ -95,9 +95,9 @@ let timeout = if !timeout <= 0 then None else Some !timeout
 let () = 
   match !output_dir,!output_file,!call with
     | None,None,false -> type_only := true
-    | _,Some _,true -> 
+(*    | _,Some _,true -> 
         eprintf "--output-file and --call can't be use at the same time.@.";
-        exit 1
+        exit 1*)
     | _ -> ()
 
 
@@ -195,7 +195,7 @@ let do_file env drv filename_printer file =
           Hashtbl.fold
             (fun tname goals acc ->
                let th = try Mnm.find tname m with Not_found -> 
-                 eprintf "File %s : --goal : Unknown theory %s@." file tname; exit 1 in                
+                 eprintf "File %s : --goal/--goals_of : Unknown theory %s@." file tname; exit 1 in                
                let filter = match goals with
                  | None -> None
                  | Some s -> Some 

src/test.why

@@ -30,6 +30,16 @@ theory Test_conjunction
        goal G2 : forall x:int. (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x=-8) and x*x*2 = 8)
 end
 
+theory Split_conj
+       logic p(x:int)
+       (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
+       (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
+       (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
+       goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
+       (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x))  or  ((p(z)) and (p(x))))) *)
+       (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
+end
+
 
 (*
 Local Variables: 

src/transform/split_conjunction.ml

@@ -13,10 +13,10 @@ let list_fold_product f acc l1 l2 =
 let rec split_pos split_neg acc f =
   let split_pos acc f = 
     let p = split_pos split_neg acc f in
-(*    Format.printf "@[<hov 2>f : %a@\n acc : %a :@\n %a@]@." 
+    Format.printf "@[<hov 2>f : %a@\n acc : %a :@\n %a@]@." 
       Pretty.print_fmla f
       (Pp.print_list Pp.semi Pretty.print_fmla) acc
-      (Pp.print_list Pp.semi Pretty.print_fmla) p;*)
+      (Pp.print_list Pp.semi Pretty.print_fmla) p;
     p in
 
   match f.f_node with
@@ -34,7 +34,7 @@ let rec split_pos split_neg acc f =
         list_fold_product 
           (fun acc f1 f2 ->  (f_or f1 f2)::acc) 
           acc (split_pos [] f1) (split_pos [] f2)
-    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_neg acc f)
+    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_neg [] f)
     | Fif (fif,fthen,felse) -> 
         split_pos 
           (split_pos acc (f_implies fif fthen)) 
@@ -60,15 +60,14 @@ let rec split_neg split_pos acc f =
         list_fold_product 
           (fun acc f1 f2 ->  (f_and f1 f2)::acc) 
           acc (split_neg [] f1) (split_neg [] f2)
-    | Fbinop (Fimplies,f1,f2) -> split_pos (split_neg acc f2) f1
+    | Fbinop (Fimplies,f1,f2) -> split_pos (split_neg acc f2) (f_not f1)
     | Fbinop (Fiff,f1,f2) -> 
-        split_neg (split_neg acc (f_and (f_not f1) f2)) (f_and (f_not f2) f1)
+        split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
     | Fbinop (For,f1,f2) -> split_neg (split_neg acc f2) f1
-    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_pos acc f)
+    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_pos [] f)
     | Fif (fif,fthen,felse) -> 
-          (split_neg acc 
-             (f_and (f_implies fif fthen) 
-                (f_implies (f_not fif) felse)))
+        split_neg (split_neg acc (f_and fif fthen))
+          (f_and (f_not fif) felse)
     | Flet (t,fb) ->
         let vs,f = f_open_bound fb in
         List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (split_neg [] f)
@@ -92,12 +91,11 @@ let elt split_pos d =
 
 let split_pos1 = split_pos (fun acc x -> x::acc)
 
-let split_conjunction () = Trans.decl_l (elt split_pos1)
-
 let rec split_pos2 acc d = split_pos split_neg2 acc d
 and split_neg2 acc d = split_neg split_pos2 acc d
 
-let split_to_cnf () = Trans.decl_l (elt split_pos2)
+let split_pos () = Trans.decl_l (elt split_pos1)
+let split_pos_neg () = Trans.decl_l (elt split_pos2)
 
-let () = Driver.register_transform_l "split_conjunction" split_conjunction
-let () = Driver.register_transform_l "split_to_cnf" split_to_cnf
+let () = Driver.register_transform_l "split_goal_pos" split_pos
+let () = Driver.register_transform_l "split_goal_pos_neg" split_pos_neg