[smt]: proper selection of SMT variant

Why3 can define several variants (e.g. counterexamples, noBV).

Currently, EasyCrypt select the first variant that comes in the
prover list. From now on, the default variant (= empty name) is
selected by default. It is also possible to provide the desired
in the prover name (syntax = "prover[variant]", e.g. "Z3[noBV]").

This is compatible with the version selection (e.g. "Z3[noBV]@4.8")

Author: strub

examples/ChaChaPoly/chacha_poly.ec

@@ -1691,9 +1691,8 @@ section PROOFS.
         swap 13 9; wp; conseq (_: true) => />; 1: smt(); islossless.
         while true (size p2).
         + move=> z; wp; conseq (_: true) => //=; 2: by islossless.
-          move => &hr; elim (p2{hr}) => //. 
-          clear &hr.
-          smt (size_drop size_eq0 gt0_block_size).
+          move => &hr; elim (p2{hr}) => //= => {&hr}.
+          smt (size_drop size_ge0 size_eq0 gt0_block_size).
         by auto; smt (size_ge0 size_eq0 dpoly_out_ll). 
       + by proc; inline *; sp 1 1; if; auto => /> *; smt(get_setE mem_set).
       + by move=> &2 _; islossless.

src/ec.ml

@@ -70,11 +70,15 @@ let print_config config =
 
   (* Print list of known provers *)
   begin
-    let string_of_prover prover =
+    let string_of_prover (prover : EcProvers.prover) =
       let fullname =
-        Printf.sprintf "%s@%s"
-          prover.EcProvers.pr_name
-          (EcProvers.Version.to_string prover.EcProvers.pr_version) in
+        Format.asprintf "%s%t@%s"
+          prover.pr_name
+          (fun fmt ->
+            if not (String.is_empty prover.pr_alt) then
+              Format.fprintf fmt "[%s]" prover.pr_alt)
+          (EcProvers.Version.to_string prover.pr_version)
+      in
 
       match prover.EcProvers.pr_evicted with
       | None -> fullname

src/ecProvers.ml

@@ -50,8 +50,13 @@ end = struct
     compare v1.v_extra v2.v_extra
 
   let to_string (v : version) =
-    Printf.sprintf "%d.%d.%d.%s"
-      v.v_major v.v_minor v.v_subminor v.v_extra
+    let parts = [v.v_major; v.v_minor; v.v_subminor] in
+    let parts = List.map string_of_int parts in
+    let parts =
+      let extra = if String.is_empty v.v_extra then None else Some v.v_extra in
+      ofold (fun extra parts -> parts @ [extra]) parts extra in
+
+    String.concat "." parts
 end
 
 module VP = Version
@@ -108,6 +113,7 @@ let evictions : prover_eviction_test list = [
 type prover = {
   pr_name    : string;
   pr_version : Version.version;
+  pr_alt     : string;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -156,6 +162,7 @@ end = struct
         { pr_prover  =
             { pr_name    = name;
               pr_version = Version.parse version;
+              pr_alt     = p.Whyconf.prover_altern;
               pr_evicted = None; };
           pr_config  = config;
           pr_driver  = driver; }
@@ -166,6 +173,15 @@ end = struct
           (fun p c acc -> load_prover p c :: acc)
           (Whyconf.get_provers config) [] in
 
+      let provers =
+        let key_of_prover (p : why3prover) =
+          let p = p.pr_prover in
+          (p.pr_name, p.pr_version, p.pr_alt) in
+
+        List.sort
+          (fun p1 p2 -> compare (key_of_prover p1) (key_of_prover p2))
+          provers in
+
       let provers =
         List.map (fun prover ->
             let prinfo   = prover.pr_prover in
@@ -212,6 +228,7 @@ exception UnknownProver of string
 
 type parsed_pname = {
   prn_name     : string;
+  prn_alt      : string;
   prn_version  : Version.version option;
   prn_ovrevict : bool;
 }
@@ -228,19 +245,32 @@ let parse_prover_name name =
 
   let version = omap Version.parse version in
 
-  if   name <> "" && name.[0] = '!'
-  then { prn_name     = String.sub name 1 (String.length name - 1);
-         prn_version  = version;
-         prn_ovrevict = true; }
-  else { prn_name     = name;
-         prn_version  = version;
-         prn_ovrevict = false; }
+  let ovrevict, name =
+      if name <> "" && name.[0] = '!' then
+        true, String.sub name 1 (String.length name - 1)
+      else false, name in
+
+  let name, alt =
+    let re = EcRegexp.regexp "^(.*)\\[(.*)\\]$" in
+    match EcRegexp.exec (`C re) name with
+    | None ->
+      name, ""
+    | Some m ->
+      let name = oget (EcRegexp.Match.group m 1) in
+      let alt  = oget (EcRegexp.Match.group m 2) in
+      name, alt in
+
+  { prn_name     = name;
+    prn_version  = version;
+    prn_alt      = alt;
+    prn_ovrevict = ovrevict; }
 
 let get_prover (rawname : string) =
   let name = parse_prover_name rawname in
 
   let test p =
        p.pr_prover.pr_name = name.prn_name
+    && p.pr_prover.pr_alt  = name.prn_alt
     && (name.prn_ovrevict || not (is_evicted p.pr_prover)) in
 
   let provers = List.filter test (Config.provers ()) in
@@ -399,6 +429,7 @@ let run_prover
   EcUtils.try_finally (fun () ->
     try
       let { pr_config = pr; pr_driver = dr; } = get_prover prover in
+
       let pc =
         let command = pr.Whyconf.command in
 

src/ecProvers.mli

@@ -30,6 +30,7 @@ type prover_eviction = [
 type prover = {
   pr_name    : string;
   pr_version : Version.version;
+  pr_alt     : string;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -58,6 +59,7 @@ val known : evicted:bool -> prover list
 (* -------------------------------------------------------------------- *)
 type parsed_pname = {
   prn_name     : string;
+  prn_alt      : string;
   prn_version  : Version.version option;
   prn_ovrevict : bool;
 }

theories/distributions/DInterval.ec

@@ -69,7 +69,8 @@ have uniq_s: uniq s; first apply: uniq_flatten_map.
   by move => x y _ _ /=; apply/addrI.
 - move=> x y /mem_range rg_x /mem_range rg_y /hasP /=.
   case=> j [/mapP[/= k [/mem_range rg_k]] ->>].
-  by case/mapP=> l [/mem_range rg_l] {rg_x} {rg_y} /#.
+  case/mapP=> l [/mem_range rg_l] {rg_x} {rg_y}.
+  smt(IntDiv.euclideU).
 - by apply: range_uniq.
 have mem_s: forall x, (x \in s) <=> (x \in range 0 p).
 - move=> x; rewrite mem_range; split.