z3 use array encoding

drivers/z3_smtv2_array.drv

@@ -164,6 +164,7 @@ theory array.Array
   meta "encoding : lskept" logic get
   meta "encoding : lskept" logic set
   meta "encoding : lskept" logic create_const
+
   meta "smt_dist_syntax" logic get, "(select %1 %2)"
   meta "smt_dist_syntax" logic set, "(store %1 %2 %3)"
   meta "smt_dist_syntax" logic create_const, "(const[%t0] %1)"

share/provers-detection-data.conf.in

@@ -88,18 +88,30 @@ version_regexp = "Version: \\([^ \n\r]+\\)"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/verit.drv"
 
-[ATP z3]
+[ATP z3_smtv1]
 name = "Z3"
 exec = "z3"
 exec = "z3-2.2"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
-version_ok = "2.2"
+version_old = "2.2"
 version_old = "2.1"
 version_old = "1.3"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
 driver = "drivers/z3.drv"
 
+[ATP z3]
+name = "Z3"
+exec = "z3"
+version_switch = "-version"
+version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok = "2.19"
+version_old = "2.18"
+version_old = "2.17"
+version_old = "2.16"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 %f"
+driver = "drivers/z3_smtv2_array.drv"
+
 [ITP coq]
 name = "Coq"
 exec = "coqc"

src/driver/autodetection.ml

@@ -189,6 +189,6 @@ let run_auto_detection config =
   let main = get_main config in
   let l = read_auto_detection_data main in
   let detect = List.fold_left (detect_prover main) Mstr.empty l in
-  let length = Mstr.fold (fun _ _ i -> i+1) detect 0 in
+  let length = Mstr.cardinal detect in
   eprintf "%d provers detected.@." length;
   set_provers config detect

src/transform/encoding_arrays.ml

@@ -301,7 +301,7 @@ let env_from_kept_lskept kept lskept =
           try
             let subst = ty_match subst ty tykept in
             aux insts (tykept::tydisl) subst tyl
-          with Not_found -> insts
+          with TypeMismatch _ -> insts
         in
         Sty.fold fold_ty kept insts
     in
@@ -344,18 +344,20 @@ let env_of_metas metas =
   in
   List.fold_left fold Mls.empty metas
 
-let env_from_fold lskept env ls tyl tyv =
+let env_from_fold lskept (env,kept) ls tyl tyv =
   if Sls.mem ls lskept &&
     List.for_all is_ty_mono tyl && option_apply true is_ty_mono tyv then
     let tydisl = option_apply tyl (fun e -> e::tyl) tyv
     in
     let lsdis = create_lsymbol (id_clone ls.ls_name) tyl tyv in
     let insts = Mls.find_default ls Mtyl.empty env in
-    Mls.add ls (Mtyl.add tydisl lsdis insts) env
-  else env
+    Mls.add ls (Mtyl.add tydisl lsdis insts) env,
+    List.fold_left (fun acc ty -> Sty.add ty acc) kept tydisl
+  else (env,kept)
 
-let mono_in_goal sls pr f =
-  let env = f_app_fold (env_from_fold sls) Mls.empty f in
+let mono_in_goal lskept pr f =
+  let _,kept = f_app_fold (env_from_fold lskept) (Mls.empty,Sty.empty) f in
+  let env = env_from_kept_lskept kept lskept in
   (* Format.eprintf "mono_in_goal %a@." print_env env; *)
   metas_of_env env [create_decl (create_prop_decl Pgoal pr f)]