verification.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2022                                                    *)
(*    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 json_config = private {
    prover : Prover.t;
    model : string;
    property : property;
  }
  [@@deriving yojson, show]

  and property = private {
    dataset : string;
    normalization : Dataset.normalization option;
    kind : Dataset.property;
  }
  [@@deriving yojson, show]

  type t

  val of_json_config : json_config -> t
  val of_string : string -> (t, string) result
  val pretty : Format.formatter -> t -> unit
end

val verify :
  ?debug:bool ->
  ?format:string ->
  loadpath:string list ->
  ?memlimit:int ->
  ?timelimit:int ->
  Prover.t ->
  ?dataset_csv:string ->
  File.t ->
  unit
(** [verify debug format loadpath memlimit timeout prover dataset_csv file]
    launches a verification of the given [file] with the provided [prover] and
    [dataset_csv].

    @param debug when set, enables debug information.
    @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 timeout is the timeout (in seconds) granted to the verification.
    @param dataset_csv
      is the filepath of a dataset, in CSV format, possibly appearing in [file]. *)