wip: feat(base): proof chunk storage

src/base/Chunk_stack.ml

@@ -0,0 +1,112 @@
+
+module Buf = struct
+  type t = {
+    mutable b: bytes;
+    mutable len: int;
+  }
+
+  let create ?(cap=16) () : t =
+    { len=0; b=Bytes.create cap; }
+
+  let ensure_size_ (self:t) (new_len:int) : unit =
+    if new_len > Bytes.length self.b then (
+      let size = min (new_len + new_len / 4 + 5) Sys.max_string_length in
+      if new_len > size then failwith "max buf size exceeded";
+
+      let b2 = Bytes.create size in
+      Bytes.blit self.b 0 b2 0 self.len;
+      self.b <- b2
+    )
+
+  let add_bytes (self:t) (b:bytes) (off:int) (len:int) =
+    ensure_size_ self (self.len + len);
+    Bytes.blit self.b self.len b off len;
+    self.len <- self.len + len
+
+  let[@inline] add_buf (self:t) (other:t) =
+    add_bytes self other.b 0 other.len
+
+  let clear self = self.len <- 0
+
+  let contents self = Bytes.sub_string self.b 0 self.len
+end
+
+module Writer = struct
+  type t = {
+    write: Buf.t -> unit;
+  }
+
+  let nop_ _ = ()
+
+  let dummy : t = { write=nop_; }
+
+  let into_buf (into:Buf.t) : t =
+    let blen = Bytes.create 4 in
+    let write buf =
+      Buf.add_buf into buf;
+      (* add len *)
+      Bytes.set_int32_le blen 0 (Int32.of_int buf.Buf.len);
+      Buf.add_bytes into blen 0 4;
+    in
+    { write; }
+
+  let into_channel (oc:out_channel) : t =
+    let blen = Bytes.create 4 in
+    let write buf =
+      output oc buf.Buf.b 0 buf.Buf.len;
+      (* add len *)
+      Bytes.set_int32_le blen 0 (Int32.of_int buf.Buf.len);
+      output oc blen 0 4
+    in
+    { write; }
+end
+
+module Reader = struct
+  type t = {
+    read: Buf.t -> bool;
+  }
+
+  let[@inline] next (self:t) buf : bool = self.read buf
+
+  let empty : t = { read=fun _ -> false }
+
+  let from_buf (buf:Buf.t) : t =
+    assert false (* TODO *)
+
+  let with_file_backward (filename:string) f =
+    CCIO.with_in ~flags:[Open_binary; Open_rdonly] filename @@ fun ic ->
+
+    let len = in_channel_length ic in
+    seek_in ic len;
+
+    (* read length *)
+    let blen = Bytes.create 4 in
+
+    let read buf : bool =
+      let pos = pos_in ic in
+      if pos > 0 then (
+        (* read length of preceding chunk *)
+        assert (pos>=4);
+        seek_in ic (pos - 4);
+
+        really_input ic blen 0 4;
+        let chunk_len = Int32.to_int (Bytes.get_int32_le blen 0) in
+        Printf.printf "read chunk of len %d\n%!" chunk_len;
+
+        (* now read chunk *)
+        Buf.ensure_size_ buf chunk_len;
+        seek_in ic (pos - 4 - chunk_len);
+        really_input ic buf.Buf.b 0 chunk_len;
+        buf.Buf.len <- chunk_len;
+
+        true
+      ) else (
+        false
+      )
+    in
+    f {read}
+end
+
+(*$T
+    false
+    *)

src/base/Chunk_stack.mli

@@ -0,0 +1,56 @@
+
+(** Manage a list of chunks.
+
+    A chunk is used for serializing proof traces, possibly on disk.
+    This way we do not have to keep the whole proof in memory.
+    Each chunk is typically one step of the proof search.
+
+    We produce chunks in forward order (chronological order of their discovery),
+    but once we find a proof of "false", we work our way backward to find
+    chunks transitively needed by this proof of false.
+    Once we obtain this subset of the chunks (as a graph in memory) we can
+    emit a proper proof with no redundant information.
+*)
+
+(** A hand made buffer *)
+module Buf : sig
+  type t = {
+    mutable b: bytes;
+    mutable len: int;
+  }
+
+  val create : ?cap:int -> unit -> t
+
+  val clear : t -> unit
+
+  val contents : t -> string
+end
+
+(** Create a stack of chunks. *)
+module Writer : sig
+  type t
+
+  val dummy : t
+
+  val into_buf : Buf.t -> t
+
+  val into_channel: out_channel -> t
+end
+
+module Reader : sig
+  type t
+
+  val next : t -> Buf.t -> bool
+  (** Read next chunk into buf.
+      Returns [true] if a chunk was read, [false] if no more chunks are there.  *)
+
+  val empty : t
+
+  val from_buf : Buf.t -> t
+
+  (** [read_file_backward filename f] calls [f] with an iterator
+      over chunks of the file, read from the end.
+
+      Each chunk is assumed to be followed by its length as an int32 LE. *)
+  val with_file_backward : string -> (t -> 'a) -> 'a
+end

src/base/dune

@@ -2,7 +2,7 @@
  (name sidekick_base)
  (public_name sidekick-base)
  (synopsis "Base term definitions for the standalone SMT solver and library")
- (libraries containers sidekick.core sidekick.util sidekick.lit
+ (libraries containers iter sidekick.core sidekick.util sidekick.lit
             sidekick.arith-lra sidekick.th-bool-static sidekick.th-data
             sidekick.zarith
             zarith)