feat(core): add Gensym module, add Proof_trace.close

src/core/Sidekick_core.ml

@@ -24,6 +24,8 @@ module Term = struct
   include T_printer
 end
 
+module Gensym = Gensym
+
 (** {2 view} *)
 
 module Bool_view = Bool_view

src/core/gensym.ml

@@ -0,0 +1,48 @@
+open Sidekick_core_logic
+
+type term = Term.t
+type ty = Term.t
+
+type Const.view +=
+  | Fresh of {
+      id: int;  (** Id of this constant *)
+      gensym_id: int;  (** Id of the gensym *)
+      pre: string;  (** Printing prefix *)
+      ty: ty;
+    }
+
+let ops =
+  (module struct
+    let equal a b =
+      match a, b with
+      | Fresh a, Fresh b -> a.id = b.id && a.gensym_id = b.gensym_id
+      | _ -> false
+
+    let hash = function
+      | Fresh { id; gensym_id; _ } ->
+        Hash.combine3 15232 (Hash.int id) (Hash.int gensym_id)
+      | _ -> assert false
+
+    let pp out = function
+      | Fresh { id; pre; _ } -> Fmt.fprintf out "$%s[%d]" pre id
+      | _ -> assert false
+  end : Const.DYN_OPS)
+
+type t = { tst: Term.store; self_id: int; mutable fresh: int }
+
+(* TODO: use atomic *)
+let id_ = ref 0
+
+let create tst : t =
+  let self_id = !id_ in
+  incr id_;
+  { tst; self_id; fresh = 0 }
+
+let fresh_term (self : t) ~pre (ty : ty) : Term.t =
+  let id = self.fresh in
+  self.fresh <- 1 + self.fresh;
+  let c =
+    Term.const self.tst
+    @@ Const.make (Fresh { id; gensym_id = self.self_id; pre; ty }) ops ~ty
+  in
+  c

src/core/gensym.mli

@@ -0,0 +1,19 @@
+(** Fresh symbol generation *)
+
+open Sidekick_core_logic
+
+type term = Term.t
+type ty = Term.t
+
+type t
+(** Fresh symbol generator.
+
+      The theory needs to be able to create new terms with fresh names,
+      to be used as placeholders for complex formulas during Tseitin
+      encoding. *)
+
+val create : Term.store -> t
+(** New (stateful) generator instance. *)
+
+val fresh_term : t -> pre:string -> ty -> term
+(** Make a fresh term of the given type *)

src/core/proof_term.ml

@@ -10,6 +10,7 @@ type rule_apply = {
   term_args: Term.t list;
   subst_args: Subst.t list;
   premises: step_id list;
+  indices: int list;
 }
 
 type t =
@@ -31,7 +32,7 @@ let let_ bs r =
   | _ -> P_let (bs, r)
 
 let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
-    rule_name : t =
+    ?(indices = []) rule_name : t =
   P_apply
     {
       rule_name;
@@ -39,4 +40,5 @@ let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
       subst_args = substs;
       term_args = terms;
       premises;
+      indices;
     }

src/core/proof_term.mli

@@ -14,6 +14,7 @@ type rule_apply = {
   term_args: Term.t list;
   subst_args: Subst.t list;
   premises: step_id list;
+  indices: int list;
 }
 
 type t =
@@ -35,5 +36,6 @@ val apply_rule :
   ?terms:Term.t list ->
   ?substs:Subst.t list ->
   ?premises:step_id list ->
+  ?indices:int list ->
   string ->
   t

src/core/proof_trace.ml

@@ -28,6 +28,7 @@ module type DYN = sig
   val add_step : Proof_term.delayed -> step_id
   val add_unsat : step_id -> unit
   val delete : step_id -> unit
+  val close : unit -> unit
 end
 
 type t = (module DYN)
@@ -36,6 +37,7 @@ let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled ()
 let[@inline] add_step ((module Tr) : t) rule : step_id = Tr.add_step rule
 let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s
 let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s
+let[@inline] close ((module Tr) : t) : unit = Tr.close ()
 let make (d : (module DYN)) : t = d
 let dummy_step_id : step_id = -1l
 
@@ -45,4 +47,5 @@ let dummy : t =
     let add_step _ = dummy_step_id
     let add_unsat _ = ()
     let delete _ = ()
+    let close _ = ()
   end)

src/core/proof_trace.mli

@@ -42,6 +42,9 @@ val delete : t -> step_id -> unit
 (** Forget a step that won't be used in the rest of the trace.
     Only useful for performance/memory considerations. *)
 
+val close : t -> unit
+(** [close p] closes the proof, and can dispose of underlying resources *)
+
 (** {2 Dummy backend} *)
 
 val dummy_step_id : step_id
@@ -58,6 +61,7 @@ module type DYN = sig
   val add_step : Proof_term.delayed -> step_id
   val add_unsat : step_id -> unit
   val delete : step_id -> unit
+  val close : unit -> unit
 end
 
 val make : (module DYN) -> t