Commit d8377cef authored by MARCHE Claude's avatar MARCHE Claude

scheduler in test

parent e9922218
......@@ -192,6 +192,8 @@ let goal_menu g =
(try
let i = try int_of_string s with Failure _ -> raise Not_found in
let p = List.assoc i menu in
(* this was for calling db directly *)
(**
let call =
try
Db.try_prover ~debug:true ~timelimit ~memlimit:0
......@@ -202,6 +204,17 @@ let goal_menu g =
in
call ();
raise Exit
**)
(* this is for calling the scheduler *)
let callback () =
printf "Scheduled goal is finished, you should update@."
in
Scheduler.schedule_proof_attempt
~debug:true ~timelimit ~memlimit:0
~prover:p.prover ~command:p.command ~driver:p.driver
~callback
g;
raise Exit
with Not_found ->
printf "unknown choice@.");
done
......
......@@ -43,82 +43,82 @@ command = "why3-cpulimit %t %m gappa %f 2>&1"
driver = "drivers/gappa.drv"
[prover cvc3_inst]
name = "CVC3"
name = "CVC3 (inst)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst.drv"
[prover z3_inst]
name = "Z3"
name = "Z3 (inst)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst.drv"
[prover cvc3_inst_nbp]
name = "CVC3"
name = "CVC3 (inst+nbp)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_nbp.drv"
[prover z3_inst_nbp]
name = "Z3"
name = "Z3 (inst+nbp)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_nbp.drv"
[prover cvc3_inst_goal]
name = "CVC3"
name = "CVC3 (inst+goal)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_goal.drv"
[prover z3_inst_goal]
name = "Z3"
name = "Z3 (inst+goal)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_goal.drv"
[prover cvc3_inst_goal_nbp]
name = "CVC3"
name = "CVC3 (inst+goal+nbp)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_goal_nbp.drv"
[prover z3_inst_goal_nbp]
name = "Z3"
name = "Z3 (inst+goal+nbp)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_goal_nbp.drv"
[prover cvc3_inst_def]
name = "CVC3"
name = "CVC3 (inst+def)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_def.drv"
[prover z3_inst_def]
name = "Z3"
name = "Z3 (inst+def)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_def.drv"
[prover cvc3_inst_def_nbp]
name = "CVC3"
name = "CVC3 (inst+def+nbp)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_def_nbp.drv"
[prover z3_inst_def_nbp]
name = "Z3"
name = "Z3 (inst+def+nbp)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_def_nbp.drv"
[prover cvc3_inst_mono]
name = "CVC3"
name = "CVC3 (inst+mono)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_mono.drv"
[prover z3_inst_mono]
name = "Z3"
name = "Z3 (inst+mono)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_mono.drv"
[prover cvc3_inst_mono_nbp]
name = "CVC3"
name = "CVC3 (inst+mono+nbp)"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_inst_mono_nbp.drv"
[prover z3_inst_mono_nbp]
name = "Z3"
name = "Z3 (inst+mono+nbp)"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_inst_mono_nbp.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