language.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(**************************************************************************)

open Why3

type nnshape = {
  nb_inputs : int;
  nb_outputs : int;
  ty_data : Ty.ty;
  filename : string;
}

type svmshape = { nb_inputs : int; nb_classes : int; filename : string }

val lookup_loaded_nets : Term.lsymbol -> nnshape option
(** @return the filename of a nnet Why3 representation. *)

val lookup_loaded_svms : Why3.Term.lsymbol -> svmshape option
(** @return the svmshape of a svm Why3 representation. *)

val register_nnet_support : unit -> unit
(** Register NNet parser. *)

val register_onnx_support : unit -> unit
(** Register ONNX parser. *)

val register_ovo_support : unit -> unit
(** Register OVO parser. *)