Option --get-ce for why3ide.

src/driver/driver.ml

@@ -332,7 +332,16 @@ let prove_task_prepared
   Buffer.reset buf;
   res
 
-let prove_task ~command ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
+let add_cntexample_meta task cntexample =
+  if not (cntexample) then task
+  else
+    let cnt_meta = lookup_meta "get_counterexmp" in
+    let g,task = Task.task_separate_goal task in
+    let task = Task.add_meta task cnt_meta [] in
+    Task.add_tdecl task g
+
+let prove_task ~command ?(cntexample=false) ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
+  let task = add_cntexample_meta task cntexample in
   let task = prepare_task drv task in
   prove_task_prepared ~command ?timelimit ?memlimit
                       ?steplimit ?old ?inplace drv task

src/driver/driver.mli

@@ -56,6 +56,7 @@ val print_theory :
 
 val prove_task :
   command    : string ->
+  ?cntexample : bool ->
   ?timelimit : int ->
   ?memlimit  : int ->
   ?steplimit : int ->

src/ide/gmain.ml

@@ -999,10 +999,9 @@ let prover_on_selected_goals pr =
       try
        let a = get_any_from_row_reference row in
        M.run_prover
-	 MA.keygen
          (env_session()) sched
          ~context_unproved_goals_only:!context_unproved_goals_only
-         ~timelimit ~memlimit
+         ~cntexample:!opt_cntexmp ~timelimit ~memlimit
          pr a
       with e ->
         eprintf "@[Exception raised while running a prover:@ %a@.@]"
@@ -1108,13 +1107,14 @@ let bisect_proof_attempt pa =
         let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
           ~goal ~env_session:eS pa in
         MA.init_any (S.Metas metas);
-        M.run_external_proof eS sched npa
+        M.run_external_proof eS sched ~cntexample:!opt_cntexmp npa
         with e ->
           dprintf debug "Bisecting error:@\n%a@."
             Exn_printer.exn_printer e end
       | Eliminate_definition.BSstep (t,c) ->
         assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
         M.schedule_proof_attempt
+	  ~cntexample:!opt_cntexmp
           ~timelimit:!timelimit
           ~memlimit:pa.S.proof_memlimit
 	  ~steplimit:(-1)
@@ -1153,6 +1153,7 @@ let bisect_proof_attempt pa =
             dprintf debug "Prover can't be loaded.@."
           | Some lp ->
             M.schedule_proof_attempt
+	      ~cntexample:!opt_cntexmp
               ~timelimit:!timelimit
               ~memlimit:pa.S.proof_memlimit
 	      ~steplimit:(-1)
@@ -1163,7 +1164,7 @@ let bisect_proof_attempt pa =
               ~callback:(callback lp pa c) sched t in
   dprintf debug "Bisecting with %a started.@."
     C.print_prover pa.S.proof_prover;
-  M.run_external_proof eS sched ~callback:first_callback pa
+  M.run_external_proof eS sched ~cntexample:!opt_cntexmp ~callback:first_callback pa
 
 let apply_bisect_on_selection () =
   List.iter

src/session/session.ml

@@ -1837,18 +1837,6 @@ let pos_of_metas lms =
   List.fold_left (fun idpos (_,args) ->
     List.fold_left look_for_ident idpos args) empty_idpos lms
 
