diff --git a/src/SAVer.ml b/src/SAVer.ml index cc1bfc6a4ccf222db3697a125239f2ad37f1615c..f5347ecdebf748bc620f16b69910d0b6ca46cabe 100644 --- a/src/SAVer.ml +++ b/src/SAVer.ml @@ -77,7 +77,7 @@ let re_group_number_of_predicate = function let negative_answer = function | Dataset.Correct -> - (* SAVer is complete wrt correct predicate. *) + (* SAVer is complete wrt [Correct] predicate. *) Call_provers.Invalid | Robust _ | CondRobust _ -> Call_provers.Unknown "" diff --git a/src/language.ml b/src/language.ml index 7d7abb4cdbef4f582390f7462b46418449c1c08e..88d81e50d98bdeeac4cb7c73a2a16dcde055753e 100644 --- a/src/language.ml +++ b/src/language.ml @@ -37,7 +37,7 @@ type nn_shape = { type svm_shape = { nb_inputs : int; - nb_classes : int; + nb_outputs : int; filename : string; } @@ -86,7 +86,7 @@ let register_nn_as_array env nb_inputs nb_outputs filename ?nier mstr = in Wstdlib.Mstr.add name (Pmodule.close_module th_uc) mstr -let register_svm_as_array env nb_inputs nb_classes filename mstr = +let register_svm_as_array env nb_inputs nb_outputs filename mstr = let name = "AsArray" in let th_uc = Pmodule.create_module env (Ident.id_fresh name) in let svm = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in @@ -95,7 +95,7 @@ let register_svm_as_array env nb_inputs nb_classes filename mstr = Ty.ty_app Theory.(ns_find_ts svm.mod_theory.th_export [ "model" ]) [] in let ls_model = Term.create_fsymbol (Ident.id_fresh "model") [] svm_type in - Term.Hls.add loaded_svms ls_model { filename; nb_inputs; nb_classes }; + Term.Hls.add loaded_svms ls_model { filename; nb_inputs; nb_outputs }; let th_uc = Pmodule.add_pdecl ~vc:false th_uc (Pdecl.create_pure_decl (Decl.create_param_decl ls_model)) diff --git a/src/language.mli b/src/language.mli index 68c71572b844dc0aff4a1578be3d999950cad000..eb025a8a9322cfe5d50dc6dbf8663a92956fac8a 100644 --- a/src/language.mli +++ b/src/language.mli @@ -32,7 +32,7 @@ type nn_shape = private { type svm_shape = private { nb_inputs : int; - nb_classes : int; + nb_outputs : int; filename : string; } @@ -60,5 +60,5 @@ val onnx_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t the given onnx [filename]. The result is memoized. *) val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t -(* [nnet_parser env filename] parses and creates the theories corresponding to +(* [ovo_parser env filename] parses and creates the theories corresponding to the given ovo [filename]. The result is memoized. *)