[SAVer] Created a new table for SVM type and logical symbols.

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

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. *)
 

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