-let add_meta_to_task g meta meta_args =
-  (*let task = goal_task goal in
-  let task = Task.add_meta task meta meta_args in
-  goal.goal_task <- Some task 
-  *)
-  let goal,task = Task.task_separate_goal (goal_task g) in
-  let task = Task.add_meta task meta meta_args in
-  g.goal_task <- Some task
-
-
-    
-
 let add_registered_metas ~keygen env added0 g =
   let added = List.fold_left (fun ma (s,l) ->
     Mstr.change (function

src/session/session.mli

@@ -443,8 +443,6 @@ val remove_transformation : ?notify:'key notify -> 'key transf -> unit
   (** Remove a transformation *)
 
 (** {2 Metas} *)
-val add_meta_to_task : 'key goal -> Theory.meta -> Theory.meta_arg list -> unit
-
 val add_registered_metas :
   keygen:'key keygen ->
   'key env_session ->

src/session/session_scheduler.ml

@@ -79,7 +79,7 @@ module Make(O : OBSERVER) = struct
 (*************************)
 
 type action =
-  | Action_proof_attempt of int * int * int * string option * bool * string *
+  | Action_proof_attempt of bool * int * int * int * string option * bool * string *
       Driver.driver * (proof_attempt_status -> unit) * Task.task
   | Action_delayed of (unit -> unit)
 
@@ -209,12 +209,12 @@ let idle_handler t =
     if Queue.length t.proof_attempts_queue < 3 * t.maximum_running_proofs then
       begin
       match Queue.pop t.actions_queue with
-        | Action_proof_attempt(timelimit,memlimit,steplimit,
+        | Action_proof_attempt(cntexample,timelimit,memlimit,steplimit,
               old,inplace,command,driver,callback,goal) ->
             begin
               try
                 let pre_call =
-                  Driver.prove_task ?old ~inplace ~command
+                  Driver.prove_task ?old ~cntexample ~inplace ~command
                     ~timelimit ~steplimit ~memlimit driver goal
                 in
                 Queue.push (callback,pre_call) t.proof_attempts_queue;
@@ -257,7 +257,7 @@ let cancel_scheduled_proofs t =
   try
     while true do
       match Queue.pop t.actions_queue with
-        | Action_proof_attempt(_timelimit,_memlimit,_steplimit,
+        | Action_proof_attempt(_cntexample,_timelimit,_memlimit,_steplimit,
               _old,_inplace,_command,_driver,callback,_goal) ->
             callback Interrupted
         | Action_delayed _ as a->
@@ -275,14 +275,14 @@ let cancel_scheduled_proofs t =
           O.notify_timer_state 0 0 (List.length t.running_proofs)
 
 
-let schedule_proof_attempt ~timelimit ~memlimit ~steplimit ?old ~inplace
+let schedule_proof_attempt ~cntexample ~timelimit ~memlimit ~steplimit ?old ~inplace
     ~command ~driver ~callback t goal =
   Debug.dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@."
     (fun fmt g -> Format.pp_print_string fmt
       (Task.task_goal g).Decl.pr_name.Ident.id_string) goal;
   callback Scheduled;
   Queue.push
-    (Action_proof_attempt(timelimit,memlimit,steplimit,
+    (Action_proof_attempt(cntexample,timelimit,memlimit,steplimit,
       old,inplace,command,driver,callback,goal))
     t.actions_queue;
   run_idle_handler t
@@ -451,7 +451,7 @@ let dummy_limits = (0,0,0)
 
 (** run_external_proof_v3 doesn't modify existing proof attempt, it can just
     create new one by find_prover *)
-let run_external_proof_v3 eS eT a callback =
+let run_external_proof_v3 eS eT a ?(cntexample=false) callback =
   match find_prover eS a with
   | None ->
     callback a a.proof_prover dummy_limits None Starting;
@@ -489,7 +489,7 @@ let run_external_proof_v3 eS eT a callback =
             if Sys.file_exists f then Some f
             else raise (NoFile f) in
         schedule_proof_attempt
-          ~timelimit ~memlimit ~steplimit
+          ~cntexample ~timelimit ~memlimit ~steplimit
           ?old ~inplace ~command
           ~driver:npc.prover_driver
           ~callback:cb
@@ -500,7 +500,7 @@ let run_external_proof_v3 eS eT a callback =
     end
 
 (** run_external_proof_v2 modify the session according to the current state *)
-let run_external_proof_v2 eS eT a callback =
+let run_external_proof_v2 eS eT a ~cntexample callback =
   let previous_res = ref (a.proof_state,a.proof_obsolete) in
   let callback a ap limits previous state =
     begin match state with
@@ -522,19 +522,19 @@ let run_external_proof_v2 eS eT a callback =
     end;
     callback a ap limits previous state
   in
-  run_external_proof_v3 eS eT a callback
+  run_external_proof_v3 eS eT a ~cntexample callback
 
 let running = function
   | Scheduled | Running -> true
   | Unedited | JustEdited | Interrupted
   | Done _ | InternalFailure _ -> false
 
-let run_external_proof_v2 eS eT a callback =
+let run_external_proof_v2 eS eT a ?(cntexample=false) callback =
   (* Perhaps the test a.proof_archived should be done somewhere else *)
   if a.proof_archived || running a.proof_state then () else
-  run_external_proof_v2  eS eT a callback
+  run_external_proof_v2 eS eT a ~cntexample callback
 
-let run_external_proof eS eT ?callback a =
+let run_external_proof eS eT ?(cntexample=false) ?callback a =
   let callback =
     match callback with
     | None -> fun _ _ _ _ _ -> ()
@@ -545,9 +545,9 @@ let run_external_proof eS eT ?callback a =
       | MissingFile _ -> c a a.proof_state
       | StatusChange s -> c a s
   in
-  run_external_proof_v2 eS eT a callback
+  run_external_proof_v2 eS eT a ~cntexample callback
 
-let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
+let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g =
   let a =
     try
       let a = PHprover.find g.goal_external_proofs p in
@@ -561,49 +561,42 @@ let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
       O.init ep.proof_key (Proof_attempt ep);
       ep
   in
-  run_external_proof eS eT ?callback a
+  run_external_proof eS eT ~cntexample ?callback a
 
 let prover_on_goal_or_children eS eT
-    ~context_unproved_goals_only ~timelimit ~memlimit p g =
+    ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit p g =
   goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
-    (prover_on_goal eS eT ~timelimit ~memlimit p) g
+    (prover_on_goal eS eT ~cntexample ~timelimit ~memlimit p) g
 
-let run_prover keygen eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
+let run_prover eS eT ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a =
   match a with
   | Goal g ->
-    (*let cntexmp_meta = [("get_counterexmp", [])] in
-    ignore (add_registered_metas ~keygen eS cntexmp_meta g);*)
-    (*
-    let meta = Theory.lookup_meta "get_counterexmp" in
-    let () = Session.add_meta_to_task g meta [] in
-    *)
-
     prover_on_goal_or_children eS eT
-      ~context_unproved_goals_only ~timelimit ~memlimit pr g
+      ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr g
   | Theory th ->
         List.iter
           (prover_on_goal_or_children eS eT
-             ~context_unproved_goals_only ~timelimit ~memlimit pr)
+             ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
           th.theory_goals
     | File file ->
         List.iter
           (fun th ->
              List.iter
                (prover_on_goal_or_children eS eT
-                  ~context_unproved_goals_only ~timelimit ~memlimit pr)
+                  ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
                th.theory_goals)
           file.file_theories
     | Proof_attempt a ->
         prover_on_goal_or_children eS eT
-          ~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent
+          ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a.proof_parent
     | Transf tr ->
         List.iter
           (prover_on_goal_or_children eS eT
-             ~context_unproved_goals_only ~timelimit ~memlimit pr)
+             ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
           tr.transf_goals
     | Metas m ->
       prover_on_goal_or_children eS eT
-        ~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
+        ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr m.metas_goal
 
 
 

src/session/session_scheduler.mli

@@ -130,9 +130,9 @@ module Make(O: OBSERVER) : sig
 (** {2 Actions} *)
 
   val run_prover :
-    O.key keygen ->
     O.key env_session -> t ->
     context_unproved_goals_only:bool ->
+    cntexample : bool ->
     timelimit:int -> memlimit:int ->
     Whyconf.prover -> O.key any -> unit
     (** [run_prover es sched p a] runs prover [p] on all goals under [a]
@@ -148,10 +148,15 @@ module Make(O: OBSERVER) : sig
 
   val run_external_proof :
     O.key env_session -> t ->
+    ?cntexample : bool ->
     ?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
     O.key proof_attempt -> unit
-  (** [run_external_proof es sched ?callback p] reruns an existing
-      proof attempt [p] *)
+  (** [run_external_proof es sched ?cntexample ?callback p] reruns an existing
+      proof attempt [p] 
+
+      ~cntexample indicates if prover should be asked to get counter-example
+	model
+  *)
 
 
   type run_external_status =
@@ -162,24 +167,33 @@ module Make(O: OBSERVER) : sig
 
   val run_external_proof_v3 :
     O.key Session.env_session -> t -> O.key Session.proof_attempt ->
+    ?cntexample : bool ->
     (O.key Session.proof_attempt -> Whyconf.prover ->
      int * int * int -> Call_provers.prover_result option -> run_external_status -> unit) ->
      unit
-  (** [run_external_proof_v3 env_session sched pa callback] the
+  (** [run_external_proof_v3 env_session sched pa ?cntexample callback] the
       callback is applied with [callback pa p limits old_result
       status]. run_external_proof_v3 don't change the existing proof
       attempt just can add new by O.uninstalled_prover. Be aware since
       the session is not modified there is no test to see if the
-      proof_attempt had already been started *)
+      proof_attempt had already been started 
+      
+      ?cntexample indicates if prover should be asked to get counter-example
+	model
+  *)
 
 
   val prover_on_goal :
     O.key env_session -> t ->
     ?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
+    ?cntexample : bool ->
     timelimit:int -> memlimit:int ->
     Whyconf.prover -> O.key goal -> unit
-  (** [prover_on_goal es sched ?timelimit p g] same as
+  (** [prover_on_goal es sched ?cntexample ?timelimit p g] same as
       {!redo_external_proof} but creates or reuses existing proof_attempt
+      
+      ?cntexample indicates if prover should be asked to get counter-example
+	model
   *)
 
 
@@ -288,6 +302,7 @@ module Make(O: OBSERVER) : sig
     *)
 
   val schedule_proof_attempt:
+    cntexample:bool ->
     timelimit:int ->
     memlimit:int ->
     steplimit:int ->

src/tools/why3prove.ml

@@ -209,9 +209,7 @@ let () = try
     in
     Task.add_meta task meta args
   in
-  let metas = if !opt_cntexmp then (("get_counterexmp", None)::!opt_metas)
-    else !opt_metas in
-  opt_task := List.fold_left add_meta !opt_task metas
+  opt_task := List.fold_left add_meta !opt_task !opt_metas
 
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;
@@ -280,7 +278,7 @@ let output_theory drv fname _tname th task dir =
 let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
   match !opt_output, !opt_command with
     | None, Some command ->
-        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
+        let call = Driver.prove_task ~command ~cntexample:!opt_cntexmp ~timelimit ~memlimit drv task in
         let res = Call_provers.wait_on_call (call ()) () in
         printf "%s %s %s : %a@." fname tname
           (task_goal task).Decl.pr_name.Ident.id_string

src/why3session/why3session_run.ml

@@ -306,7 +306,8 @@ let run_one sched env config filters interactive_provers fname =
         if b then
           let callback_edit pa =
             M.run_external_proof_v3
-              env_session sched pa callback in
+              env_session sched pa 
+	      callback in
           M.edit_proof_v3 env_session sched
             ~default_editor:"" (** TODO? *)
             ~callback:callback_edit a