Add mlis for Symbolic_choice_with(out)_memory modules

src/cmd/cmd_sym.ml

@@ -109,7 +109,6 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     else results
   in
   let* count = print_and_count_failures 0 results in
-  Format.pp_std "completed paths: %d@." !path_counter;
   if count > 0 then Error (`Found_bug count)
   else begin
     Fmt.pr "All OK";

src/intf/thread_intf.ml

@@ -52,20 +52,11 @@ module type S = sig
   val incr_symbols : t -> t
 end
 
-module type S_with_memory =
-  S with type Memory.collection = Symbolic_memory.collection
-
-module type S_without_memory = S with type Memory.collection = bool
-
 module type Intf = sig
   module type M = M
 
   module type S = S
 
-  module type S_with_memory = S_with_memory
-
-  module type S_without_memory = S_without_memory
-
   module Make (Symbolic_memory : M) :
     S with type Memory.collection = Symbolic_memory.collection
 end

src/symbolic/symbolic.ml

@@ -3,7 +3,7 @@
 (* Written by the Owi programmers *)
 
 module MakeP
-    (Thread : Thread.S_with_memory)
+    (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection)
     (Choice : Choice_intf.Complete
                 with module V := Symbolic_value
                  and type thread := Thread.t) =

src/symbolic/symbolic_choice.ml

@@ -225,10 +225,10 @@ module CoreImpl = struct
       other =
       St
         (fun st ->
-          let ( let* ) = M.( let* ) in
+          let ( let+ ) = M.( let+ ) in
           let proj, backup = project_and_backup st in
-          let* res, new_state = run other proj in
-          M.return (res, restore backup new_state) )
+          let+ res, new_state = run other proj in
+          (res, restore backup new_state) )
   end
 
   module Eval = struct
@@ -274,7 +274,9 @@ module CoreImpl = struct
   end
 
   (*  *)
-  module Make (Thread : Thread.S) = struct
+  module Make (Thread : Thread.S) :
+    S with type thread := Thread.t and type 'a t = ('a, Thread.t) Eval.t =
+  struct
     include Eval
 
     type 'a t = ('a, Thread.t) Eval.t
@@ -343,7 +345,6 @@ end
     We can now use CoreImpl only through its exposed signature which
     maintains all invariants.
   *)
-(* module CoreImpl' : S = CoreImpl *)
 
 module Make (Thread : Thread.S) = struct
   include CoreImpl.Make (Thread)

src/symbolic/symbolic_choice_with_memory.ml

@@ -1,3 +1,7 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
 include Symbolic_choice.Make (Thread_with_memory)
 
 let lift_mem (mem_op : 'a Symbolic_choice_without_memory.t) : 'a t =

src/symbolic/.symbolic_choice.mli → src/symbolic/symbolic_choice_with_memory.mli

@@ -9,8 +9,7 @@ type 'a eval = private
 
 include
   Choice_intf.Complete
-    with type thread := Thread.t
-     and type 'a run_result = ('a eval * Thread.t) Seq.t
+    with type thread := Thread_with_memory.t
      and module V := Symbolic_value
 
 val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
@@ -19,8 +18,8 @@ val run :
      workers:int
   -> Smtml.Solver_dispatcher.solver_type
   -> 'a t
-  -> Thread.t
-  -> callback:('a eval * Thread.t -> unit)
+  -> Thread_with_memory.t
+  -> callback:('a eval * Thread_with_memory.t -> unit)
   -> callback_init:(unit -> unit)
   -> callback_end:(unit -> unit)
   -> unit Domain.t array

src/symbolic/symbolic_choice_without_memory.ml

@@ -1 +1,5 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
 include Symbolic_choice.Make (Thread_without_memory)

src/symbolic/symbolic_choice_without_memory.mli

@@ -0,0 +1,42 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type 'a eval = private
+  | EVal of 'a
+  | ETrap of Trap.t * Smtml.Model.t
+  | EAssert of Smtml.Expr.t * Smtml.Model.t
+
+type 'a t = ('a, Thread_without_memory.t) Symbolic_choice.CoreImpl.Eval.t
+
+type thread := Thread_without_memory.t
+
+module V := Symbolic_value
+
+type 'a run_result
+
+val return : 'a -> 'a t
+
+val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+val map : 'a t -> ('a -> 'b) -> 'b t
+
+val select : V.vbool -> bool t
+
+val select_i32 : V.int32 -> Int32.t t
+
+val trap : Trap.t -> 'a t
+
+val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+val assertion : V.vbool -> unit t
+
+val with_thread : (thread -> 'b) -> 'b t
+
+val solver : Solver.t t
+
+val thread : thread t
+
+val add_pc : V.vbool -> unit t

src/symbolic/thread_with_memory.mli

@@ -3,7 +3,7 @@
 (* Written by the Owi programmers *)
 
 (** @inline *)
-include Thread.S_with_memory
+include Thread.S with type Memory.collection = Symbolic_memory.collection
 
 val project : t -> Thread_without_memory.t * Memory.collection
 

src/symbolic/thread_without_memory.mli

@@ -3,4 +3,4 @@
 (* Written by the Owi programmers *)
 
 (** @inline *)
-include Thread.S_without_memory
+include Thread.S with type Memory.collection = bool