Commit 60ada434 authored by Francois Bobot's avatar Francois Bobot

options : -M for defining an exclusif meta on the command line

parent 9f3e9d78
......@@ -471,7 +471,7 @@ install::
DIR_DRIVERS := drivers/
DRIVERS := z3_inst cvc3_inst
DRIVERS := $(DRIVERS) $(addsuffix _def, $(DRIVERS)) \
DRIVERS := $(DRIVERS) $(addsuffix _all, $(DRIVERS)) \
$(addsuffix _goal, $(DRIVERS)) $(addsuffix _mono, $(DRIVERS))
DRIVERS := $(DRIVERS) $(addsuffix _incomplete, $(DRIVERS))
DRIVERS := $(addsuffix .drv, $(DRIVERS))
......
......@@ -3,7 +3,7 @@
DIR=drivers/
for prover in z3 cvc3; do
for what in "" _goal _mono _def; do
for what in "" _goal _mono _all; do
for complete in "" _incomplete; do
cat ${DIR}${prover}.drv |sed -e "s/transformation \"encoding_decorate\"/transformation \"encoding_instantiate$what$complete\"/" > ${DIR}${prover}_inst${what}${complete}.drv
done
......
......@@ -29,6 +29,7 @@ _arguments -s -S \
"(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/ "\
"(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
"(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:->provers"\
'-M'"[<meta_name>,<string> Add a meta option to each tasks]:<meta_name>:->metas:<meta_arg>:"\
"(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
"(-F --format)"'--format'"[same as -F]:<input format>:"\
"(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
......@@ -45,6 +46,7 @@ _arguments -s -S \
'--list-printers'"[List the registered printers]"\
'--list-provers'"[List the known provers]"\
'--list-formats'"[List the known input formats]"\
'--list-metas'"[List the known metas]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--parse-only'"[Stop after parsing]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
'--debug'"[Set the debug flag]"\
......@@ -70,6 +72,11 @@ case $state in
compadd $($cmd --list-provers | egrep -E "^ [a-z]"|cut -d' ' -f 3);
return 0
;;
metas)
_message "<metas>"
compadd "$($cmd --list-metas | egrep -E "^ [a-z]" | sed "s/^[ ]*\(.*\)$/\1/")";
return 0
;;
theories)
tmp=$($cmd --print-namespace $last_file 2> /dev/null);
if [[ $? = 0 ]]; then
......
......@@ -57,7 +57,7 @@ let mm_find mm t =
let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
let mm_add mm t td = if is_meta_exc t
let mm_add mm t td = if is_meta_excl t
then Mstr.add t (tds_singleton td) mm
else Mstr.add t (tds_add td (mm_find mm t)) mm
......@@ -193,8 +193,8 @@ let split_tdecl names (res,task) td = match td.td_node with
| _ ->
res, flat_tdecl task td
let split_theory th names =
fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
let split_theory ?(init=None) th names =
fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
(* Generic utilities *)
......@@ -245,7 +245,7 @@ let find_tagged_pr t tds acc =
exception NotExclusiveMeta of string
let get_meta_exc t tds =
if not (is_meta_exc t) then raise (NotExclusiveMeta t);
if not (is_meta_excl t) then raise (NotExclusiveMeta t);
Stdecl.fold (fun td _ -> match td.td_node with
| Meta (s,_) when s = t -> Some td
| _ -> assert false) tds.tds_set None
......
......@@ -81,7 +81,7 @@ val add_ind_decls : task -> ind_decl list -> task
(** {2 utilities} *)
val split_theory : theory -> Spr.t option -> task list
val split_theory : ?init:task -> theory -> Spr.t option -> task list
(** [split_theory th s] returns the tasks of [th] which end by one
of [s]. They are in the opposite order than in the theory *)
......
......@@ -102,7 +102,7 @@ exception BadMetaArity of string * int * int
exception MetaTypeMismatch of string * meta_arg_type * meta_arg_type
let meta_table = Hashtbl.create 17
let meta_exc = Hashtbl.create 17
let meta_excl = Hashtbl.create 17
let register_meta s al =
begin try
......@@ -111,17 +111,17 @@ let register_meta s al =
with Not_found -> Hashtbl.add meta_table s al end;
s
let register_meta_exc s al =
Hashtbl.add meta_exc s ();
let register_meta_excl s al =
Hashtbl.add meta_excl s ();
register_meta s al
let lookup_meta s =
try Hashtbl.find meta_table s
with Not_found -> raise (UnknownMeta s)
let is_meta_exc s = Hashtbl.mem meta_exc s
let is_meta_excl s = Hashtbl.mem meta_excl s
let list_meta () = Hashtbl.fold (fun k _ acc -> k::acc) meta_table []
let list_metas () = Hashtbl.fold (fun k v acc -> (k,v)::acc) meta_table []
(** Theory *)
......
......@@ -54,13 +54,13 @@ type meta_arg =
| MAstr of string
| MAint of int
val register_meta : string -> meta_arg_type list -> string
val register_meta_exc : string -> meta_arg_type list -> string
val register_meta : string -> meta_arg_type list -> string
val register_meta_excl : string -> meta_arg_type list -> string
val lookup_meta : string -> meta_arg_type list
val is_meta_exc : string -> bool
val lookup_meta : string -> meta_arg_type list
val is_meta_excl : string -> bool
val list_meta : unit -> string list
val list_metas : unit -> (string * meta_arg_type list) list
(** Theory *)
......
......@@ -37,6 +37,7 @@ let opt_queue = Queue.create ()
let opt_input = ref None
let opt_theory = ref None
let opt_trans = ref []
let opt_metas = ref []
let add_opt_file x =
let tlist = Queue.create () in
......@@ -77,6 +78,9 @@ let add_opt_goal x = match !opt_theory with
let add_opt_trans x = opt_trans := x::!opt_trans
let add_opt_meta meta_name meta_arg =
opt_metas := (meta_name,meta_arg)::!opt_metas
let opt_config = ref None
let opt_parser = ref None
let opt_prover = ref None
......@@ -86,6 +90,7 @@ let opt_output = ref None
let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_command = ref None
let opt_task = ref None
let opt_print_theory = ref false
let opt_print_namespace = ref false
......@@ -93,6 +98,7 @@ let opt_list_transforms = ref false
let opt_list_printers = ref false
let opt_list_provers = ref false
let opt_list_formats = ref false
let opt_list_metas = ref false
let opt_parse_only = ref false
let opt_type_only = ref false
......@@ -135,6 +141,11 @@ let option_list = Arg.align [
"<MiB> Set the prover's memory limit (default: no limit)";
"--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
" same as -m";
"-M",
begin let meta_opt = ref "" in
Arg.Tuple ([Arg.Set_string meta_opt;
Arg.String (fun s -> add_opt_meta !meta_opt s)]) end,
"<meta_name>,<string> Add a meta option to each tasks";
"-D", Arg.String (fun s -> opt_driver := Some s),
"<file> Specify a prover's driver (conflicts with -P)";
"--driver", Arg.String (fun s -> opt_driver := Some s),
......@@ -155,6 +166,8 @@ let option_list = Arg.align [
" List the known provers";
"--list-formats", Arg.Set opt_list_formats,
" List the known input formats";
"--list-metas", Arg.Set opt_list_metas,
" List the known metas option (currently only with one string argument)";
"--parse-only", Arg.Set opt_parse_only,
" Stop after parsing";
"--type-only", Arg.Set opt_type_only,
......@@ -169,6 +182,8 @@ let option_list = Arg.align [
let () =
Arg.parse option_list add_opt_file usage_msg;
(* TODO? : Since drivers can dynlink ml code they can add printer,
transformations, ... So drivers should be loaded before listing *)
if !opt_list_transforms then begin
printf "@[<hov 2>Transed non-splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline Pp.string)
......@@ -197,9 +212,20 @@ let () =
let print fmt m = Mstr.iter (print fmt) m in
printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
end;
if !opt_list_metas then begin
let metas = list_metas () in
let filter (s,args) =
match args with
| [MTstring] -> is_meta_excl s
| _ -> false in
let metas = List.filter filter metas in
let metas = List.map fst metas in
printf "@[<hov 2>Known metas:@\n%a@]@\n@."
(Pp.print_list Pp.newline Pp.string)
(List.sort String.compare metas)
end;
if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
!opt_list_formats
!opt_list_formats || !opt_list_metas
then exit 0;
if Queue.is_empty opt_queue then begin
......@@ -245,7 +271,7 @@ let () =
opt_loadpath := List.rev_append !opt_loadpath config.loadpath;
if !opt_timelimit = None then opt_timelimit := config.timelimit;
if !opt_memlimit = None then opt_memlimit := config.memlimit;
match !opt_prover with
begin match !opt_prover with
| Some s ->
let prover = try Mstr.find s config.provers with
| Not_found -> eprintf "Driver %s not found.@." s; exit 1
......@@ -253,7 +279,9 @@ let () =
opt_command := Some prover.command;
opt_driver := Some prover.driver
| None ->
()
() end;
let add_meta task (meta,s) = add_meta task meta [MAstr s] in
opt_task := List.fold_left add_meta !opt_task !opt_metas
let timelimit = match !opt_timelimit with
| None -> 10
......@@ -335,12 +363,12 @@ let do_theory env drv fname tname th trans glist =
let drv = Util.of_option drv in
if Queue.is_empty glist
then
let tasks = List.rev (split_theory th None) in
let tasks = List.rev (split_theory ~init:!opt_task th None) in
let do_tasks = do_tasks env drv fname tname th trans in
List.iter do_tasks tasks
else
let prtrans,prs = Queue.fold add ([],Decl.Spr.empty) glist in
let tasks = split_theory th (Some prs) in
let tasks = split_theory ~init:!opt_task th (Some prs) in
let recover_pr mpr task =
let pr = task_goal task in
Decl.Mpr.add pr task mpr in
......
......@@ -29,6 +29,8 @@ open Decl
let meta_kept = register_meta "encoding_instantiate : kept" [MTtysymbol]
let meta_level = register_meta_excl "encoding_instantiate : level" [MTstring]
(* Ce type est utiliser pour indiquer un alpha *)
let tv_dumb = create_tvsymbol (id_fresh "instantiate_alpha")
......@@ -542,7 +544,7 @@ let () =
Trans.register_env_transform name (encoding_gen get_kept))
["encoding_instantiate",Trans.identity;
"encoding_instantiate_goal", mono_in_goal;
"encoding_instantiate_def", mono_in_def;
"encoding_instantiate_all", mono_in_def;
"encoding_instantiate_mono", mono_in_mono]
......@@ -551,5 +553,5 @@ let () =
Trans.register_transform name (encoding_gen_incomplete get_kept))
["encoding_instantiate_incomplete",Trans.identity;
"encoding_instantiate_goal_incomplete", mono_in_goal;
"encoding_instantiate_def_incomplete", mono_in_def;
"encoding_instantiate_all_incomplete", mono_in_def;
"encoding_instantiate_mono_incomplete", mono_in_mono]
......@@ -102,25 +102,25 @@ name = "Z3 (inst+goal+incomplete)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_goal_incomplete.drv"
[prover cvc3_inst_def]
[prover cvc3_inst_all]
name = "CVC3 (inst+def)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_def.drv"
driver = "drivers/cvc3_inst_all.drv"
[prover z3_inst_def]
[prover z3_inst_all]
name = "Z3 (inst+def)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_def.drv"
driver = "drivers/z3_inst_all.drv"
[prover cvc3_inst_def_incomplete]
[prover cvc3_inst_all_incomplete]
name = "CVC3 (inst+def+incomplete)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_def_incomplete.drv"
driver = "drivers/cvc3_inst_all_incomplete.drv"
[prover z3_inst_def_incomplete]
[prover z3_inst_all_incomplete]
name = "Z3 (inst+def+incomplete)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_def_incomplete.drv"
driver = "drivers/z3_inst_all_incomplete.drv"
[prover cvc3_inst_mono]
......
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