From 4b510f29837765264a7222b6cd6c29da13027b0c Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 11 Jan 2023 16:54:43 +0100
Subject: [PATCH] [json] Rename result into prover_answer.
---
src/JSON.ml | 2 +-
src/JSON.mli | 2 +-
src/main.ml | 13 +++++++------
src/verification.ml | 6 +++---
src/verification.mli | 2 +-
5 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/JSON.ml b/src/JSON.ml
index 67ecce4..012332f 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 c7074c1..2c02254 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 248bdf4..d7d68f1 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 2743cc8..7c8747c 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 c2d17bf..1c93426 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;
}
--
GitLab