Locking the Dolmen to a dev commit

This commit locks the Dolmen used by AE to a specific commit
in order to use the unreleased feature for custom statements.

I also notice that the `with_cache` in `d_cnf` was silently shadow by
the same function from the module `Expr` of `Dolmen`. The signature of
this latter changed recently. I fix it by using the `with_cache` from
Dolmen. Notice that the hash table of the cache is hidden in the closure
of `with_cache` and `bv2nat` and `int2bv` don't share their cache as
before.

alt-ergo-lib.opam

@@ -59,3 +59,18 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+  "dolmen.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+  [
+  "dolmen_loop.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+  [
+  "dolmen_type.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+]

alt-ergo-lib.opam.locked

@@ -8,18 +8,21 @@ This is the core library used in the Alt-Ergo SMT solver.
 Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
 
 See more details on http://alt-ergo.ocamlpro.com/"""
-maintainer: "Alt-Ergo developers"
-authors: "Alt-Ergo developers"
+maintainer: "Alt-Ergo developers <[email protected]>"
+authors: "Alt-Ergo developers <[email protected]>"
 license: ["LicenseRef-OCamlpro-Non-Commercial" "Apache-2.0"]
 tags: "org:OCamlPro"
 homepage: "https://alt-ergo.ocamlpro.com/"
 doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
+  "astring" {= "0.8.5" & with-doc}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
+  "biniou" {= "1.2.1"}
+  "camlp-streams" {= "5.0.1" & with-doc}
   "camlzip" {= "1.11"}
   "cmdliner" {= "1.2.0"}
   "conf-gmp" {= "4"}
@@ -30,36 +33,45 @@ depends: [
   "dolmen" {= "0.9"}
   "dolmen_loop" {= "0.9"}
   "dolmen_type" {= "0.9"}
-  "dune" {= "3.10.0"}
-  "dune-build-info" {= "3.10.0"}
-  "dune-configurator" {= "3.10.0"}
+  "dune" {= "3.11.1"}
+  "dune-build-info" {= "3.11.1"}
+  "dune-configurator" {= "3.11.1"}
+  "easy-format" {= "1.3.4"}
   "fmt" {= "0.9.0"}
+  "fpath" {= "0.7.3" & with-doc}
   "gen" {= "1.1"}
   "js_of_ocaml" {= "5.4.0"}
   "js_of_ocaml-compiler" {= "5.4.0"}
   "logs" {= "0.7.0"}
-  "lwt" {= "5.6.1"}
+  "lwt" {= "5.7.0"}
   "menhir" {= "20230608"}
   "menhirLib" {= "20230608"}
   "menhirSdk" {= "20230608"}
   "num" {= "1.4"}
   "ocaml-compiler-libs" {= "v0.12.4"}
+  "ocaml-options-vanilla" {= "1"}
   "ocamlbuild" {= "0.14.2"}
   "ocamlfind" {= "1.9.6"}
   "ocplib-endian" {= "1.2"}
   "ocplib-simplex" {= "0.5"}
+  "odoc" {= "2.2.1" & with-doc}
+  "odoc-parser" {= "2.0.0" & with-doc}
   "pp_loc" {= "2.1.0"}
   "ppx_blob" {= "0.7.2"}
   "ppx_derivers" {= "1.2.1"}
-  "ppxlib" {= "0.30.0"}
+  "ppx_deriving" {= "5.2.1"}
+  "ppxlib" {= "0.31.0"}
+  "re" {= "1.11.0" & with-doc}
+  "result" {= "1.5"}
   "sedlex" {= "3.2"}
   "seq" {= "base"}
-  "sexplib0" {= "v0.15.1"}
+  "sexplib0" {= "v0.16.0"}
   "spelll" {= "0.4"}
   "stdlib-shims" {= "0.3.0"}
   "topkg" {= "1.0.7"}
+  "tyxml" {= "4.6.0" & with-doc}
   "uutf" {= "1.0.3"}
-  "yojson" {= "2.1.0"}
+  "yojson" {= "1.7.0"}
   "zarith" {= "1.13"}
 ]
 build: [
@@ -78,4 +90,8 @@ build: [
   ]
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+conflicts: [
+  "ppxlib" {< "0.30.0"}
+  "result" {< "1.5"}
+]

alt-ergo-lib.opam.template

@@ -6,3 +6,18 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+  "dolmen.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+  [
+  "dolmen_loop.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+  [
+  "dolmen_type.dev"
+  "git+https://github.com/Gbury/dolmen.git#baaf1f92ccd473294679dd9025c3ae9a441a82fa"
+  ]
+]

src/lib/frontend/d_cnf.ml

@@ -193,24 +193,17 @@ type _ DStd.Builtin.t +=
   (* Internal use for semantic triggers -- do not expose outside of theories *)
   | Not_theory_constant | Is_theory_constant | Linear_dependency
 
-let with_cache ~cache f x =
-  try Hashtbl.find cache x
-  with Not_found ->
-    let res = f x in
-    Hashtbl.add cache x res;
-    res
-
 module Const = struct
   open DE
 
   let bv2nat =
-    with_cache ~cache:(Hashtbl.create 13) (fun n ->
+    with_cache (fun n ->
         let name = "bv2nat" in
         Id.mk ~name ~builtin:(BV2Nat n)
           (DStd.Path.global name) Ty.(arrow [bitv n] int))
 
   let int2bv =
-    with_cache ~cache:(Hashtbl.create 13) (fun n ->
+    with_cache (fun n ->
         let name = "int2bv" in
         Id.mk ~name ~builtin:(Int2BV n)
           (DStd.Path.global name) Ty.(arrow [int] (bitv n)))