perf(smt): no relevance tables when no lemma is to be selected

src/ecProvers.ml

@@ -383,6 +383,27 @@ module Hints = struct
       | None -> assert false
       | Some `Include -> true
       | Some `Exclude -> false
+
+  let included (m : hints) =
+    let rec doit prefix (m : hints) (inherited : hflag) acc =
+      let this =
+        match m.ht_this with
+        | `Inherit -> inherited
+        | #hflag as flag -> flag in
+      let sub x =
+        match prefix with
+        | None   -> EcPath.psymbol x
+        | Some p -> EcPath.pqname p x in
+      match prefix, this with
+      | None  , `Include -> `All :: acc
+      | Some p, `Include -> if inherited = `Include then acc else `Theory p :: acc
+      | _     , `Exclude ->
+          let acc =
+            Msym.fold
+              (fun x flag acc -> if flag = `Include then `Lemma (sub x) :: acc else acc)
+              m.ht_axs acc in
+          Msym.fold (fun x m acc -> doit (Some (sub x)) m this acc) m.ht_sub acc
+    in doit None m `Exclude []
 end
 
 (* -------------------------------------------------------------------- *)

src/ecProvers.mli

@@ -13,6 +13,10 @@ module Hints : sig
   val addm : path -> hflag -> hints -> hints
 
   val mem : path -> hints -> bool
+
+  (* The inclusions of the hints: the lemmas flagged so, the theories
+     flagged so that no included theory contains, or everything. *)
+  val included : hints -> [ `All | `Lemma of path | `Theory of path ] list
 end
 
 (* -------------------------------------------------------------------- *)

src/ecSmt.ml

@@ -1679,6 +1679,38 @@ let select env pi hyps concl execute_task =
     let init_select p ax =
       ax.ax_smt && not (P.Hints.mem p pi.P.pr_unwanted) in
     (execute_task (EcEnv.Ax.all ~check:init_select env) = Some true)
+  else if pi.P.pr_max <= 0 then
+    (* No lemma is selected beyond the ones given (this is the case of
+       `smt(lemmas)` without `maxlemmas`): the relevance tables, which
+       scan every axiom of the environment, are not built, and the given
+       lemmas are resolved by their path, the given theories walked. The
+       items of abstract theories are not bound in the environment and
+       are skipped, as the scan would have. *)
+    let wanted = pi.P.pr_wanted in
+    let rec of_theory (p : EcPath.path) (cth : EcTheory.ctheory) acc =
+      if cth.EcTheory.cth_mode = `Abstract then acc else
+      List.fold_left (fun acc (item : EcTheory.theory_item) ->
+          match item.ti_item with
+          | EcTheory.Th_axiom (x, ax) ->
+              let p = EcPath.pqname p x in
+              if P.Hints.mem p wanted then (p, ax) :: acc else acc
+          | EcTheory.Th_theory (x, sub) ->
+              of_theory (EcPath.pqname p x) sub acc
+          | _ -> acc)
+        acc cth.cth_items in
+    let toadd =
+      List.fold_left (fun acc h ->
+          match h with
+          | `All ->
+              EcEnv.Ax.all ~check:(fun p _ -> P.Hints.mem p wanted) env @ acc
+          | `Lemma p ->
+              Option.fold ~none:acc ~some:(fun ax -> (p, ax) :: acc)
+                (EcEnv.Ax.by_path_opt p env)
+          | `Theory p ->
+              Option.fold ~none:acc ~some:(fun cth -> of_theory p cth acc)
+                (EcEnv.Theory.by_path_opt ~mode:`All p env))
+        [] (P.Hints.included wanted) in
+    (execute_task toadd = Some true)
   else
     let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in
     let ri, other = init_relevant env pi rs in

tests/smt-given-lemmas.ec

@@ -0,0 +1,25 @@
+(* `smt(lemmas)` without `maxlemmas` sends the given lemmas and nothing
+   else: a lemma by its path, a theory by all its lemmas, including those
+   of its sub-theories. *)
+require import AllCore.
+
+op f : int -> int.
+op g : int -> int.
+
+theory T.
+  axiom fP (x : int) : 0 <= f x.
+
+  theory U.
+    axiom gP (x : int) : f x <= g x.
+  end U.
+
+  abstract theory A.
+    module M = { proc m() : int = { return 0; } }.
+    axiom mP : hoare[M.m : true ==> res = 0].
+  end A.
+end T.
+
+lemma t1 (x : int) : 0 <= f x by smt(T.fP).
+lemma t2 (x : int) : 0 <= g x by smt(T.fP T.U.gP).
+lemma t3 (x : int) : 0 <= g x by smt(@T).
+lemma t4 (x : int) : f x <= g x by smt(@T.U).