diff --git a/src/JSON.ml b/src/JSON.ml index 67ecce40f77e344e2131ac9930f169ce12698c80..012332f4f53181aa67bc64b7c0227660862deff9 100644 --- a/src/JSON.ml +++ b/src/JSON.ml @@ -42,7 +42,7 @@ and property = { type output = { id : string; - result : prover_answer; + prover_answer : prover_answer; percentage_valid : float; dataset_results : string; } diff --git a/src/JSON.mli b/src/JSON.mli index c7074c16ebdb5b9b1286a292a1cb2e5608ca6aad..2c02254f4a92a554c19c9818fe354a28c33ccd82 100644 --- a/src/JSON.mli +++ b/src/JSON.mli @@ -41,7 +41,7 @@ and property = private { type output = { id : string; - result : prover_answer; + prover_answer : prover_answer; percentage_valid : float; dataset_results : string; } diff --git a/src/main.ml b/src/main.ml index 248bdf4ab811b73daf2079d5639cf8d042c7c5e9..d7d68f1eb287bab16f3d595aec620700a6fafed4 100644 --- a/src/main.ml +++ b/src/main.ml @@ -125,13 +125,13 @@ let log_theory_answer = Logs.info (fun m -> m "@[Verification results for theory '%s'@]" theory_name); List.iter task_answers - ~f:(fun { Verification.id; result; additional_info } -> + ~f:(fun { Verification.id; prover_answer; additional_info } -> let additional_info = match additional_info with Generic s -> s | Dataset _ -> None in Logs.app (fun m -> m "@[Goal %a:@ %a%a@]" Pretty.print_pr id - Call_provers.print_prover_answer result + Call_provers.print_prover_answer prover_answer Fmt.(option ~none:nop (any " " ++ string)) additional_info))) @@ -149,7 +149,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern List.iter theory_answers ~f:log_theory_answer; theory_answers -let record_dataset_results id result dataset outfile = +let record_dataset_results id prover_answer dataset outfile = let percentage_valid = let nb_valid = List.count dataset ~f:(fun record -> @@ -170,7 +170,7 @@ let record_dataset_results id result dataset outfile = Csv.close_out csv_out_channel; dataset_results in - let output = { JSON.id; result; percentage_valid; dataset_results } in + let output = { JSON.id; prover_answer; percentage_valid; dataset_results } in let out_channel = Stdlib.open_out outfile in Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output); Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile); @@ -179,8 +179,9 @@ let record_dataset_results id result dataset outfile = let record_theory_answers id outfile = Why3.Wstdlib.Mstr.iter (fun theory_name task_answers -> match task_answers with - | [ { Verification.result; additional_info = Dataset dataset; _ } ] -> - record_dataset_results id result dataset outfile + | [ { Verification.prover_answer; additional_info = Dataset dataset; _ } ] + -> + record_dataset_results id prover_answer dataset outfile | _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" theory_name)) let verify_json ?memlimit ?timelimit ?outfile json = diff --git a/src/verification.ml b/src/verification.ml index 2743cc877d7cc9a6686f94e687a66b637749571c..7c8747c03b79a40de351c374532ba476fa8ad976 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -61,7 +61,7 @@ type theory_answer = answer list Wstdlib.Mstr.t and answer = { id : Decl.prsymbol; - result : Call_provers.prover_answer; + prover_answer : Call_provers.prover_answer; additional_info : additional_info; } @@ -223,7 +223,7 @@ let answer_generic limit config env prover config_prover driver task = (prover_answer, None) let call_prover ?dataset ~limit config env prover config_prover driver task = - let result, additional_info = + let prover_answer, additional_info = match prover with | Prover.Saver -> let prover_answer, additional_info = @@ -243,7 +243,7 @@ let call_prover ?dataset ~limit config env prover config_prover driver task = (prover_answer, Generic additional_info) in let id = Task.task_goal task in - { id; result; additional_info } + { id; prover_answer; additional_info } let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern file = diff --git a/src/verification.mli b/src/verification.mli index c2d17bf139957392eb6a8168add1bf059c57a33d..1c934265180d90f877d0c2f0ccbd0488cccf3441 100644 --- a/src/verification.mli +++ b/src/verification.mli @@ -34,7 +34,7 @@ type theory_answer = answer list Wstdlib.Mstr.t and answer = private { id : Decl.prsymbol; - result : Call_provers.prover_answer; + prover_answer : Call_provers.prover_answer; additional_info : additional_info; }