encoding_arrays : correct it

encoding_sort   : identity on meta lsymbol without definition
                  undefined symbol are defined before using them...

courses  WP_registerStudent : 0.53 s -> 0.03!!

drivers/z3.drv

@@ -133,8 +133,11 @@ theory int.EuclideanDivision
 end
 
 theory transform.array.Array
-   syntax logic get "(select %1 %2)"
-   syntax logic get "(store %1 %2)"
+  syntax logic get "(select %1 %2)"
+  syntax logic set "(store %1 %2)"
+  remove prop Select_eq
+  remove prop Select_neq
+
 end
 
 (*

src/printer/smt.ml

@@ -65,15 +65,16 @@ type info = {
 
 let rec print_type info fmt ty = match ty.ty_node with
   | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
-  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
-      | Some s -> syntax_arguments s (print_type info) fmt tl
-      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
-    end
+  | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with
+      | Some s -> syntax_arguments s (print_type info) fmt []
+      | None -> fprintf fmt "%a" print_ident ts.ts_name
+  end
+  | Tyapp (_, _) -> unsupported "smt : you must encode the complexe type"
 
-and print_tyapp info fmt = function
-  | [] -> ()
-  | [ty] -> fprintf fmt "%a " (print_type info) ty
-  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
+(* and print_tyapp info fmt = function *)
+(*   | [] -> () *)
+(*   | [ty] -> fprintf fmt "%a " (print_type info) ty *)
+(*   | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *)
 
 let print_type info fmt = catch_unsupportedType (print_type info fmt)
 
@@ -223,15 +224,15 @@ let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 let barrays task =
   let fold barrays =
     function
-      | [MAts tst;MAts tsk;MAts tse] ->
-        let extract_ty ts =
-          if ts.ts_args <> [] then
-            unsupported "smtv1 : type with argument are not supported";
-          match ts.ts_def with
-            | Some ty -> ty
-            | None -> ty_app ts [] in
-        Mts.add tst (extract_ty tsk,extract_ty tse) barrays
-      | _ -> barrays in
+      | [MAts tst;MAty tyk;MAty tye] ->
+        (* let extract_ty ts = *)
+        (*   if ts.ts_args <> [] then *)
+        (*     unsupported "smtv1 : type with argument are not supported"; *)
+        (*   match ts.ts_def with *)
+        (*     | Some ty -> ty *)
+        (*     | None -> ty_app ts [] in *)
+        Mts.add tst (tyk,tye) barrays
+      | _ -> assert false in
   Task.on_meta Encoding_arrays.meta_mono_array fold Mts.empty task
 
 let print_task pr thpr fmt task =

src/transform/encoding_arrays.ml

@@ -219,12 +219,19 @@ let gen_tvar su =
     Ssubst.fold fold su su in
   Ssubst.fold aux su (Ssubst.singleton (Mtv.empty))
 
+(* find all the possible instantiation which can give a type of env.keep *)
 let ty_quant env =
   let rec add_vs s ty =
     let s = ty_fold add_vs s ty in
     match ty.ty_node with
       | Tyapp(app,_) when ts_equal app env.poly_ts  ->
-        Mty.fold (fun uty _ s -> Ssubst.add (ty_match Mtv.empty ty uty) s)
+        Mty.fold (fun uty _ s ->
+          try
+            Ssubst.add (ty_match Mtv.empty ty uty) s
+          with Ty.TypeMismatch _ ->
+            (* No instantiation possible *)
+            s
+        )
           env.keep s
       | _ -> s in
   f_ty_fold add_vs Ssubst.empty
@@ -320,7 +327,7 @@ let collect_arrays poly_ts tds =
   Sts.fold extract tds Mty.empty
 
 let meta_mono_array = register_meta "encoding_arrays : mono_arrays"
-  [MTtysymbol;MTtysymbol;MTtysymbol]
+  [MTtysymbol;MTty;MTty]
 
 (* Some general env creation function *)
 let create_env env task thpoly tds =

src/transform/encoding_sort.ml

@@ -150,7 +150,7 @@ let fold tenv taskpre task =
             | ls, None -> conv_ls tenv ud ls, None
             | _ -> Printer.unsupportedDecl d "use eliminate_definition"
           in
-          decl_ud ud (add_logic_decl task (List.map conv ll))
+          add_logic_decl (decl_ud ud task) (List.map conv ll)
         | Dind _ ->
           Printer.unsupportedDecl d "use eliminate_inductive"
         | Dprop _ ->
@@ -165,12 +165,13 @@ let fold tenv taskpre task =
           | MAty ty -> MAty (conv_ty tenv ud ty)
           | MAts {ts_name = name; ts_args = []; ts_def = Some ty} ->
             MAts (conv_ts tenv ud name ty)
+          | MAts {ts_args = []; ts_def = None} as x -> x
           | MAts _ -> raise Exit
           | MAls ls -> MAls (conv_ls tenv ud ls)
           | MApr _ -> raise Exit
           | MAstr _ as s -> s
           | MAint _ as i -> i in
-        decl_ud ud (add_meta task meta (List.map map ml))
+        add_meta (decl_ud ud task) meta (List.map map ml)
       with
         | Printer.UnsupportedType _
         | Exit -> add_tdecl task taskpre.task_decl