[verification] Factor out code for building the prover command.

src/verification.ml

@@ -149,10 +149,19 @@ let answer_aimos limit config env config_prover dataset task =
   let additional_info = Generic None in
   (answer, additional_info)
 
-let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
-let config_re = Re__Core.(compile (str "%{config}"))
+let re_nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let re_config = Re__Core.(compile (str "%{config}"))
 let config_site = List.hd_exn Dirs.Sites.config
 
+let build_command config_prover ~nn_filename =
+  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
+  let command =
+    Re__Core.replace_string re_nnet_or_onnx
+      ~by:(Unix.realpath nn_filename)
+      command
+  in
+  Re__Core.replace_string re_config ~by:config_site command
+
 let call_prover_on_task limit config command driver task =
   let prover_call =
     Driver.prove_task_prepared ~command ~config ~limit driver task
@@ -193,10 +202,8 @@ let answer_dataset limit config env prover config_prover driver dataset task =
     Dataset.tasks_of_nn_csv_predicate env dataset_predicate
     |> List.map ~f:(Driver.prepare_task driver)
   in
-  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
   let command =
-    let nn_file = Unix.realpath dataset_predicate.model.filename in
-    Re__Core.replace_string nnet_or_onnx ~by:nn_file command
+    build_command config_prover ~nn_filename:dataset_predicate.model.filename
   in
   let dataset_answers =
     match prover with
@@ -231,9 +238,9 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
   let answers =
     List.concat_map tasks ~f:(fun task ->
       let task = Driver.prepare_task driver task in
-      let nn_file =
+      let nn_filename =
         match Task.on_meta_excl Utils.meta_nn_filename task with
-        | Some [ MAstr nn_file ] -> Unix.realpath nn_file
+        | Some [ MAstr nn_filename ] -> nn_filename
         | Some _ -> assert false (* By construction of the meta. *)
         | None -> invalid_arg "No neural network model found in task"
       in
@@ -245,11 +252,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         | Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
         | _ -> [ task ]
       in
-      let command =
-        Whyconf.get_complete_command ~with_steps:false config_prover
-      in
-      let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
-      let command = Re__Core.replace_string config_re ~by:config_site command in
+      let command = build_command config_prover ~nn_filename in
       List.map tasks ~f:(call_prover_on_task limit config command driver))
   in
   let prover_answer = combine_prover_answers answers in