diff --git a/Makefile.in b/Makefile.in
index 66dc042e6ed52c072c0f585affb346c66ef8c15b..63d3246d314cbbacc52be69b621f5ac0d913178c 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -607,7 +607,7 @@ clean::
##############
SERVER_MODULES := logging arraylist options queue readbuf request \
- writebuf server-unix server-win
+ proc writebuf server-unix server-win
CPULIM_MODULES := cpulimit-unix cpulimit-win
diff --git a/src/core/ident.ml b/src/core/ident.ml
index 0bf75e75819df8b942b82044a2e3ea2c304a40df..04e8b20d42c13022edeccb749ea59b8fb6fd2407 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -368,7 +368,8 @@ let append_to_model_element_name ~attrs ~to_append =
let splitted = Strings.bounded_split '@' attr_str 2 in
match splitted with
| [before; after] -> before ^ to_append ^ "@" ^ after
- | _ -> attr_str^to_append in
+ | _ -> attr_str^to_append
+ in
transform_model_trace_attr attrs trans
let append_to_model_trace_attr ~attrs ~to_append =
diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml
index 3254e923790c6d3e7a520718ec1c444cd831757f..edeed352e7ff11f05c176139bd268fe510afc8bb 100644
--- a/src/core/model_parser.ml
+++ b/src/core/model_parser.ml
@@ -37,8 +37,11 @@ type float_type =
| Float_hexa of string * float
-let interp_float b eb sb =
+let interp_float ?(interp=true) b eb sb =
try
+ (* We don't interpret when this is disable *)
+ if not interp then
+ raise Exit;
let is_neg = match b with
| "#b0" -> false
| "#b1" -> true
diff --git a/src/core/model_parser.mli b/src/core/model_parser.mli
index 4928c6202c824d7447e11904266baec8a978048a..9d51e1fdedf388f62dc7fddc63b23fecc35c93a9 100644
--- a/src/core/model_parser.mli
+++ b/src/core/model_parser.mli
@@ -24,7 +24,7 @@ type float_type =
| Float_value of string * string * string
| Float_hexa of string * float
-val interp_float: string -> string -> string -> float_type
+val interp_float: ?interp:bool -> string -> string -> string -> float_type
type model_value =
| Integer of string
diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml
index 4f14ea753574ecfdd920cb0bfad4a6c4120be907..61705f8708927f223e8ddcc6cbce74676c432e71 100644
--- a/src/driver/call_provers.ml
+++ b/src/driver/call_provers.ml
@@ -551,3 +551,5 @@ let call_editor ~command fin =
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in;
EditorCall pid
+
+let interrupt_call id = Prove_client.send_interrupt ~id
diff --git a/src/driver/call_provers.mli b/src/driver/call_provers.mli
index 070a07bd84f1e861977b5c884ae7b25821991e77..61f2545ea006fea85e99bcfc6bf87f48105dd38a 100644
--- a/src/driver/call_provers.mli
+++ b/src/driver/call_provers.mli
@@ -179,3 +179,5 @@ val query_call : prover_call -> prover_update
val wait_on_call : prover_call -> prover_result
(** blocking function that waits until the prover finishes. *)
+
+val interrupt_call : int -> unit
diff --git a/src/driver/parse_smtv2_model_lexer.mll b/src/driver/parse_smtv2_model_lexer.mll
index 08785cee9fa10bb42c6c6ab78f9e790bcc837477..0989693e25edd7c31afee6e53d79ec2248d2e3c1 100644
--- a/src/driver/parse_smtv2_model_lexer.mll
+++ b/src/driver/parse_smtv2_model_lexer.mll
@@ -59,6 +59,7 @@ rule token = parse
| "true" { TRUE }
| "false" { FALSE }
| "LAMBDA" { LAMBDA }
+ | "lambda" { LAMBDA }
| "ARRAY_LAMBDA" { ARRAY_LAMBDA }
| "(_" space+ "bv"(num as bv_value) space+ num")" { BITVECTOR_VALUE bv_value }
| "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
diff --git a/src/driver/prove_client.ml b/src/driver/prove_client.ml
index 11acd25ebf5bba35f7248c17eca6623b7f06e3f4..9e00e84026c977259469bb00b063a7e9d928c174 100644
--- a/src/driver/prove_client.ml
+++ b/src/driver/prove_client.ml
@@ -165,6 +165,14 @@ let send_request ~id ~timelimit ~memlimit ~use_stdin ~cmd =
let s = Buffer.contents send_buf in
send_request_string s
+let send_interrupt ~id =
+ if not (is_connected ()) then connect_internal ();
+ Buffer.clear send_buf;
+ Buffer.add_string send_buf "interrupt;";
+ Buffer.add_string send_buf (string_of_int id);
+ let s = Buffer.contents send_buf in
+ send_request_string s
+
let rec read_lines blocking =
let s = read_from_client blocking in
(* TODO: should we detect and handle EOF here? *)
diff --git a/src/driver/prove_client.mli b/src/driver/prove_client.mli
index 11cb0611cdf03e376830085e7f33dc9562cd5ba6..928f19d0dcbb666aaebf7ad0b0c7e6b750bb7a16 100644
--- a/src/driver/prove_client.mli
+++ b/src/driver/prove_client.mli
@@ -42,6 +42,8 @@ val send_request :
cmd:string list ->
unit
+val send_interrupt : id:int -> unit
+
type final_answer = {
id : int;
time : float;
diff --git a/src/server/proc.c b/src/server/proc.c
new file mode 100644
index 0000000000000000000000000000000000000000..9ffc5646f79a4b3dee55d210f703b87faeb0fbde
--- /dev/null
+++ b/src/server/proc.c
@@ -0,0 +1,42 @@
+#include <signal.h>
+#include <stdlib.h>
+#include <string.h>
+#include "proc.h"
+#include "options.h"
+
+// global pointers are initialized with NULL by C semantics
+plist processes;
+
+// kill process using os specific routine
+void os_kill(pproc p);
+
+void os_kill(pproc p) {
+#ifdef _WIN32
+ // arbitrarily chosen exit code
+ TerminateProcess(p->handle, ERROR_REQUEST_ABORTED);
+#else
+ kill(p->id, SIGKILL);
+#endif
+}
+
+void init_process_list () {
+ processes = init_list(parallel);
+}
+
+void kill_processes(char *id) {
+ for (int i = 0; i < processes->len; i++) {
+ if (!strcmp(((pproc)(processes->data[i]))->task_id, id)) {
+ os_kill((pproc)processes->data[i]);
+ }
+ }
+}
+
+void free_process(pproc proc) {
+#ifdef _WIN32
+ CloseHandle(proc->handle);
+ CloseHandle(proc->job);
+#endif
+ free(proc->outfile);
+ free(proc->task_id);
+ free(proc);
+}
diff --git a/src/server/proc.h b/src/server/proc.h
new file mode 100644
index 0000000000000000000000000000000000000000..906619c683a02095dda3b8b7c79c5bddfbf33459
--- /dev/null
+++ b/src/server/proc.h
@@ -0,0 +1,35 @@
+#ifndef PROC_H
+#define PROC_H
+
+#ifdef _WIN32
+#include <windows.h>
+#else
+#include <sys/types.h>
+#endif
+
+#include "arraylist.h"
+
+typedef struct {
+#ifdef _WIN32
+ HANDLE handle;
+ HANDLE job;
+#else
+ pid_t id;
+#endif
+ int client_key;
+ char* task_id;
+ char* outfile;
+} t_proc, *pproc;
+
+extern plist processes;
+
+// free memory and resources associated with the process p
+void free_process(pproc p);
+
+// kill all processes whose task_id is equal to id
+void kill_processes(char *id);
+
+// initialize global list of processes
+void init_process_list();
+
+#endif
diff --git a/src/server/server-unix.c b/src/server/server-unix.c
index 97d941c04168161f66b70e492bc9a2223ba73f76..3b1cfd9d870763748e6d16639d7b9ba638f7c98f 100644
--- a/src/server/server-unix.c
+++ b/src/server/server-unix.c
@@ -27,7 +27,6 @@
#include <poll.h>
#include <stddef.h>
#include <stdlib.h>
-#include <string.h>
#include <signal.h>
#include <sys/time.h>
#include <sys/wait.h>
@@ -41,6 +40,7 @@
#include "writebuf.h"
#include "options.h"
#include "logging.h"
+#include "proc.h"
#define READ_ONCE 1024
@@ -53,13 +53,6 @@ typedef struct {
int server_sock = -1;
-typedef struct {
- pid_t id;
- int client_fd;
- char* task_id;
- char* outfile;
-} t_proc, *pproc;
-
// the poll list is the list of file descriptors for which we monitor certain
// events.
struct pollfd* poll_list;
@@ -67,7 +60,6 @@ int poll_num = 0;
int poll_len = 0;
// global pointers are initialized with NULL by C semantics
-plist processes;
plist clients;
char *current_dir;
@@ -275,7 +267,7 @@ void server_init_listening(char* socketname, int parallel) {
free(socketname_copy1);
free(socketname_copy2);
add_to_poll_list(server_sock, POLLIN);
- processes = init_list(parallel);
+ init_process_list();
setup_child_pipe();
}
@@ -427,12 +419,6 @@ void send_msg_to_client(pclient client,
queue_write(client, msgbuf);
}
-void free_process(pproc proc) {
- free(proc->outfile);
- free(proc->task_id);
- free(proc);
-}
-
void handle_child_events() {
pproc child;
pclient client;
@@ -461,7 +447,7 @@ void handle_child_events() {
}
child = (pproc) list_lookup(processes, pid);
list_remove(processes, pid);
- client = (pclient) list_lookup(clients, child->client_fd);
+ client = (pclient) list_lookup(clients, child->client_key);
if (client != NULL) {
send_msg_to_client(client,
child->task_id,
@@ -500,7 +486,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->task_id = r->id;
- proc->client_fd = r->key;
+ proc->client_key = r->key;
proc->id = id;
proc->outfile = outfile;
list_append(processes, id, (void*) proc);
@@ -538,8 +524,7 @@ void handle_msg(pclient client, int key) {
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
remove_from_queue(r->id);
- // kill all processes whose id is r->id;
- // TODO kill_processes(processes, r->id);
+ kill_processes(r->id);
free_request(r);
break;
}
diff --git a/src/server/server-win.c b/src/server/server-win.c
index 50aa60e99bb3a10ce137ecc15876279b5b2bbe72..ff3f8ebfce0bd69d10342315544216af60f3c413 100644
--- a/src/server/server-win.c
+++ b/src/server/server-win.c
@@ -32,6 +32,7 @@
#include "writebuf.h"
#include "arraylist.h"
#include "logging.h"
+#include "proc.h"
#define READ_ONCE 1024
#define BUFSIZE 4096
@@ -62,14 +63,6 @@ typedef struct {
pwritebuf writebuf;
} t_client, *pclient;
-typedef struct {
- HANDLE handle;
- HANDLE job;
- int client_key;
- char* id;
- char* outfile;
-} t_proc, *pproc;
-
// AFAIU, there is no connection queue or something like that, so we need to
// create several socket instances to be able to process several clients that
// would connect almost at the same time. The two variables below will be
@@ -79,7 +72,6 @@ pserver* server_socket;
int* server_key;
plist clients;
-plist processes;
char current_dir[MAX_PATH];
int gen_key = 1;
@@ -109,7 +101,6 @@ HANDLE completion_port;
void shutdown_with_msg(char* msg);
void shutdown_with_msg(char* msg) {
- pproc proc;
if (completion_port != NULL) {
CloseHandle (completion_port);
}
@@ -125,9 +116,7 @@ void shutdown_with_msg(char* msg) {
}
if (processes != NULL) {
for (int i = 0; i < list_length(processes); i++) {
- proc = processes->data[i];
- CloseHandle(proc->handle);
- CloseHandle(proc->job);
+ free_process(processes->data[i]);
}
}
logging_shutdown(msg);
@@ -430,7 +419,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->handle = pi.hProcess;
proc->job = ghJob;
- proc->id = r->id;
+ proc->task_id = r->id;
proc->client_key = r->key;
proc->outfile = outfile;
key = keygen();
@@ -469,7 +458,10 @@ void handle_msg(pclient client, int key) {
break;
case REQ_INTERRUPT:
remove_from_queue(r->id);
- // TODO: remove r from the queue if still there, or kill the process r->id;
+ kill_processes(r->id);
+ // no need to clean up the list of processes and free the memory for
+ // processes, this will be done when we get notified of the end of the
+ // child process
free_request(r);
break;
}
@@ -502,14 +494,6 @@ void accept_client(int key, int socket_num) {
do_read(client);
}
-void free_process(pproc proc) {
- CloseHandle(proc->handle);
- CloseHandle(proc->job);
- free(proc->id);
- free(proc->outfile);
- free(proc);
-}
-
void send_started_msg_to_client(pclient client,
char* id) {
char* msgbuf;
@@ -621,7 +605,7 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
timeout = (exitcode == ERROR_NOT_ENOUGH_QUOTA) ||
(exitcode == STATUS_QUOTA_EXCEEDED);
send_msg_to_client(client,
- child->id,
+ child->task_id,
exitcode,
cpu_time,
timeout,
@@ -648,7 +632,7 @@ void init() {
init_request_queue();
clients = init_list(parallel);
- processes = init_list(parallel);
+ init_process_list();
server_socket = (pserver*) malloc(parallel * sizeof(pserver));
server_key = (int*) malloc(parallel * sizeof(int));
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index c9941cc95e8db6b630602ad679a3ac875056d60f..c2eb78850e98da0130ffc29d38a3d8712b564bc4 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -262,9 +262,34 @@ end
module Make(S : Scheduler) = struct
-let scheduled_proof_attempts = Queue.create ()
+(* type for scheduled proof attempts *)
+type sched_pa_rec =
+ { spa_contr : controller;
+ spa_id : proofNodeID;
+ spa_pr : Whyconf.prover;
+ spa_limit : Call_provers.resource_limit;
+ spa_pr_scr : string option;
+ spa_callback : (proof_attempt_status -> unit);
+ spa_ores : Call_provers.prover_result option;
+ }
+
+let scheduled_proof_attempts : sched_pa_rec Queue.t = Queue.create ()
+
+(* type for prover tasks in progress *)
+type tasks_prog_rec =
+ {
+ tp_session : Session_itp.session;
+ tp_id : proofNodeID;
+ tp_pr : Whyconf.prover;
+ tp_callback : (proof_attempt_status -> unit);
+ tp_started : bool;
+ tp_call : Call_provers.prover_call;
+ tp_ores : Call_provers.prover_result option;
+ }
-let prover_tasks_in_progress = Hashtbl.create 17
+let prover_tasks_in_progress :
+ (Call_provers.prover_call,tasks_prog_rec) Hashtbl.t =
+ Hashtbl.create 17
(* We need to separate tasks that are edited from proofattempt in progress
because we are not using why3server for the edited proofs and timeout_handler
@@ -282,9 +307,7 @@ let register_observer = (:=) observer
module Hprover = Whyconf.Hprover
-(* calling provers, with limits adaptation
-
- *)
+(* calling provers, with limits adaptation *)
(* to avoid corner cases when prover results are obtained very closely
@@ -356,28 +379,38 @@ let fuzzy_proof_time nres ores =
else nres
-let build_prover_call ?proof_script c id pr limit callback ores =
- let (config_pr,driver) = Hprover.find c.controller_provers pr in
- let with_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
+let build_prover_call spa =
+ let c = spa.spa_contr in
+ let limit = spa.spa_limit in
+ let (config_pr,driver) = Hprover.find c.controller_provers spa.spa_pr in
+ let with_steps =
+ Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let command =
Whyconf.get_complete_command config_pr ~with_steps in
try
- let task = Session_itp.get_task c.controller_session id in
+ let task = Session_itp.get_task c.controller_session spa.spa_id in
Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
- (Pp.print_option Pp.string) proof_script;
+ (Pp.print_option Pp.string) spa.spa_pr_scr;
let inplace = config_pr.Whyconf.in_place in
let interactive = config_pr.Whyconf.interactive in
try
let call =
- Driver.prove_task ?old:proof_script ~inplace ~command
- ~limit ~interactive driver task
+ Driver.prove_task ?old:spa.spa_pr_scr ~inplace ~command
+ ~limit ~interactive driver task
in
- let pa = (c.controller_session,id,pr,callback,false,call,ores) in
+ let pa =
+ { tp_session = c.controller_session;
+ tp_id = spa.spa_id;
+ tp_pr = spa.spa_pr;
+ tp_callback = spa.spa_callback;
+ tp_started = false;
+ tp_call = call;
+ tp_ores = spa.spa_ores } in
Hashtbl.replace prover_tasks_in_progress call pa
with Sys_error _ as e ->
- callback (InternalFailure e)
+ spa.spa_callback (InternalFailure e)
with Not_found (* goal has no task, it is detached *) ->
- callback Detached
+ spa.spa_callback Detached
let update_observer () =
let scheduled = Queue.length scheduled_proof_attempts in
@@ -393,31 +426,31 @@ let timeout_handler () =
let results = Call_provers.get_new_results ~blocking:S.blocking in
List.iter (fun (call, prover_update) ->
match Hashtbl.find prover_tasks_in_progress call with
- | (ses,id,pr,callback,started,call,ores) ->
+ | ptp ->
begin match prover_update with
| Call_provers.NoUpdates -> ()
| Call_provers.ProverStarted ->
- assert (not started);
- callback Running;
+ assert (not ptp.tp_started);
+ ptp.tp_callback Running;
incr number_of_running_provers;
- Hashtbl.replace prover_tasks_in_progress call
- (ses,id,pr,callback,true,call,ores)
+ Hashtbl.replace prover_tasks_in_progress ptp.tp_call
+ {ptp with tp_started = true}
| Call_provers.ProverFinished res ->
- Hashtbl.remove prover_tasks_in_progress call;
- if started then decr number_of_running_provers;
- let res = Opt.fold fuzzy_proof_time res ores in
+ Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
+ if ptp.tp_started then decr number_of_running_provers;
+ let res = Opt.fold fuzzy_proof_time res ptp.tp_ores in
(* inform the callback *)
- callback (Done res)
+ ptp.tp_callback (Done res)
| Call_provers.ProverInterrupted ->
- Hashtbl.remove prover_tasks_in_progress call;
- if started then decr number_of_running_provers;
+ Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
+ if ptp.tp_started then decr number_of_running_provers;
(* inform the callback *)
- callback (Interrupted)
+ ptp.tp_callback (Interrupted)
| Call_provers.InternalFailure exn ->
- Hashtbl.remove prover_tasks_in_progress call;
- if started then decr number_of_running_provers;
+ Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
+ if ptp.tp_started then decr number_of_running_provers;
(* inform the callback *)
- callback (InternalFailure (exn))
+ ptp.tp_callback (InternalFailure (exn))
end
| exception Not_found -> ()
(* We probably received ProverStarted after ProverFinished,
@@ -454,12 +487,10 @@ let timeout_handler () =
try
for _i = Hashtbl.length prover_tasks_in_progress
to S.multiplier * !session_max_tasks do
- let (c,id,pr,limit,proof_script,callback,ores) =
- Queue.pop scheduled_proof_attempts in
- try
- build_prover_call ?proof_script c id pr limit callback ores
+ let spa = Queue.pop scheduled_proof_attempts in
+ try build_prover_call spa
with e when not (Debug.test_flag Debug.stack_trace) ->
- callback (InternalFailure e)
+ spa.spa_callback (InternalFailure e)
done
with Queue.Empty -> ()
end;
@@ -468,8 +499,7 @@ let timeout_handler () =
let interrupt () =
(* Interrupt provers *)
- Hashtbl.iter (fun _k e ->
- let (_, _, _, callback, _, _, _) = e in callback Interrupted)
+ Hashtbl.iter (fun _k e -> e.tp_callback Interrupted)
prover_tasks_in_progress;
Hashtbl.clear prover_tasks_in_progress;
(* Do not interrupt editors
@@ -481,9 +511,8 @@ let interrupt () =
*)
number_of_running_provers := 0;
while not (Queue.is_empty scheduled_proof_attempts) do
- let (_c,_id,_pr,_limit,_proof_script,callback,_ores) =
- Queue.pop scheduled_proof_attempts in
- callback Interrupted
+ let spa = Queue.pop scheduled_proof_attempts in
+ spa.spa_callback Interrupted
done;
!observer 0 0 0
@@ -543,8 +572,15 @@ let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
with Not_found | Session_itp.BadID -> limit,None,save_to
in
let panid = graft_proof_attempt ~limit ses id pr in
- Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,ores)
- scheduled_proof_attempts;
+ let spa =
+ { spa_contr = c;
+ spa_id = id;
+ spa_pr = pr;
+ spa_limit = adaptlimit;
+ spa_pr_scr = proof_script;
+ spa_callback = callback panid;
+ spa_ores = ores } in
+ Queue.add spa scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 1083cdb4cbbaa147b77fb06ecb73ce873f3d7efd..51a859245f5bbe5b8eea5d5e87d1293e2e56304d 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -353,7 +353,9 @@ let () =
let model_any : any Hint.t = Hint.create 17
- let any_from_node_ID (nid:node_ID) : any = Hint.find model_any nid
+ let any_from_node_ID (nid:node_ID) : any option =
+ try Some (Hint.find model_any nid) with
+ | Not_found -> None
let pan_to_node_ID : node_ID Hpan.t = Hpan.create 17
let pn_to_node_ID : node_ID Hpn.t = Hpn.create 17
@@ -519,7 +521,7 @@ module P = struct
(* true if nid is below f_node or does not exists (in which case the
notification is a remove). false if not below. *)
let is_below s nid f_nodes =
- let any = try Some (any_from_node_ID nid) with _ -> None in
+ let any = any_from_node_ID nid in
match any with
| None -> true
| Some any ->
@@ -852,6 +854,10 @@ end
let send_task nid show_full_context loc =
let d = get_server_data () in
let any = any_from_node_ID nid in
+ match any with
+ | None ->
+ P.notify (Message (Error "Please select a node id"))
+ | Some any ->
if Session_itp.is_detached d.cont.controller_session any then
match any with
| APn _id ->
@@ -1079,28 +1085,37 @@ end
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 ?save_to:None d.cont id prover
- ~limit ~callback ~notification:(notify_change_proved d.cont))
- unproven_goals
+ let any = any_from_node_ID nid in
+ match any with
+ | None -> P.notify (Message (Error "Please select a node id"))
+ | Some any ->
+ let unproven_goals = unproven_goals_below_id d.cont any in
+ List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id
+ prover ~limit ~callback ~notification:(notify_change_proved d.cont))
+ unproven_goals
let schedule_edition (nid: node_ID) (prover: Whyconf.prover) =
let d = get_server_data () in
let callback = callback_update_tree_proof d.cont in
- try
- let id =
- match any_from_node_ID nid with
- | APn id -> id
- | APa panid -> get_proof_attempt_parent d.cont.controller_session panid
- | _ -> raise Not_found
- in
- C.schedule_edition d.cont id prover
- ~callback ~notification:(notify_change_proved d.cont)
- with Not_found ->
- P.notify
- (Message
- (Error
- "for edition you must select a proof attempt node"))
+ let any = any_from_node_ID nid in
+ match any with
+ | None -> P.notify (Message (Error "Please select a node id"));
+ | Some any ->
+ try
+ let id =
+ match any with
+ | APn id -> id
+ | APa panid ->
+ get_proof_attempt_parent d.cont.controller_session panid
+ | _ -> raise Not_found
+ in
+ C.schedule_edition d.cont id prover
+ ~callback ~notification:(notify_change_proved d.cont)
+ with Not_found ->
+ P.notify
+ (Message
+ (Error
+ "for edition you must select a proof attempt node"))
(* ----------------- Schedule transformation -------------------- *)
@@ -1152,7 +1167,10 @@ end
List.iter (fun id -> apply_transform (APn id) t args) child_ids
in
let nid = any_from_node_ID node_id in
- apply_transform nid t args
+ match nid with
+ | None -> P.notify (Message (Error "Please select a node id"));
+ | Some nid ->
+ apply_transform nid t args
let removed x =
let nid = node_ID_from_any x in
@@ -1165,7 +1183,7 @@ end
try
let id =
match any_from_node_ID nid with
- | APa panid -> panid
+ | Some (APa panid) -> panid
| _ -> raise Not_found
in
let callback_pa = callback_update_tree_proof d.cont in
@@ -1187,7 +1205,11 @@ end
let run_strategy_on_task nid s =
let d = get_server_data () in
- let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
+ let any = any_from_node_ID nid in
+ match any with
+ | None -> P.notify (Message (Error "Please select a node id"));
+ | Some any ->
+ let unproven_goals = unproven_goals_below_id d.cont any in
try
let (n,_,_,st) = Hstr.find d.cont.controller_strategies s in
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
@@ -1214,13 +1236,16 @@ end
let remove_node nid =
let d = get_server_data () in
- let n = any_from_node_ID nid in
+ let any = any_from_node_ID nid in
+ match any with
+ | None -> P.notify (Message (Error "Please select a node id"))
+ | Some any ->
begin
try
remove_subtree
~notification:(notify_change_proved d.cont)
~removed
- d.cont n
+ d.cont any
with RemoveError -> (* TODO send an error instead of information *)
P.notify (Message (Information "Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"))
end
@@ -1293,8 +1318,12 @@ end
let notify_first_unproven_node d ni =
let s = d.cont.controller_session in
let any = any_from_node_ID ni in
+ match any with
+ | None -> P.notify (Message (Error "Please select a node id"))
+ | Some any ->
let unproven_any =
get_first_unproven_goal_around
+ ~always_send:false
~proved:(Session_itp.any_proved s)
~children:(get_undetached_children_no_pa s)
~get_parent:(get_any_parent s)
@@ -1351,15 +1380,21 @@ end
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
begin
- try
- C.copy_paste
- ~notification:(notify_change_proved d.cont)
- ~callback_pa:(callback_update_tree_proof d.cont)
- ~callback_tr:(callback_update_tree_transform)
- d.cont from_any to_any;
- session_needs_saving := true
- with C.BadCopyPaste ->
- P.notify (Message (Error "invalid copy"))
+ match from_any, to_any with
+ | None, _ | _, None ->
+ P.notify (Message (Error "Please select a node id"));
+ | Some from_any, Some to_any ->
+ begin
+ try
+ C.copy_paste
+ ~notification:(notify_change_proved d.cont)
+ ~callback_pa:(callback_update_tree_proof d.cont)
+ ~callback_tr:(callback_update_tree_transform)
+ d.cont from_any to_any;
+ session_needs_saving := true
+ with C.BadCopyPaste ->
+ P.notify (Message (Error "invalid copy"))
+ end
end
| Get_file_contents f ->
read_and_send f
@@ -1372,7 +1407,7 @@ end
| Interrupt_req ->
C.interrupt ()
| Command_req (nid, cmd) ->
- let snid = try Some(any_from_node_ID nid) with Not_found -> None in
+ let snid = any_from_node_ID nid in
begin
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) ->
@@ -1402,16 +1437,20 @@ end
mark_obsolete snid;
session_needs_saving := true
| Focus_req ->
- let d = get_server_data () in
- let s = d.cont.controller_session in
- let any = any_from_node_ID nid in
- let focus_on =
- match any with
- | APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
- | _ -> any
- in
- focused_node := Focus_on [focus_on];
- reset_and_send_the_whole_tree ()
+ let d = get_server_data () in
+ let s = d.cont.controller_session in
+ let any = any_from_node_ID nid in
+ begin match any with
+ | None -> P.notify (Message (Error "Please select a node id"))
+ | Some any ->
+ let focus_on =
+ match any with
+ | APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
+ | _ -> any
+ in
+ focused_node := Focus_on [focus_on];
+ reset_and_send_the_whole_tree ()
+ end
| Server_utils.Unfocus_req -> unfocus ()
| Help_message s -> P.notify (Message (Information s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml
index 149736a85d53c70a8668508d936d07c028507eb7..32a612188a4799d8280893ff6470c4e1b30054bf 100644
--- a/src/session/server_utils.ml
+++ b/src/session/server_utils.ml
@@ -497,7 +497,7 @@ let split_list l node =
split_list l []
let get_first_unproven_goal_around
- ~proved ~children ~get_parent ~is_goal ~is_pa node =
+ ~always_send ~proved ~children ~get_parent ~is_goal ~is_pa node =
let rec look_around node =
match get_parent node with
| None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
@@ -517,7 +517,7 @@ let get_first_unproven_goal_around
| [] ->
begin
match before_node with
- | [] -> None
+ | [] -> if always_send then Some node else None
| hd :: _tl -> Some hd
end
| hd :: _tl -> Some hd
diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli
index ba06b1a885b3e222bf0c5b42e1bca5513bbfbff0..a44e3dba4949dfaa15fc6ed8957f83df4621af17 100644
--- a/src/session/server_utils.mli
+++ b/src/session/server_utils.mli
@@ -83,10 +83,19 @@ val interp:
Controller_itp.controller ->
Session_itp.any option -> string -> command
-
+(* Find the first unproven goal around the node given.
+ @param always_send: if true then always returns something
+ @param proved : oracle for proved node
+ @param children : returns the list children of a node
+ @param get_parent : returns the parent of a node
+ @param is_goal : answer true iff a given node is a goal
+ @param is_pa : answer true iff a given node is a proof attempt
+ @param node : node_id
+*)
val get_first_unproven_goal_around:
- proved:('a -> bool) ->
- children:('a -> 'a list) ->
- get_parent:('a -> 'a option) ->
- is_goal:('a -> bool) ->
- is_pa:('a -> bool) -> 'a -> 'a option
+ always_send:bool ->
+ proved:('a -> bool) ->
+ children:('a -> 'a list) ->
+ get_parent:('a -> 'a option) ->
+ is_goal:('a -> bool) ->
+ is_pa:('a -> bool) -> 'a -> 'a option
diff --git a/src/transform/intro_vc_vars_counterexmp.ml b/src/transform/intro_vc_vars_counterexmp.ml
index 318cbeff0d43fea5f814a4ee114c64d2eb62e2d2..7b3e0005003114cbce39eadeb90989052327a70f 100644
--- a/src/transform/intro_vc_vars_counterexmp.ml
+++ b/src/transform/intro_vc_vars_counterexmp.ml
@@ -85,6 +85,14 @@ module Hprid = Exthtbl.Make (struct
let hash p = Exthtbl.hash p
end)
+let same_line_loc loc1 loc2 =
+ match loc1, loc2 with
+ | Some loc1, Some loc2 ->
+ let (f1, l1, _, _) = Loc.get loc1 in
+ let (f2, l2, _, _) = Loc.get loc2 in
+ f1 = f2 && l1 = l2
+ | _ -> false
+
(* Used to generate duplicate vc_constant and axioms for counterex generation.
This function is always called when the term is in negative position or
under a positive term that is not introducible. This means it never change the
@@ -107,7 +115,7 @@ let rec do_intro info vc_loc vc_map vc_var t =
if info.vc_inside then begin
match info.vc_loc with
| None -> []
- | Some loc ->
+ | Some loc when not (same_line_loc info.vc_loc ls.id_loc) ->
(* variable inside the term T that triggers VC. If the variable
should be in counterexample, introduce new constant in location
loc with all attributes necessary for collecting it for
@@ -131,15 +139,16 @@ let rec do_intro info vc_loc vc_map vc_var t =
because those integrates a unique hash that would make
identical preid different lsymbol *)
if (Hprid.mem vc_map id_new) then
- []
- else
- begin
- Hprid.add vc_map id_new true;
- intro_const_equal_to_term
- ~term:t ~id_new:id_new ~axiom_name
- end
+ []
+ else
+ begin
+ Hprid.add vc_map id_new true;
+ intro_const_equal_to_term
+ ~term:t ~id_new:id_new ~axiom_name
+ end
| exception Not_found -> []
end
+ | _ -> []
end
else [] in
match t.t_node with