diff --git a/src/verification.ml b/src/verification.ml
index 03a22e2b1285720265cda63c4c450fca7b003a42..3a7bacdb55f8da024dd714031e792a7b429e3257 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -55,128 +55,135 @@ let combine_prover_answers answers =
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
-let handle_task_saver task env dataset_csv command =
+let answer_saver limit config task env prover dataset_csv =
let open Why3 in
- let dataset_filename =
- match dataset_csv with
- | Some s -> s
- | None -> failwith "Error, no dataset provided for SAVer."
+ let handle_task_saver task env dataset_csv command =
+ let dataset_filename =
+ match dataset_csv with
+ | Some s -> s
+ | None -> failwith "Error, no dataset provided for SAVer."
+ in
+ let goal = Task.task_goal_fmla task in
+ let eps, svm_filename =
+ match goal.t_node with
+ | Tquant (Tforall, b) -> (
+ let _, _, pred = Term.t_open_quant b in
+ let svm_t = Pmodule.read_module env [ "caisar" ] "SVM" in
+ let robust_to_predicate =
+ let open Theory in
+ ns_find_ls svm_t.mod_theory.th_export [ "robust_to" ]
+ in
+ match pred.t_node with
+ | Term.Tapp
+ ( ls,
+ [
+ { t_node = Tapp (svm_app_sym, _); _ };
+ _;
+ { t_node = Tconst e; _ };
+ ] ) ->
+ if Term.ls_equal ls robust_to_predicate
+ then
+ let eps = Fmt.str "%a" Constant.print_def e in
+ let svm_filename =
+ match Language.lookup_loaded_svms svm_app_sym with
+ | Some t -> t.filename
+ | None -> failwith "Svm file not found in environment."
+ in
+ (eps, svm_filename)
+ else failwith "Wrong predicate found."
+ (* no other predicate than robust_to is supported *)
+ | _ -> failwith "Unsupported by SAVer.")
+ | _ -> failwith "Unsupported by SAVer."
+ in
+ let svm_file = Filename.concat (Caml.Sys.getcwd ()) svm_filename in
+ let dataset_file = Filename.concat (Caml.Sys.getcwd ()) dataset_filename in
+ let command = Re__Core.replace_string svm ~by:svm_file command in
+ let command = Re__Core.replace_string dataset ~by:dataset_file command in
+ let command = Re__Core.replace_string epsilon ~by:eps command in
+ command
+ in
+ let command = Whyconf.get_complete_command ~with_steps:false prover in
+ let command = handle_task_saver task env dataset_csv command in
+ let res_parser =
+ {
+ Call_provers.prp_regexps =
+ [ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
+ prp_timeregexps = [];
+ prp_stepregexps = [];
+ prp_exitcodes = [];
+ prp_model_parser = Model_parser.lookup_model_parser "no_model";
+ }
+ in
+ let prover_call =
+ Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
+ ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
+ ~filename:"foo.txt" ~get_counterexmp:false ~gen_new_file:false
+ ~printing_info:Printer.default_printing_info (Buffer.create 10)
in
- let goal = Task.task_goal_fmla task in
- let eps, svm_filename =
- match goal.t_node with
- | Tquant (Tforall, b) -> (
- let _, _, pred = Term.t_open_quant b in
- let svm_t = Pmodule.read_module env [ "caisar" ] "SVM" in
- let robust_to_predicate =
- let open Theory in
- ns_find_ls svm_t.mod_theory.th_export [ "robust_to" ]
+ let prover_result = Call_provers.wait_on_call prover_call in
+ let answer =
+ match prover_result.pr_answer with
+ | Call_provers.HighFailure -> (
+ let pr_output = prover_result.pr_output in
+ let matcher =
+ Re__Pcre.regexp
+ "\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
in
- match pred.t_node with
- | Term.Tapp
- ( ls,
- [
- { t_node = Tapp (svm_app_sym, _); _ }; _; { t_node = Tconst e; _ };
- ] ) ->
- if Term.ls_equal ls robust_to_predicate
- then
- let eps = Fmt.str "%a" Constant.print_def e in
- let svm_filename =
- match Language.lookup_loaded_svms svm_app_sym with
- | Some t -> t.filename
- | None -> failwith "Svm file not found in environment."
- in
- (eps, svm_filename)
- else failwith "Wrong predicate found."
- (* no other predicate than robust_to is supported *)
- | _ -> failwith "Unsupported by SAVer.")
- | _ -> failwith "Unsupported by SAVer."
+ match Re__Core.exec_opt matcher pr_output with
+ | Some g ->
+ if Int.of_string (Re__Core.Group.get g 1)
+ = Int.of_string (Re__Core.Group.get g 2)
+ then Call_provers.Valid
+ else Call_provers.Invalid
+ | None -> Call_provers.HighFailure
+ (* Any other answer than HighFailure should
+ * never happen as we do not define
+ * anything in SAVer's driver *))
+ | _ -> assert false
in
- let svm_file = Filename.concat (Caml.Sys.getcwd ()) svm_filename in
- let dataset_file = Filename.concat (Caml.Sys.getcwd ()) dataset_filename in
- let command = Re__Core.replace_string svm ~by:svm_file command in
- let command = Re__Core.replace_string dataset ~by:dataset_file command in
- let command = Re__Core.replace_string epsilon ~by:eps command in
- command
+ answer
-let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
- dataset_csv task =
+let answer_generic limit config task driver
+ (prover : Why3.Whyconf.config_prover) =
let open Why3 in
- if String.equal prover.prover.prover_name "SAVer"
- then
- let command = Whyconf.get_complete_command ~with_steps:false prover in
- let command = handle_task_saver task env dataset_csv command in
- let res_parser =
- {
- Call_provers.prp_regexps =
- [ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
- prp_timeregexps = [];
- prp_stepregexps = [];
- prp_exitcodes = [];
- prp_model_parser = Model_parser.lookup_model_parser "no_model";
- }
- in
-
+ let task_prepared = Driver.prepare_task driver task in
+ let tasks =
+ (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
+ if String.equal prover.prover.prover_name "Marabou"
+ then Trans.apply Split_goal.split_goal_full task_prepared
+ else [ task_prepared ]
+ in
+ let command = Whyconf.get_complete_command ~with_steps:false prover in
+ let nn_file =
+ match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
+ | Some [ MAstr nn_file ] -> nn_file
+ | Some _ -> assert false (* By construction of the meta. *)
+ | None -> invalid_arg (Fmt.str "No neural network model found in task")
+ in
+ let nn_file = Unix.realpath nn_file in
+ let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
+ let call_prover_on_task task_prepared =
let prover_call =
- Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
- ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
- ~filename:"foo.txt" ~get_counterexmp:false ~gen_new_file:false
- ~printing_info:Printer.default_printing_info (Buffer.create 10)
+ Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
+ ~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
in
let prover_result = Call_provers.wait_on_call prover_call in
- let answer =
- match prover_result.pr_answer with
- | Call_provers.HighFailure -> (
- let pr_output = prover_result.pr_output in
- let matcher =
- Re__Pcre.regexp
- "\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
- in
- match Re__Core.exec_opt matcher pr_output with
- | Some g ->
- if Int.of_string (Re__Core.Group.get g 1)
- = Int.of_string (Re__Core.Group.get g 2)
- then Call_provers.Valid
- else Call_provers.Invalid
- | None -> Call_provers.HighFailure
- (* Any other answer than HighFailure should
- * never happen as we do not define
- * anything in SAVer's driver *))
- | _ -> assert false
- in
- Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
- Call_provers.print_prover_answer answer
- else
- let task_prepared = Driver.prepare_task driver task in
- let tasks =
- (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
- if String.equal prover.prover.prover_name "Marabou"
- then Trans.apply Split_goal.split_goal_full task_prepared
- else [ task_prepared ]
- in
- let command = Whyconf.get_complete_command ~with_steps:false prover in
- let nn_file =
- match
- Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared
- with
- | Some [ MAstr nn_file ] -> nn_file
- | Some _ -> assert false (* By construction of the meta. *)
- | None -> invalid_arg (Fmt.str "No neural network model found in task")
- in
- let nn_file = Unix.realpath nn_file in
- let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
- let call_prover_on_task task_prepared =
- let prover_call =
- Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
- ~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
- in
- let prover_result = Call_provers.wait_on_call prover_call in
- prover_result.pr_answer
- in
- let answers = List.map tasks ~f:call_prover_on_task in
- let answer = combine_prover_answers answers in
- Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
- Call_provers.print_prover_answer answer
+ prover_result.pr_answer
+ in
+ let answers = List.map tasks ~f:call_prover_on_task in
+ let answer = combine_prover_answers answers in
+ answer
+
+let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
+ dataset_csv task =
+ let open Why3 in
+ let prover_answer =
+ if String.equal prover.prover.prover_name "SAVer"
+ then answer_saver limit config task env prover dataset_csv
+ else answer_generic limit config task driver prover
+ in
+ Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
+ Call_provers.print_prover_answer prover_answer
let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
~dataset_csv file =