Skip to content
GitLab
Commit ccbc7d89 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Generate cntexmp according to config file.

parent b7cfc967
Hide whitespace changes
Inline Side-by-side
src/session/controller_itp.ml
View file @ ccbc7d89
......@@ -448,7 +448,7 @@ let register_observer = (:=) observer
module Hprover = Whyconf.Hprover
let build_prover_call c id pr limit callback =
let build_prover_call ~cntexample c id pr limit callback =
let (config_pr,driver) = Hprover.find c.controller_provers pr in
let command =
Whyconf.get_complete_command
......@@ -457,7 +457,7 @@ let build_prover_call c id pr limit callback =
let task = Session_itp.get_task c.controller_session id in
let table = Session_itp.get_table c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
Driver.prove_task ?old:None ~cntexample:cntexample ~inplace:false ~command
~limit ?name_table:table driver task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
......@@ -499,9 +499,9 @@ let timeout_handler () =
try
for _i = Queue.length prover_tasks_in_progress
to 3 * !max_number_of_running_provers do
let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
let (c,id,pr,limit,callback,cntexample) = Queue.pop scheduled_proof_attempts in
try
build_prover_call c id pr limit callback
build_prover_call ~cntexample c id pr limit callback
with e when not (Debug.test_flag Debug.stack_trace) ->
(*Format.eprintf
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
......@@ -525,7 +525,7 @@ let interrupt () =
done;
number_of_running_provers := 0;
while not (Queue.is_empty scheduled_proof_attempts) do
let (_c,_id,_pr,_limit,callback) = Queue.pop scheduled_proof_attempts in
let (_c,_id,_pr,_limit,callback,_cntexample) = Queue.pop scheduled_proof_attempts in
callback Interrupted
done;
!observer 0 0 0
......@@ -537,21 +537,21 @@ let run_timeout_handler () =
S.timeout ~ms:125 timeout_handler;
end
let schedule_proof_attempt_r c id pr ~limit ~callback =
let schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback =
let panid =
graft_proof_attempt c.controller_session id pr ~limit
in
Queue.add (c,id,pr,limit,callback panid) scheduled_proof_attempts;
Queue.add (c,id,pr,limit,callback panid,counterexmp) scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt c id pr ~limit ~callback ~notification =
let schedule_proof_attempt c id pr ~counterexmp ~limit ~callback ~notification =
let callback panid s = callback panid s;
(match s with
| Scheduled | Done _ -> update_goal_node notification c id
| _ -> ())
in
schedule_proof_attempt_r c id pr ~limit ~callback
schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
......@@ -593,7 +593,7 @@ let schedule_transformation c id name args ~callback ~notification =
open Strategy
let run_strategy_on_goal
c id strat ~callback_pa ~callback_tr ~callback ~notification =
c id strat ~counterexmp ~callback_pa ~callback_tr ~callback ~notification =
let rec exec_strategy pc strat g =
if pc < 0 || pc >= Array.length strat then
callback STShalt
......@@ -621,7 +621,7 @@ let run_strategy_on_goal
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ~limit ~callback ~notification
schedule_proof_attempt c g p ~counterexmp ~limit ~callback ~notification
| Itransform(trname,pcsuccess) ->
let callback ntr =
callback_tr ntr;
......@@ -708,7 +708,7 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
raise BadCopyPaste
| APn from_pn, APn to_pn ->
let from_pa_list = get_proof_attempts s from_pn in
List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn
List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn ~counterexmp:false
~callback:callback_pa ~notification) from_pa_list;
let from_tr_list = get_transformations s from_pn in
let callback x st = callback_tr st;
......@@ -751,7 +751,7 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
if not (Hprover.mem c.controller_provers pr) then
callback id (Uninstalled pr)
else
schedule_proof_attempt c parid pr ~limit ~callback ~notification
schedule_proof_attempt c parid pr ~counterexmp:false ~limit ~callback ~notification
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
......
src/session/controller_itp.mli
View file @ ccbc7d89
......@@ -180,6 +180,7 @@ val schedule_proof_attempt :
controller ->
proofNodeID ->
Whyconf.prover ->
counterexmp:bool ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:notifier -> unit
......@@ -206,6 +207,7 @@ val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
counterexmp:bool ->
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(transformation_status -> unit) ->
callback:(strategy_status -> unit) ->
......
src/session/itp_server.ml
View file @ ccbc7d89
......@@ -921,12 +921,12 @@ let get_locations t =
| _ -> ()
with Not_found -> ()
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
let schedule_proof_attempt ~counterexmp nid (p: Whyconf.config_prover) limit =
let d = get_server_data () in
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover ~counterexmp
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
......@@ -966,7 +966,7 @@ let get_locations t =
let debug_strat = Debug.register_flag "strategy_exec" ~desc:"Trace strategies execution"
let run_strategy_on_task nid s =
let run_strategy_on_task ~counterexmp nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
let l = strategies d.cont.controller_env d.config loaded_strategies in
......@@ -980,7 +980,8 @@ let get_locations t =
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr st = callback_update_tree_transform st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
C.run_strategy_on_goal d.cont id st ~counterexmp
~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
| _ -> Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
......@@ -1082,10 +1083,14 @@ let get_locations t =
in
begin match p with
| None -> ()
| Some p -> schedule_proof_attempt nid p limit
| Some p ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main d.config) in
schedule_proof_attempt ~counterexmp nid p limit
end
| Transform_req (nid, t, args) -> apply_transform nid t args
| Strategy_req (nid, st) -> run_strategy_on_task nid st
| Strategy_req (nid, st) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main d.config) in
run_strategy_on_task ~counterexmp nid st
| Clean_req -> clean_session ()
| Save_req -> save_session ()
| Reload_req -> reload_session ()
......@@ -1134,8 +1139,12 @@ let get_locations t =
match (interp commands_table d.config d.cont snid cmd) with
| Transform (s, _t, args) -> treat_request (Transform_req (nid, s, args))
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) -> schedule_proof_attempt nid p limit
| Strategies st -> run_strategy_on_task nid st
| Prove (p, limit) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main d.config) in
schedule_proof_attempt ~counterexmp nid p limit
| Strategies st ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main d.config) in
run_strategy_on_task ~counterexmp nid st
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
......
Supports Markdown
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