Add mlis for Symbolic_choice_with(out)_memory modules

src/cmd/cmd_sym.ml

@@ -126,7 +126,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
     Format.pp_std "All OK";

src/symbolic/symbolic_choice.ml

@@ -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.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.mli

@@ -0,0 +1,38 @@
+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