refactor: extract Model into its own library

src/model/dune

@@ -0,0 +1,6 @@
+(library
+ (name sidekick_model)
+ (public_name sidekick.model)
+ (synopsis "Finite models for Sidekick")
+ (libraries sidekick.sigs sidekick.util sidekick.core)
+ (flags :standard -w +32 -open Sidekick_util))

src/model/sidekick_model.ml

@@ -0,0 +1,24 @@
+open Sidekick_core
+module T = Term
+
+type t = { m: Term.t T.Map.t } [@@unboxed]
+
+let empty : t = { m = T.Map.empty }
+let is_empty self = T.Map.is_empty self.m
+let mem self t = T.Map.mem t self.m
+let find self t = T.Map.find_opt t self.m
+let eval = find
+let add t v self : t = { m = T.Map.add t v self.m }
+let keys self = T.Map.keys self.m
+let to_iter self = T.Map.to_iter self.m
+
+let pp out (self : t) =
+  if is_empty self then
+    Fmt.string out "(model)"
+  else (
+    let pp_pair out (t, v) =
+      Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Term.pp v
+    in
+    Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
+      (T.Map.to_iter self.m)
+  )

src/model/sidekick_model.mli

@@ -0,0 +1,19 @@
+(** Models
+
+    A model can be produced when the solver is found to be in a
+    satisfiable state after a call to {!solve}. *)
+
+open Sidekick_core
+
+type t
+
+val empty : t
+val is_empty : t -> bool
+val mem : t -> Term.t -> bool
+val find : t -> Term.t -> Term.t option
+val eval : t -> Term.t -> Term.t option
+val add : Term.t -> Term.t -> t -> t
+val keys : t -> Term.t Iter.t
+val to_iter : t -> (Term.t * Term.t) Iter.t
+
+include Sidekick_sigs.PRINT with type t := t

src/smt/Sidekick_smt_solver.ml

@@ -7,7 +7,7 @@
 *)
 
 module Sigs = Sigs
-module Model = Model
+module Model = Sidekick_model
 module Model_builder = Model_builder
 module Registry = Registry
 module Solver_internal = Solver_internal

src/smt/dune

@@ -3,5 +3,5 @@
  (public_name sidekick.smt-solver)
  (synopsis "main SMT solver")
  (libraries containers iter sidekick.core sidekick.util sidekick.cc
-   sidekick.sat sidekick.simplify)
+   sidekick.sat sidekick.simplify sidekick.model)
  (flags :standard -w +32 -open Sidekick_util))

src/smt/model.ml

@@ -1,28 +0,0 @@
-open Sigs
-
-type t = Empty | Map of term Term.Tbl.t
-
-let empty = Empty
-
-let mem = function
-  | Empty -> fun _ -> false
-  | Map tbl -> Term.Tbl.mem tbl
-
-let find = function
-  | Empty -> fun _ -> None
-  | Map tbl -> Term.Tbl.get tbl
-
-let eval = find
-
-let pp out = function
-  | Empty -> Fmt.string out "(model)"
-  | Map tbl ->
-    let pp_pair out (t, v) =
-      Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp_debug t Term.pp_debug v
-    in
-    Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
-      (Term.Tbl.to_iter tbl)
-
-module Internal_ = struct
-  let of_tbl t = Map t
-end

src/smt/model.mli

@@ -1,18 +0,0 @@
-(** Models
-
-      A model can be produced when the solver is found to be in a
-      satisfiable state after a call to {!solve}. *)
-
-open Sigs
-
-type t
-
-val empty : t
-val mem : t -> term -> bool
-val find : t -> term -> term option
-val eval : t -> term -> term option
-val pp : t Fmt.printer
-
-module Internal_ : sig
-  val of_tbl : term Term.Tbl.t -> t
-end

src/smt/model_builder.ml

@@ -3,7 +3,7 @@ module T = Term
 
 type t = {
   tst: Term.store;
-  m: Term.t T.Tbl.t;
+  mutable m: Model.t;
   required: Term.t Queue.t;
   gensym: Gensym.t;
 }
@@ -11,15 +11,14 @@ type t = {
 let create tst : t =
   {
     tst;
-    m = T.Tbl.create 8;
+    m = Model.empty;
     required = Queue.create ();
     gensym = Gensym.create tst;
   }
 
 let pp out (self : t) : unit =
-  let pp_pair out (t, v) = Fmt.fprintf out "(@[%a :=@ %a@])" T.pp t T.pp v in
+  Fmt.fprintf out "(@[model-builder@ :model %a@ :q (@[%a@])@])" Model.pp self.m
-  Fmt.fprintf out "(@[model-builder@ :m (@[%a@])@ :q (@[%a@])@])"
+    (Util.pp_iter T.pp)
-    (Util.pp_iter pp_pair) (T.Tbl.to_iter self.m) (Util.pp_iter T.pp)
     (Iter.of_queue self.required)
 
 let gensym self ~pre ~ty : Term.t = Gensym.fresh_term self.gensym ~pre ty
@@ -27,33 +26,33 @@ let gensym self ~pre ~ty : Term.t = Gensym.fresh_term self.gensym ~pre ty
 let rec pop_required (self : t) : _ option =
   match Queue.take_opt self.required with
   | None -> None
-  | Some t when T.Tbl.mem self.m t -> pop_required self
+  | Some t when Model.mem self.m t -> pop_required self
   | Some t -> Some t
 
 let require_eval (self : t) t : unit =
-  if not @@ T.Tbl.mem self.m t then Queue.push t self.required
+  if not @@ Model.mem self.m t then Queue.push t self.required
 
-let mem self t : bool = T.Tbl.mem self.m t
+let[@inline] mem self t : bool = Model.mem self.m t
 
 let add (self : t) ?(subs = []) t v : unit =
-  if not @@ T.Tbl.mem self.m t then (
+  if not @@ mem self t then (
-    T.Tbl.add self.m t v;
+    self.m <- Model.add t v self.m;
     List.iter (fun u -> require_eval self u) subs
   )
 
 type eval_cache = Term.Internal_.cache
 
 let eval ?(cache = Term.Internal_.create_cache 8) (self : t) (t : Term.t) =
-  let t = try T.Tbl.find self.m t with Not_found -> t in
+  let t = Model.find self.m t |> Option.value ~default:t in
   T.Internal_.replace_ ~cache self.tst ~recursive:true t ~f:(fun ~recurse:_ u ->
-      T.Tbl.find_opt self.m u)
+      Model.find self.m u)
 
 let to_model (self : t) : Model.t =
   (* ensure we evaluate each term only once *)
   let cache = T.Internal_.create_cache 8 in
-  let tbl =
+  let m =
-    T.Tbl.keys self.m
+    Model.keys self.m
     |> Iter.map (fun t -> t, eval ~cache self t)
-    |> T.Tbl.of_iter
+    |> Iter.fold (fun m (t, v) -> Model.add t v m) Model.empty
   in
-  Model.Internal_.of_tbl tbl
+  m

src/smt/sigs.ml

@@ -13,6 +13,7 @@
 *)
 
 include Sidekick_core
+module Model = Sidekick_model
 module Simplify = Sidekick_simplify
 module CC = Sidekick_cc.CC
 module E_node = Sidekick_cc.E_node