Adds caches_consts flag to mappings

Solvers can inform us that they cache constants by setting the flag
`caches_consts = true` in their mappings. This should avoid having a
`Map.find_opt` everytime we call `make_symbol`.

Concretely `caches_consts = true` is when we have:
`assert(ty1 = ty2) => M.eq (M.const "x" ty1) (M.const "x" ty2)` is sat.

Currently the mappings that behave like this are only Z3

src/bitwuzla_mappings.default.ml

@@ -18,6 +18,7 @@
 
 include Mappings_intf
 
+(* Hack: this was a hack to try and run bitwuzla in Owi *)
 let leak =
   let leaky_list = ref [] in
   let mutex = Mutex.create () in
@@ -48,6 +49,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   (* Not supported *)
   type func_decl = unit
 
+  let caches_consts = false
+
   let true_ = mk_true ()
 
   let false_ = mk_false ()

src/cvc5_mappings.default.ml

@@ -36,6 +36,8 @@ module Fresh_cvc5 () = struct
 
   type func_decl = unit
 
+  let caches_consts = true
+
   let tm = TermManager.mk_tm ()
 
   let true_ = Term.mk_true tm

src/mappings.ml

@@ -79,14 +79,16 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         Fmt.failwith "Unsupported theory: %a@." Ty.pp ty
 
     let make_symbol (ctx : symbol_ctx) (s : Symbol.t) : symbol_ctx * M.term =
-      match Smap.find_opt s ctx with
-      | Some sym -> (ctx, sym)
-      | None ->
-        let name =
-          match s.name with Simple name -> name | _ -> assert false
-        in
+      let name = match s.name with Simple name -> name | _ -> assert false in
+      if M.caches_consts then
         let sym = M.const name (get_type s.ty) in
         (Smap.add s sym ctx, sym)
+      else
+        match Smap.find_opt s ctx with
+        | Some sym -> (ctx, sym)
+        | None ->
+          let sym = M.const name (get_type s.ty) in
+          (Smap.add s sym ctx, sym)
 
     module Bool_impl = struct
       let true_ = M.true_

src/mappings.nop.ml

@@ -34,6 +34,8 @@ module Nop = struct
 
     type func_decl = unit
 
+    let caches_consts = false
+
     let true_ = ()
 
     let false_ = ()

src/mappings_intf.ml

@@ -39,6 +39,8 @@ module type M = sig
 
   type func_decl
 
+  val caches_consts : bool
+
   val true_ : term
 
   val false_ : term