Commit e1635f0e authored by François Bobot's avatar François Bobot
Browse files

bench : db.ml doesnt use AlreadyDefined, so don't use it

parent b33ce30f
......@@ -19,6 +19,7 @@
open Thread
open Why
open Util
open Env
open Theory
open Task
......@@ -175,12 +176,19 @@ let apply_trans (task,db_goal) (trans,db_trans) =
let task = Trans.apply trans task in
match db_goal, db_trans with
| Some db_goal, Some db_trans ->
let transf = try Db.add_transformation db_goal db_trans
with Db.AlreadyExist ->
Db.Htransf.find (Db.transformations db_goal) db_trans in
let db_goal = Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
(task_checksum task) in
let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
with Not_found ->
Db.add_transformation db_goal db_trans
in
let md5 = task_checksum task in
let db_goal =
try
Mstr.find md5 (Db.subgoals transf)
with Not_found ->
Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
md5
in
(task,Some db_goal)
| _ -> ((task:task),None)
......@@ -188,13 +196,19 @@ let apply_transl (task,db_goal) (trans,db_trans) =
let tasks = Trans.apply trans task in
match db_goal, db_trans with
| Some db_goal, Some db_trans ->
let transf = try Db.add_transformation db_goal db_trans
with Db.AlreadyExist ->
Db.Htransf.find (Db.transformations db_goal) db_trans in
let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
with Not_found -> Db.add_transformation db_goal db_trans
in
let map task =
let db_goal = Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
(task_checksum task) in
let md5 = task_checksum task in
let db_goal =
try
Mstr.find md5 (Db.subgoals transf)
with Not_found ->
Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
md5
in
(task,Some db_goal) in
List.map map tasks
| _ -> List.map (fun task -> (task:task),None) tasks
......@@ -225,23 +239,29 @@ let call callback tool prob =
| Some db_goal, Some db_tool ->
let proof_attempt =
try
Db.Hprover.find (Db.external_proofs db_goal) db_tool
with Not_found ->
Db.add_proof_attempt db_goal db_tool
with Db.AlreadyExist ->
Db.Hprover.find (Db.external_proofs db_goal) db_tool in
in
let (proof_status,time,_,_) = Db.status_and_time proof_attempt in
Debug.dprintf debug "Database has %a for the goal@."
print_prover_answer proof_status;
Debug.dprintf debug "Database has (%a,%f) for the goal@."
print_prover_answer proof_status time;
begin
if proof_status = Db.Success ||
(proof_status = Db.Timeout && time > float tool.ttime) then
(proof_status = Db.Timeout && time > (float tool.ttime -. 0.1))
then
callback pval i task (Cached (proof_status,time))
else
let cb res =
let (status,time) = proof_status_to_db_result res in
callback pval i task (Runned (Done (status,time)));
Db.set_status proof_attempt status time
in
new_external_proof pval i cb task
begin
Debug.dprintf debug "@.time = %f %i@.@."
time tool.ttime;
let cb res =
let (status,time) = proof_status_to_db_result res in
callback pval i task (Runned (Done (status,time)));
Db.set_status proof_attempt status time
in
new_external_proof pval i cb task
end
end
| _ ->
let cb res =
......
......@@ -113,13 +113,14 @@ let apply_use_before_goal (task,goal_id) (th_use,th_use_id) =
| Some goal_id, Some th_use_id ->
Some begin
let transf =
try Db.add_transformation goal_id th_use_id
with Db.AlreadyExist ->
Db.Htransf.find (Db.transformations goal_id) th_use_id in
try Db.Htransf.find (Db.transformations goal_id) th_use_id
with Not_found ->
Db.add_transformation goal_id th_use_id in
let name2 = (Task.task_goal task2).Decl.pr_name.Ident.id_string in
let md5_2 = task_checksum task2 in
try Db.add_subgoal transf name2 md5_2
with Db.AlreadyExist -> Mstr.find md5_2 (Db.subgoals transf)
try Mstr.find md5_2 (Db.subgoals transf)
with Not_found ->
Db.add_subgoal transf name2 md5_2
end
| _,_ -> None in
(task,goal_id)
......@@ -136,22 +137,24 @@ let gen_from_file ~format ~prob_name ~file_path ~file_name env lth =
Mnm.bindings m in
let file_db = file_name (* TODO relativise it with db file path*) in
let file_id = if Db.is_initialized () then Some
(try Db.add_file file_db
with Db.AlreadyExist ->
fst (List.find (fun (_,x) -> file_db = x) (Db.files ())))
(try fst (List.find (fun (_,x) -> file_db = x) (Db.files ()))
with Not_found ->
Db.add_file file_db)
else None in
let map (th_name,th) =
let theory_id = option_map (fun file_id ->
try Db.add_theory file_id th_name
with Db.AlreadyExist -> Mstr.find th_name (Db.theories file_id)
try Mstr.find th_name (Db.theories file_id)
with Not_found ->
Db.add_theory file_id th_name
) file_id in
(* TODO make DB aware of the env *)
let tasks = Task.split_theory th None None in
let map task =
let goal_id = option_map (fun theory_id ->
let name = (Task.task_goal task).Decl.pr_name.Ident.id_string in
try Db.add_goal theory_id name (task_checksum task)
with Db.AlreadyExist -> Mstr.find name (Db.goals theory_id)
try Mstr.find name (Db.goals theory_id)
with Not_found ->
Db.add_goal theory_id name (task_checksum task)
) theory_id in
let (task,goal_id) = List.fold_left apply_use_before_goal
(task,goal_id) lth in
......
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