Allows selecting a prover by its version number.

Syntax is name@version. The selected prover is the prover with name
`name` and with the lowest version that is greater (or equal) than
`version`.

For example, if Z3 4.8.0, Z3 4.8.2 & Z3 4.12.2 are installed, [email protected]
selects Z3 4.8.2.

Makefile

@@ -6,7 +6,7 @@ ECARGS    ?=
 ECTOUT    ?= 10
 ECJOBS    ?= 0
 ECEXTRA   ?= --report=report.log
-ECPROVERS ?= Alt-Ergo Z3 CVC4
+ECPROVERS ?= Alt-Ergo@2.4 Z3@4.8 CVC4@1.8
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
 CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"

src/ec.ml

@@ -72,7 +72,7 @@ let print_config config =
       let fullname =
         Printf.sprintf "%s@%s"
           prover.EcProvers.pr_name
-          prover.EcProvers.pr_version in
+          (EcProvers.Version.to_string prover.EcProvers.pr_version) in
 
       match prover.EcProvers.pr_evicted with
       | None -> fullname

src/ecProvers.ml

@@ -70,7 +70,7 @@ let test_if_evict_prover test (name, version) =
   let evict =
     match test.pe_test with
     | `ByVersion (tname, (trel, tversion)) when name = tname -> begin
-        let cmp = VP.compare (VP.parse version) tversion in
+        let cmp = VP.compare version tversion in
         match trel with
         | `Eq -> cmp =  0
         | `Lt -> cmp <  0
@@ -107,7 +107,7 @@ let evictions : prover_eviction_test list = [
 (* -------------------------------------------------------------------- *)
 type prover = {
   pr_name    : string;
-  pr_version : string;
+  pr_version : Version.version;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -155,7 +155,7 @@ end = struct
 
         { pr_prover  =
             { pr_name    = name;
-              pr_version = version;
+              pr_version = Version.parse version;
               pr_evicted = None; };
           pr_config  = config;
           pr_driver  = driver; }
@@ -212,24 +212,65 @@ exception UnknownProver of string
 
 type parsed_pname = {
   prn_name     : string;
+  prn_version  : Version.version option;
   prn_ovrevict : bool;
 }
 
 let parse_prover_name name =
+  let name, version =
+    if String.contains name '@' then
+      let index   = String.index name '@' in
+      let name    = String.sub name 0 index
+      and version = String.sub name (index+1) (String.length name - (index+1)) in
+      (name, Some version)
+    else
+      (name, None) in
+
+  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_ovrevict = false; }
+  else { prn_name     = name;
+         prn_version  = version;
+         prn_ovrevict = false; }
 
-let get_prover name =
-  let name = parse_prover_name name in
+let get_prover (rawname : string) =
+  let name = parse_prover_name rawname in
 
   let test p =
        p.pr_prover.pr_name = name.prn_name
     && (name.prn_ovrevict || not (is_evicted p.pr_prover)) in
 
-  try  List.find test (Config.provers ())
-  with Not_found -> raise (UnknownProver name.prn_name)
+  let provers = List.filter test (Config.provers ()) in
+
+  let provers = List.sort (fun p1 p2 ->
+      let v1 = p1.pr_prover.pr_version in
+      let v2 = p2.pr_prover.pr_version in
+      Version.compare v1 v2
+    ) provers
+  in
+
+  let exception CannotFindProver in
+
+  try
+    match name.prn_version with
+    | None ->
+        oget ~exn:CannotFindProver (List.Exceptionless.hd (List.rev provers))
+
+    | Some version -> begin
+        try
+          List.find
+            (fun p ->
+               Version.compare version p.pr_prover.pr_version <= 0)
+          provers
+
+        with Not_found -> raise CannotFindProver
+      end
+
+  with CannotFindProver ->
+    raise (UnknownProver rawname)
 
 let is_prover_known name =
   try ignore (get_prover name); true with UnknownProver _ -> false

src/ecProvers.mli

@@ -15,14 +15,21 @@ module Hints : sig
   val mem : path -> hints -> bool
 end
 
+(* -------------------------------------------------------------------- *)
+module Version : sig
+  type version
+
+  val to_string : version -> string
+end
+
 (* -------------------------------------------------------------------- *)
 type prover_eviction = [
   | `Inconsistent
 ]
 
 type prover = {
   pr_name    : string;
-  pr_version : string;
+  pr_version : Version.version;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -51,6 +58,7 @@ val known : evicted:bool -> prover list
 (* -------------------------------------------------------------------- *)
 type parsed_pname = {
   prn_name     : string;
+  prn_version  : Version.version option;
   prn_ovrevict : bool;
 }