Commit ba1cb1c8 authored by MARCHE Claude's avatar MARCHE Claude

provers in db

parent 4ab0dce6
......@@ -33,10 +33,9 @@ type config = {
provers : config_prover Mstr.t; (* indexed by short identifiers *)
}
(* if conf_file is not given, tries the following:
(** if conf_file is not given, tries the following:
"$WHY_CONFIG"; "./why.conf"; "./.why.conf";
"$HOME/.why.conf"; "$USERPROFILE/.why.conf" *)
val read_config : string option -> config
val save_config : config -> unit
......
......@@ -109,15 +109,16 @@ type proof_attempt_status =
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
type prover_data =
{ prover_name : string;
command : string;
driver : Why.Driver.driver;
type prover =
{ prover_id : int64;
prover_name : string;
}
let prover_name p = p.prover_name
type external_proof = {
mutable external_proof_id : db_ident;
mutable prover : prover_data;
mutable prover : prover;
mutable timelimit : int;
mutable memlimit : int;
mutable status : proof_attempt_status;
......@@ -189,7 +190,73 @@ let rec string_from_origin o =
let goal_name g = string_from_origin g.goal_origin
module Prover = struct
let init db =
let sql =
"CREATE TABLE IF NOT EXISTS prover (prover_id INTEGER PRIMARY KEY AUTOINCREMENT,prover_name TEXT);"
in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
let sql =
"CREATE UNIQUE INDEX IF NOT EXISTS prover_name_idx ON prover (prover_name)"
in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
(*
let delete db pr =
let id = pr.prover_id in
let sql = "DELETE FROM prover WHERE id=?" in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db (fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.INT id));
ignore (step_fold db stmt (fun _ -> ()));
pr.prover_id <- 0L
*)
let add db name =
transaction db
(fun () ->
let sql = "INSERT INTO prover VALUES(NULL,?)" in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT name));
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
{ prover_id = new_id ; prover_name = name })
let get db name =
let sql =
"SELECT prover.prover_id, prover.prover_name FROM prover WHERE prover.prover_name=?"
in
let stmt=Sqlite3.prepare db.raw_db sql in
(* bind the position variables to the statement *)
db_must_ok db
(fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT name));
(* convert statement into record *)
let of_stmt stmt =
{ prover_id =
(match Sqlite3.column stmt 0 with
| Sqlite3.Data.INT i -> i
| x ->
try Int64.of_string (Sqlite3.Data.to_string x)
with _ -> failwith "Db.Prover.get") ;
prover_name =
(match Sqlite3.column stmt 1 with
| x -> Sqlite3.Data.to_string x)
}
in
(* execute the SQL query *)
match step_fold db stmt of_stmt with
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
end
let get_prover n =
let db = current () in
try Prover.get db n
with Not_found -> Prover.add db n
module Loc = struct
let init db =
......@@ -197,6 +264,7 @@ module Loc = struct
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
(* object definition *)
(*
let create (* ?id *) ~file ~line ~start ~stop : loc_record =
{
loc_id = None (* id *);
......@@ -205,6 +273,7 @@ module Loc = struct
start = start;
stop = stop;
}
*)
(* admin functions *)
let delete db loc =
......@@ -393,7 +462,6 @@ let int64_from_pas = function
module External_proof = struct
let init db =
let sql = "create table if not exists external_proof (id integer primary key autoincrement,prover text,timelimit integer,memlimit integer,status integer,result_time real,trace text,obsolete integer);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
......@@ -1158,6 +1226,7 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
}
in
current_db := Some db;
Prover.init db;
Loc.init db;
External_proof.init db;
Goal.init db;
......@@ -1191,7 +1260,8 @@ let string_from_result = function
exception AlreadyAttempted
let try_prover ~timelimit ?memlimit (g : goal) (d: prover_data) : unit -> unit =
let try_prover ~timelimit ?memlimit ~prover:_prover ~command ~driver
(g : goal) : unit -> unit =
(* TODO: check if attempt already present *)
(* TODO: add attempt as "Running" *)
begin
......@@ -1199,22 +1269,25 @@ let try_prover ~timelimit ?memlimit (g : goal) (d: prover_data) : unit -> unit =
| Some _ -> Format.eprintf "Db.try_prover warning: memlimit is ignored@."
end;
Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
let [task] = Why.Driver.apply_transforms d.driver g.task in
Format.eprintf "Task for prover: %a@." (Why.Driver.print_task d.driver) task;
let task = match Why.Driver.apply_transforms driver g.task with
| [t] -> t
| _ -> assert false
in
Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) task;
(*
let callback = Why.Driver.call_prover_ext ~debug:true ~timeout:timelimit d.driver g.task
let callback = Why.Driver.call_prover_ext ~debug:true ~timeout:timelimit d g.task
in
*)
let callback =
let dest =
Why.Driver.file_of_task d.driver "" "" task
Why.Driver.file_of_task driver "" "" task
in
let print_task fmt =
Format.fprintf fmt "@[%a@]@?" (Why.Driver.print_task d.driver) task
Format.fprintf fmt "@[%a@]@?" (Why.Driver.print_task driver) task
in
let regexps = Why.Driver.get_regexps d.driver in
let regexps = Why.Driver.get_regexps driver in
Why.Call_provers.call_on_formatter ~debug:true ~suffix:dest
~command:d.command ~timelimit ~memlimit:0 ~regexps print_task
~command ~timelimit ~memlimit:0 ~regexps print_task
in
fun () ->
let r = callback () in
......
......@@ -53,6 +53,14 @@ type loc_record
}
*)
(** prover data *)
type prover
val prover_name : prover -> string
val get_prover : string -> prover
(** status of an external proof attempt *)
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
......@@ -62,15 +70,9 @@ type proof_attempt_status =
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
type prover_data =
{ prover_name : string;
command : string;
driver : Why.Driver.driver;
}
type external_proof
val prover : external_proof -> prover_data
val prover : external_proof -> prover
val timelimit : external_proof -> int
val memlimit : external_proof -> int
val status : external_proof -> proof_attempt_status
......@@ -157,7 +159,8 @@ val root_goals : unit -> goal list
exception AlreadyAttempted
val try_prover :
timelimit:int -> ?memlimit:int -> goal -> prover_data -> (unit -> unit)
timelimit:int -> ?memlimit:int -> prover:prover -> command:string ->
driver:Why.Driver.driver -> goal -> (unit -> unit)
(** attempts to prove goal with the given prover. This function
prepares the goal for that prover, adds it as an new
external_proof attempt, setting its current status to Running,
......
......@@ -58,11 +58,20 @@ let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.l
let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
let fname = "tests/test-claude"
let () = Db.init_base (fname ^ ".db")
let get_driver name =
let pi = Util.Mstr.find name config.provers in
Why.Driver.load_driver pi.Whyconf.driver env
type prover_data =
{ prover : Db.prover;
command : string;
driver : Why.Driver.driver;
}
let provers_data =
printf "Provers: ";
let l =
......@@ -70,9 +79,9 @@ let provers_data =
(fun id conf acc ->
let name = conf.Whyconf.name in
printf " %s, " name;
{ Db.prover_name = name;
Db.command = conf.Whyconf.command;
Db.driver = get_driver id; } :: acc
{ prover = Db.get_prover name;
command = conf.Whyconf.command;
driver = get_driver id; } :: acc
) config.provers []
in
printf "@.";
......@@ -80,11 +89,6 @@ let provers_data =
let fname = "tests/test-claude"
let () = Db.init_base (fname ^ ".prm")
let () =
printf "previously known goals:@\n";
List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
......@@ -190,7 +194,7 @@ let goal_menu g =
let _,menu = List.fold_left
(fun (i,acc) p ->
let i = succ i in
printf "%2d: try %s@." i p.Db.prover_name;
printf "%2d: try %s@." i (Db.prover_name p.prover);
(i,(i,p)::acc)) (0,[]) provers_data
in
printf "Select a choice:@.";
......@@ -199,7 +203,7 @@ let goal_menu g =
let i = int_of_string s in
if i=0 then raise Exit;
let p = List.assoc i menu in
let call = Db.try_prover ~timelimit:10 g p in
let call = Db.try_prover ~timelimit:config.timelimit ~prover:p.prover ~command:p.command ~driver:p.driver g in
call ()
with Not_found | Failure _ ->
printf "unknown choice@.");
......
[main]
library = "theories"
timelimit = 10
timelimit = 2
[prover alt-ergo]
name = "Alt-Ergo"
......@@ -18,7 +18,7 @@ command = "cvc3 -lang smt"
driver = "drivers/cvc3.drv"
[prover z3]
name = "Z3 en mieux"
name = "Z3"
command = "why-cpulimit %t z3 -smt %f"
driver = "drivers/z3.drv"
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