diff --git a/src/language.ml b/src/language.ml index 20fa0ddc577530c8518230666af6575c6a6df2a0..ba7fb6e3242a69c6b0984ea7dd99571fb1f9c6d4 100644 --- a/src/language.ml +++ b/src/language.ml @@ -17,8 +17,10 @@ type nnshape = { filename : string; } -let loaded_nets = Term.Hls.create 10 -let lookup_loaded_nets = Term.Hls.find_opt loaded_nets +let loaded_nets = Why3.Term.Hls.create 10 +let loaded_svms = Why3.Term.Hls.create 10 +let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets +let lookup_loaded_svms = Why3.Term.Hls.find_opt loaded_svms let register_nn_as_tuple nb_inputs nb_outputs filename env = let net = Pmodule.read_module env [ "caisar" ] "NN" in @@ -57,7 +59,7 @@ let register_svm nb_inputs nb_outputs filename env = (Ident.id_fresh "svm_apply") [] (Ty.ty_func asarray_input_type asarray_input_type) in - Why3.Term.Hls.add loaded_nets ls_svm_apply + Why3.Term.Hls.add loaded_svms ls_svm_apply { filename; nb_inputs; nb_outputs; ty_data = asarray_input_type }; let th_uc = Pmodule.add_pdecl ~vc:false th_uc diff --git a/src/language.mli b/src/language.mli index 2a053a0161ece50b59ee7ffaefd5649809d5a8c1..55d5051d7ec8a4fcdf592c43b8e9f8999bc7c2e1 100644 --- a/src/language.mli +++ b/src/language.mli @@ -16,6 +16,9 @@ type nnshape = { val lookup_loaded_nets : Term.lsymbol -> nnshape option (** @return the filename of a nnet Why3 representation. *) +val lookup_loaded_svms : Why3.Term.lsymbol -> nnshape option +(** @return the ioshape of a svm Why3 representation. *) + val register_nnet_support : unit -> unit (** Register NNet parser. *) diff --git a/src/verification.ml b/src/verification.ml index c16475ab20839c8d382000f7bcf1e4342d26f634..03a22e2b1285720265cda63c4c450fca7b003a42 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -82,7 +82,7 @@ let handle_task_saver task env dataset_csv command = then let eps = Fmt.str "%a" Constant.print_def e in let svm_filename = - match Language.lookup_loaded_nets svm_app_sym with + match Language.lookup_loaded_svms svm_app_sym with | Some t -> t.filename | None -> failwith "Svm file not found in environment." in