Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
(**************************************************************************)
(* *)
(* This file is part of CAISAR. *)
(* *)
(* Copyright (C) 2024 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* You can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Why3
open Base
module File = struct
type t =
| Stdin
| File of string
[@@deriving of_yojson, show]
let of_string s =
if String.equal s "-"
then Ok Stdin
else if Stdlib.Sys.file_exists s
then Ok (File s)
else Error (Fmt.str "No '%s' file or directory" s)
let pretty fmt = function
| Stdin -> Fmt.string fmt "-"
| File f -> Fmt.string fmt f
end
module Problem = struct
type t =
| GenericProblem of {
filepath : File.t;
definitions : (string * string) list option;
goals : (string * string list) list option;
theories : string list;
}
[@@deriving of_yojson { strict = false }, show]
let of_file ~definitions ~goals ~theories file =
(* TODO: analyze the property inside of the filepath in order to extract the
proper dataset predicate? *)
GenericProblem { filepath = file; definitions; goals; theories }
end
module Query = struct
let id_int = ref 0
type t = {
id : string;
prover : Prover.t;
prover_altern : string option;
problem : Problem.t;
loadpath : string list;
time_limit : int option;
memory_limit : int option;
onnx_out_dir : string option;
output_file : string option;
dataset : string option;
}
[@@deriving of_yojson { strict = false }, show]
let make ~id prover ~prover_altern problem ~loadpath ~time_limit ~memory_limit
~onnx_out_dir ~dataset ~output_file =
let id =
Int.incr id_int;
id ^ Int.to_string !id_int
in
{
id;
prover;
prover_altern;
loadpath;
time_limit;
problem;
memory_limit;
onnx_out_dir;
output_file;
dataset;
}
let of_json s =
match of_yojson (Yojson.Safe.from_file s) with
| Ok t -> t
| Error msg ->
invalid_arg
(Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg)
| exception Yojson.Json_error msg ->
failwith
(Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg)
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
let pretty fmt = Fmt.fmt "%a" fmt pp
end
module Answer = struct
let prsymbol_to_yojson pr = `String (Fmt.str "%a" Pretty.print_pr pr)
let pp_prsymbol fmt pr = Fmt.pf fmt "%a" Pretty.print_pr pr
let id = ref 0
type t = {
id : int;
problem_answer : problem_answer;
}
[@@deriving to_yojson, show]
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving to_yojson, show]
and problem_answer =
| LegacyDatasetAnswer of {
id : Why3.Decl.prsymbol;
[@to_yojson prsymbol_to_yojson] [@printer pp_prsymbol]
prover_answer : prover_answer;
percentage_valid : float option;
dataset_results : prover_answer list;
additional_info : string option;
}
| GenericProblemAnswer of {
id : Why3.Decl.prsymbol;
[@to_yojson prsymbol_to_yojson] [@printer pp_prsymbol]
prover_answer : prover_answer;
additional_info : string option;
}
[@@deriving to_yojson, show]
let make p =
Int.incr id;
{ id = !id; problem_answer = p }
let pretty fmt = Fmt.fmt "%a" fmt pp
end