Commit 5f6f38a8 authored by Francois Bobot's avatar Francois Bobot

ajout de la transformation split_to_cnf qui met en une forme presque cnf. Une...

ajout de la transformation split_to_cnf qui met en une forme presque cnf. Une CNF où on garde la position des négations et implications. L'interet est au moins pour la visualisation. On retrouve (normalement) une cnf simplement en poussant les négations.
parent 1c683c99
......@@ -15,7 +15,7 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
(* À discuter *)
transformations
"simplify_recursive_definition"
"split_conjunction"
"split_conjunction" (*"split_to_cnf"*)
"inline_trivial"
end
......
......@@ -250,7 +250,7 @@ let do_file env drv filename_printer file =
let fmt = if file = "-"
then std_formatter
else formatter_of_out_channel (open_out file) in
fprintf fmt "%a@?" (Driver.print_context drv) ctxt) goals
fprintf fmt "%a\000@?" (Driver.print_context drv) ctxt) goals
end;
if !call then
(* we are in the call mode *)
......
......@@ -27,6 +27,7 @@ end
theory Test_conjunction
use import prelude.Int
goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x=-8) and x*x*2 = 8)
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
......
......@@ -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 _ -> 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 acc f)
| Fif (fif,fthen,felse) ->
split_pos
(split_pos acc (f_implies fif fthen))
......@@ -60,13 +60,11 @@ 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) f1
| Fbinop (Fiff,f1,f2) ->
(* TODO plus directe? *)
split_neg acc (f_and (f_implies f1 f2) (f_implies f2 f1))
split_neg (split_neg acc (f_and (f_not f1) f2)) (f_and (f_not f2) f1)
| Fbinop (For,f1,f2) -> split_neg (split_neg acc f2) f1
| Fnot _ -> split_neg acc f
| Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_pos acc f)
| Fif (fif,fthen,felse) ->
(split_neg acc
(f_and (f_implies fif fthen)
......@@ -82,9 +80,8 @@ let rec split_neg split_pos acc f =
(f_exists vsl trl f)::acc) acc (split_neg [] fmla)
| Fquant (Fforall,_) -> f::acc
let split_pos = split_pos (fun acc x -> x::acc)
let elt d =
let elt split_pos d =
match d.d_node with
| Dprop (Pgoal,pr,f) ->
let l = split_pos [] f in
......@@ -92,6 +89,15 @@ let elt d =
(create_prop (id_clone (pr_name pr))) p]) l
| _ -> [[d]]
let t () = Transform.elt' elt
let () = Driver.register_transform' "split_conjunction" t
let split_pos1 = split_pos (fun acc x -> x::acc)
let split_conjunction () = Transform.elt' (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 () = Transform.elt' (elt split_pos2)
let () = Driver.register_transform' "split_conjunction" split_conjunction
let () = Driver.register_transform' "split_to_cnf" split_to_cnf
Markdown is supported
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