verification.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2023                                                    *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

module File : sig
  type t = private
    | Stdin
    | File of string
    | JSON of Json.input

  val of_json_input : Json.input -> (t, string) result
  val of_string : string -> (t, string) result
  val pretty : Format.formatter -> t -> unit
end

type verification_result = answer list Why3.Wstdlib.Mstr.t

and answer = private {
  id : Why3.Decl.prsymbol;
  prover_answer : Why3.Call_provers.prover_answer;
  additional_info : additional_info;
}

and additional_info = private
  | Generic of string option
  | Dataset of Why3.Call_provers.prover_answer list
      (** A prover answer per data point. *)

val verify :
  ?format:string ->
  loadpath:string list ->
  ?memlimit:int ->
  ?timelimit:int ->
  ?dataset:string ->
  Prover.t ->
  ?prover_altern:string ->
  ?def_constants:(string * string) list ->
  ?theories:string list ->
  ?goals:(string * string list) list ->
  ?onnx_out_dir:string ->
  File.t ->
  verification_result
(** Starts a verification of the given [file] with the provided [prover].

    @param format is the [file] format.
    @param loadpath is the additional loadpath.
    @param memlimit
      is the memory limit (in megabytes) granted to the verification.
    @param timelimit is the timeout (in seconds) granted to the verification.
    @param dataset
      is the filepath of a dataset (eg, in CSV format) possibly appearing in
      [file].
    @param prover_altern is the alternative [prover] configuration.
    @param def_constants is a key:value list defining toplevel constants.
    @param theories
      identifies the theories whose goals are the only ones to verify.
    @param goals
      is a theory:goals list each identifying only the goals of a theory to
      verify.
    @param onnx_out_dir
      is the directory in which to write the ONNX files generated from the NIER.
    @return
      for each theory, an [answer] for each goal of the theory, respecting the
      order of appearance. *)

val create_env : string list -> Why3.Env.env * Why3.Whyconf.config