Commit d1ff6736 authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: calling Alt-Ergo works !

parent 43047de3
...@@ -1433,17 +1433,33 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \ ...@@ -1433,17 +1433,33 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-I $(ALTERGODIR)/src/util \ -I $(ALTERGODIR)/src/util \
-I $(ALTERGODIR)/src/structures \ -I $(ALTERGODIR)/src/structures \
-I $(ALTERGODIR)/src/parsing \ -I $(ALTERGODIR)/src/parsing \
-I $(ALTERGODIR)/src/preprocess -I $(ALTERGODIR)/src/preprocess \
-I $(ALTERGODIR)/src/theories \
-I $(ALTERGODIR)/src/instances \
-I $(ALTERGODIR)/src/sat \
-I $(ALTERGODIR)/src/main
ALTERGOMODS=util/numsNumbers util/numbers \ ALTERGOMODS=util/numsNumbers util/numbers \
util/version util/myUnix util/config util/options \ util/version util/myUnix util/config util/options \
util/hashcons util/hstring util/lists util/loc \ util/hashcons util/hstring util/lists util/loc \
util/profiling_default util/profiling \
util/util \
structures/parsed structures/symbols \ structures/parsed structures/symbols \
structures/ty structures/errors \ structures/ty structures/errors \
structures/term structures/literal structures/formula \ structures/term structures/literal structures/formula \
structures/explanation structures/exception \
parsing/why_parser parsing/why_lexer \ parsing/why_parser parsing/why_lexer \
preprocess/existantial preprocess/triggers \ preprocess/existantial preprocess/triggers \
preprocess/why_typing preprocess/cnf preprocess/why_typing preprocess/cnf \
theories/polynome theories/ac \
theories/intervals theories/inequalities \
theories/intervalCalculus \
theories/arith theories/records theories/bitv \
theories/arrays theories/sum theories/uf theories/use \
theories/combine theories/ccx theories/theory \
instances/matching \
sat/sat_solvers \
main/frontend
TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS))) TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
......
(* (* simple helpers *)
small helpers
*)
let get_opt o = Js.Opt.get o (fun () -> assert false) let get_opt o = Js.Opt.get o (fun () -> assert false)
let log s = Firebug.console ## log (Js.string s) let log s = Firebug.console ## log (Js.string s)
(*
module for generating HTML elements (* module for generating HTML elements *)
*)
module Html = struct module Html = struct
...@@ -40,11 +33,8 @@ let ul nl = ...@@ -40,11 +33,8 @@ let ul nl =
end end
(*
Interface to Why3 and Alt-Ergo
*) (* Interface to Why3 and Alt-Ergo *)
let why3_conf_file = "/trywhy3.conf" let why3_conf_file = "/trywhy3.conf"
...@@ -79,6 +69,18 @@ let alt_ergo_driver : Driver.driver = ...@@ -79,6 +69,18 @@ let alt_ergo_driver : Driver.driver =
Exn_printer.exn_printer e s; Exn_printer.exn_printer e s;
exit 1 exit 1
module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
module FE = Frontend.Make (SAT)
let print_status fmt _d status steps =
match status with
| FE.Unsat _dep ->
fprintf fmt "Proved (%Ld steps)" steps
| FE.Inconsistent -> ()
(* fprintf fmt "Inconsistent assumption" *)
| FE.Unknown _t | FE.Sat _t ->
fprintf fmt "Unknown (%Ld steps)@." steps
let run_alt_ergo_on_task t = let run_alt_ergo_on_task t =
(* printing the task in a string *) (* printing the task in a string *)
Driver.print_task alt_ergo_driver str_formatter t; Driver.print_task alt_ergo_driver str_formatter t;
...@@ -93,14 +95,14 @@ let run_alt_ergo_on_task t = ...@@ -93,14 +95,14 @@ let run_alt_ergo_on_task t =
| [d] -> | [d] ->
let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
(* (*
SAT.reset_steps (); fprintf str_formatter
List.iter "Alt-Ergo: %d command(s) to process" (Queue.length d);
(fun cnf ->
ignore (Queue.fold (FE.process_decl FE.print_status)
(SAT.empty (), true, Explanation.empty) cnf)
) d
*) *)
"Alt-Ergo: " ^ string_of_int (Queue.length d) ^ " command(s) to process" SAT.reset_steps ();
let _x = Queue.fold (FE.process_decl (print_status str_formatter))
(SAT.empty (), true, Explanation.empty) d
in
flush_str_formatter ()
| _ -> "error: zero or more than 1 goal to solve" | _ -> "error: zero or more than 1 goal to solve"
let split_trans = Trans.lookup_transform_l "split_goal_wp" env let split_trans = Trans.lookup_transform_l "split_goal_wp" env
...@@ -182,11 +184,8 @@ let why3_execute (modules,_theories) = ...@@ -182,11 +184,8 @@ let why3_execute (modules,_theories) =
in in
Html.ul mods Html.ul mods
(*
Connecting why3 calls to the interface
*) (* Connecting Why3 calls to the interface *)
let temp_file_name = "/input.mlw" let temp_file_name = "/input.mlw"
...@@ -246,11 +245,7 @@ let () = ...@@ -246,11 +245,7 @@ let () =
add_why3_cmd "run" why3_execute Mlw_module.mlw_language add_why3_cmd "run" why3_execute Mlw_module.mlw_language
(* (* Predefined examples *)
Predefined examples
*)
let add_file_example buttonname file = let add_file_example buttonname file =
let handler = Dom.handler let handler = Dom.handler
...@@ -274,7 +269,8 @@ let () = ...@@ -274,7 +269,8 @@ let () =
add_file_example "drinkers" "/drinkers.why"; add_file_example "drinkers" "/drinkers.why";
(* add_file_example "simplearith" "/simplearith.why";*) (* add_file_example "simplearith" "/simplearith.why";*)
add_file_example "bin_mult" "/bin_mult.mlw"; add_file_example "bin_mult" "/bin_mult.mlw";
add_file_example "isqrt" "/isqrt.mlw" add_file_example "isqrt" "/isqrt.mlw";
Options.set_steps_bound 100
(* (*
......
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