refactor: provide a state for Ty.bool in core signature

src/arith/base-term/Base_types.ml

@@ -260,6 +260,7 @@ let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
 
 module Ty : sig
   type t = ty
+  type state = unit
   type view = ty_view =
     | Ty_bool
     | Ty_real
@@ -283,8 +284,8 @@ module Ty : sig
   val id : t -> int
   val view : t -> view
 
-  val bool : t
+  val bool : state -> t
-  val real : t
+  val real : state -> t
   val atomic : def -> t list -> t
 
   val atomic_uninterpreted : ID.t -> t
@@ -316,6 +317,7 @@ module Ty : sig
   end
 end = struct
   type t = ty
+  type state = unit
   type view = ty_view =
     | Ty_bool
     | Ty_real
@@ -390,8 +392,8 @@ end = struct
     | Ty_bool | Ty_real -> assert false
     | Ty_atomic r -> r.finite <- b
 
-  let bool = make_ Ty_bool
+  let bool () = make_ Ty_bool
-  let real = make_ Ty_real
+  let real () = make_ Ty_real
 
   let atomic def args : t =
     make_ (Ty_atomic {def; args; finite=true;})
@@ -684,7 +686,7 @@ end = struct
   let[@inline] lra l : t = LRA l
 
   let ty (t:t): Ty.t = match t with
-    | Bool _ | Eq _ | Not _ -> Ty.bool
+    | Bool _ | Eq _ | Not _ -> Ty.bool ()
     | Ite (_, b, _) -> b.term_ty
     | App_fun (f, args) ->
       begin match Fun.view f with
@@ -707,15 +709,15 @@ end = struct
                ))
             ty_args;
           ty_ret
-        | Fun_is_a _ -> Ty.bool
+        | Fun_is_a _ -> Ty.bool ()
         | Fun_def def -> def.ty f.fun_id args
         | Fun_select s -> Lazy.force s.select_ty
         | Fun_cstor c -> Lazy.force c.cstor_ty
       end
     | LRA l ->
       begin match l with
-        | LRA_pred _ | LRA_simplex_pred _ -> Ty.bool
+        | LRA_pred _ | LRA_simplex_pred _ -> Ty.bool ()
-        | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_simplex_var _ -> Ty.real
+        | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_simplex_var _ -> Ty.real ()
         | LRA_other x -> x.term_ty
       end
 
@@ -864,7 +866,7 @@ end = struct
   }
 
   let[@inline] make st (c:t term_view) : t =
-    let t = {term_id= -1; term_ty=Ty.bool; term_view=c} in
+    let t = {term_id= -1; term_ty=Ty.bool(); term_view=c} in
     let t' = H.hashcons st.tbl t in
     if t == t' then (
       t'.term_ty <- Term_cell.ty c;

src/arith/lra/sidekick_arith_lra.ml

@@ -76,7 +76,10 @@ module type S = sig
 
   type state
 
-  val create : ?stat:Stat.t -> A.S.T.Term.state -> state
+  val create : ?stat:Stat.t ->
+    A.S.T.Term.state ->
+    A.S.T.Ty.state ->
+    state
 
   val theory : A.S.theory
 end
@@ -129,6 +132,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   type state = {
     tst: T.state;
+    ty_st: Ty.state;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
@@ -139,8 +143,8 @@ module Make(A : ARG) : S with module A = A = struct
     stat_th_comb: int Stat.counter;
   }
 
