theory for uninterpreted types

src/base/th_ty_unin.ml

@@ -0,0 +1,5 @@
+let theory : Solver.theory =
+  Sidekick_th_ty_unin.theory
+    (module struct
+      let ty_is_unin = Ty.is_uninterpreted
+    end : Sidekick_th_ty_unin.ARG)

src/th-unin-ty/dune

@@ -0,0 +1,6 @@
+(library
+ (name sidekick_th_ty_unin)
+ (public_name sidekick.th-ty-unin)
+ (synopsis "Theory for uninterpreted types")
+ (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)
+ (libraries containers sidekick.cc sidekick.smt-solver))

src/th-unin-ty/sidekick_th_ty_unin.ml

@@ -0,0 +1,43 @@
+open Sidekick_core
+open Sidekick_smt_solver
+
+open struct
+  module SI = Solver_internal
+end
+
+type ty = Term.t
+
+module type ARG = sig
+  val ty_is_unin : ty -> bool
+end
+
+module Make (A : ARG) = struct
+  open A
+
+  type t = { gensym: Gensym.t }
+
+  let create (tst : Term.store) : t =
+    let gensym = Gensym.create tst in
+    { gensym }
+
+  let pop_levels (self : t) n = if n > 0 then Gensym.reset self.gensym
+
+  let model_ask_ (self : t) (_solver : SI.t) (_m : Model_builder.t) (t : Term.t)
+      : _ option =
+    if ty_is_unin (Term.ty t) then (
+      let s = Gensym.fresh_term self.gensym ~pre:"@c" (Term.ty t) in
+      Some (s, [])
+    ) else
+      None
+
+  let create_and_setup ~id:_ (solver : SI.t) : t =
+    let state = create (SI.tst solver) in
+    SI.on_model solver ~ask:(model_ask_ state);
+    state
+
+  let theory = Solver.mk_theory ~name:"ty-unin" ~create_and_setup ~pop_levels ()
+end
+
+let theory (arg : (module ARG)) : Theory.t =
+  let module M = Make ((val arg)) in
+  M.theory

src/th-unin-ty/sidekick_th_ty_unin.mli

@@ -0,0 +1,10 @@
+open Sidekick_core
+
+type ty = Term.t
+
+module type ARG = sig
+  val ty_is_unin : ty -> bool
+end
+
+val theory : (module ARG) -> Sidekick_smt_solver.Theory.t
+(** Theory of uninterpreted types *)