-  let create ?(stat=Stat.create()) tst : state =
+  let create ?(stat=Stat.create()) tst ty_st : state =
-    { tst;
+    { tst; ty_st;
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       encoded_eqs=T.Tbl.create 8;
@@ -163,7 +167,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
   let fresh_lit (self:state) ~mk_lit ~pre : Lit.t =
-    let t = fresh_term ~pre self Ty.bool in
+    let t = fresh_term ~pre self (Ty.bool self.ty_st) in
     mk_lit t
 
   let pp_pred_def out (p,l1,l2) : unit =
@@ -542,7 +546,7 @@ module Make(A : ARG) : S with module A = A = struct
   let create_and_setup si =
     Log.debug 2 "(th-lra.setup)";
     let stat = SI.stats si in
-    let st = create ~stat (SI.tst si) in
+    let st = create ~stat (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
     SI.add_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);

src/core/Sidekick_core.ml

@@ -56,7 +56,9 @@ module type TERM = sig
     val hash : t -> int
     val pp : t Fmt.printer
 
-    val bool : t
+    type state
+
+    val bool : state -> t
     val is_bool : t -> bool
   end
 
@@ -341,6 +343,7 @@ module type SOLVER_INTERNAL = sig
   type ty = T.Ty.t
   type term = T.Term.t
   type term_state = T.Term.state
+  type ty_state = T.Ty.state
   type proof = P.t
 
   (** {3 Main type for a solver} *)
@@ -348,6 +351,7 @@ module type SOLVER_INTERNAL = sig
   type solver = t
 
   val tst : t -> term_state
+  val ty_st : t -> ty_state
   val stats : t -> Stat.t
 
   (** {3 Actions for the theories} *)
@@ -380,6 +384,7 @@ module type SOLVER_INTERNAL = sig
     type t
 
     val tst : t -> term_state
+    val ty_st : t -> ty_state
 
     val clear : t -> unit
     (** Reset internal cache, etc. *)
@@ -662,6 +667,7 @@ module type SOLVER = sig
     ?store_proof:bool ->
     theories:theory list ->
     T.Term.state ->
+    T.Ty.state ->
     unit ->
     t
   (** Create a new solver.

src/main/main.ml

@@ -95,7 +95,8 @@ module Dimacs = struct
         match Util.Int_tbl.find atoms (abs i) with
         | x -> Term.const tst x
         | exception Not_found ->
-          let f = Sidekick_base_term.Fun.mk_undef_const (ID.makef "%d" (abs i)) Ty.bool in
+          let f = Sidekick_base_term.Fun.mk_undef_const
+              (ID.makef "%d" (abs i)) (Ty.bool()) in
           Util.Int_tbl.add atoms (abs i) f;
           Term.const tst f
       in
@@ -145,12 +146,12 @@ let main () =
   let solver =
     let theories =
       if is_cnf then [] else [
-        Process.th_bool ;
+        Process.th_bool;
         Process.th_data;
         Process.th_lra;
       ]
     in
-    Process.Solver.create ~store_proof:!check ~theories tst ()
+    Process.Solver.create ~store_proof:!check ~theories tst () ()
   in
   if !check then (
     (* might have to check conflicts *)

src/mini-cc/tests/tests.ml

@@ -12,7 +12,7 @@ module Setup() = struct
   let tst = Term.create()
   let (@->) l ret = Ty.Fun.mk l ret
   let ty_i = Ty.atomic_uninterpreted (ID.make "$i")
-  let ty_bool = Ty.bool
+  let ty_bool = Ty.bool ()
 
   let fun_f = Fun.mk_undef (ID.make "f") ([ty_i] @-> ty_i)
   let fun_g = Fun.mk_undef (ID.make "g") ([ty_i; ty_i] @-> ty_i)

src/msat-solver/Sidekick_msat_solver.ml

@@ -105,6 +105,7 @@ module Make(A : ARG)
     type ty = Ty.t
     type lit = Lit.t
     type term_state = Term.state
+    type ty_state = Ty.state
 
     type th_states =
       | Ths_nil
@@ -120,13 +121,16 @@ module Make(A : ARG)
     module Simplify = struct
       type t = {
         tst: term_state;
+        ty_st: ty_state;
         mutable hooks: hook list;
         cache: Term.t Term.Tbl.t;
       }
       and hook = t -> term -> term option
 
-      let create tst : t = {tst; hooks=[]; cache=Term.Tbl.create 32;}
+      let create tst ty_st : t =
+        {tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;}
       let[@inline] tst self = self.tst
+      let[@inline] ty_st self = self.ty_st
       let add_hook self f = self.hooks <- f :: self.hooks
       let clear self = Term.Tbl.clear self.cache
 
@@ -156,6 +160,7 @@ module Make(A : ARG)
 
     type t = {
       tst: Term.state; (** state for managing terms *)
+      ty_st: Ty.state;
       cc: CC.t lazy_t; (** congruence closure *)
       stat: Stat.t;
       count_axiom: int Stat.counter;
@@ -194,6 +199,7 @@ module Make(A : ARG)
 
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
+    let[@inline] ty_st t = t.ty_st
     let stats t = t.stat
 
     let simplifier self = self.simp
@@ -381,16 +387,17 @@ module Make(A : ARG)
       CC.mk_model (cc self) m
        *)
 
-    let create ~stat (tst:Term.state) () : t =
+    let create ~stat (tst:Term.state) (ty_st:Ty.state) () : t =
       let rec self = {
         tst;
+        ty_st;
         cc = lazy (
           (* lazily tie the knot *)
           CC.create ~size:`Big self.tst;
         );
         th_states=Ths_nil;
         stat;
-        simp=Simplify.create tst;
+        simp=Simplify.create tst ty_st;
         on_progress=(fun () -> ());
         preprocess=[];
         preprocess_cache=Term.Tbl.create 32;
@@ -467,9 +474,9 @@ module Make(A : ARG)
   let add_theory_l self = List.iter (add_theory self)
 
   (* create a new solver *)
-  let create ?(stat=Stat.global) ?size ?store_proof ~theories tst () : t =
+  let create ?(stat=Stat.global) ?size ?store_proof ~theories tst ty_st () : t =
     Log.debug 5 "msat-solver.create";
-    let si = Solver_internal.create ~stat tst () in
+    let si = Solver_internal.create ~stat tst ty_st () in
     let self = {
       si;
       solver=Sat_solver.create ?store_proof ?size si;

src/smtlib/Form.ml

@@ -32,7 +32,7 @@ let view_as_bool (t:T.t) : T.t bool_view =
   | _ -> B_atom t
 
 module Funs = struct
-  let get_ty _ _ = Ty.bool
+  let get_ty _ _ = Ty.bool()
 
   let abs ~self _a =
     match T.view self with

src/smtlib/Process.ml

@@ -320,11 +320,11 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let mk_bool = T.bool
   let view_as_lra t = match T.view t with
     | T.LRA l -> l
-    | T.Eq (a,b) when Ty.equal (T.ty a) Ty.real -> LRA_pred (Eq, a, b)
+    | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b)
     | _ -> LRA_other t
 
-  let ty_lra _st = Ty.real
+  let ty_lra _st = Ty.real()
-  let has_ty_real t = Ty.equal (T.ty t) Ty.real
+  let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
 
   module Gensym = struct
     type t = {

src/smtlib/Process.mli

@@ -6,6 +6,7 @@ module Solver
   : Sidekick_msat_solver.S with type T.Term.t = Term.t
                             and type T.Term.state = Term.state
                             and type T.Ty.t = Ty.t
+                            and type T.Ty.state = Ty.state
 
 val th_bool : Solver.theory
 val th_data : Solver.theory

src/smtlib/Typecheck.ml

@@ -77,7 +77,7 @@ let ill_typed ctx fmt =
   errorf_ctx ctx ("ill-typed: " ^^ fmt)
 
 let check_bool_ ctx t =
-  if not (Ty.equal (T.ty t) Ty.bool) then (
+  if not (Ty.equal (T.ty t) (Ty.bool())) then (
     ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t)
   )
 
@@ -87,8 +87,8 @@ let find_id_ ctx (s:string): ID.t * Ctx.kind =
 
 (* parse a type *)
 let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with
-  | PA.Ty_bool -> Ty.bool
+  | PA.Ty_bool -> Ty.bool()
-  | PA.Ty_real -> Ty.real
+  | PA.Ty_real -> Ty.real()
   | PA.Ty_app ("Int",[]) ->
     ill_typed ctx "cannot handle ints for now"
     (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *)

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -44,7 +44,7 @@ module type S = sig
 
   type state
 
-  val create : A.S.T.Term.state -> state
+  val create : A.S.T.Term.state -> A.S.T.Ty.state -> state
 
   val simplify : state -> A.S.Solver_internal.simplify_hook
   (** Simplify given term *)
@@ -64,13 +64,14 @@ module Make(A : ARG) : S with module A = A = struct
 
   type state = {
     tst: T.state;
+    ty_st: Ty.state;
     simps: T.t T.Tbl.t; (* cache *)
     cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
     gensym: A.Gensym.t;
   }
 
-  let create tst : state =
+  let create tst ty_st : state =
-    { tst; simps=T.Tbl.create 128;
+    { tst; ty_st; simps=T.Tbl.create 128;
       cnf=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
     }
@@ -129,7 +130,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
   let fresh_lit (self:state) ~mk_lit ~pre : Lit.t =
-    let t = fresh_term ~pre self Ty.bool in
+    let t = fresh_term ~pre self (Ty.bool self.ty_st) in
     mk_lit t
 
   (* preprocess "ite" away *)
@@ -243,7 +244,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   let create_and_setup si =
     Log.debug 2 "(th-bool.setup)";
-    let st = create (SI.tst si) in
+    let st = create (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
     SI.add_preprocess si (preproc_ite st);
     SI.add_preprocess si (cnf st);