1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
type 'a eval =
| EVal of 'a
| ETrap of
Result.err
* Smtml.Model.t
* (int * string) list
* int list
* Symbol_scope.t
| EAssert of
Smtml.Expr.t
* Smtml.Model.t
* (int * string) list
* int list
* Symbol_scope.t
module type S = sig
module V : Func_intf.Value_types
type thread
type 'a t
val return : 'a -> 'a t
val stop : 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
val map : 'a t -> ('a -> 'b) -> 'b t
val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
val trap : Result.err -> 'a t
val select : V.bool -> Bool.t t
val select_i32 : V.int32 -> Int32.t t
val assertion : V.bool -> unit t
val with_thread : (thread -> 'a) -> 'a t
val with_new_invisible_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val solver : Solver.t t
val thread : thread t
val add_pc : V.bool -> unit t
val get_pc : unit -> Smtml.Expr.Set.t t
val add_label : int * string -> unit t
val open_scope : string -> unit t
val close_scope : unit -> unit t
type 'a run_result = ('a eval * thread) Seq.t
val run :
workers:int
-> Smtml.Solver_type.t
-> 'a t
-> thread
-> callback:('a eval * thread -> unit)
-> callback_init:(unit -> unit)
-> callback_end:(unit -> unit)
-> unit Domain.t array
end
module type Intf = sig
module type S = S
module CoreImpl : sig
(* The core implementation of the monad. It is isolated in a module to *)
(* restict its exposed interface and maintain its invariant. *)
module State : sig
type ('a, 's) t
val project_state :
('st1 -> 'st2 * 'backup)
-> ('backup -> 'st2 -> 'st1)
-> ('a, 'st2) t
-> ('a, 'st1) t
end
end
module Make (Thread : Thread_intf.S) :
S
with type 'a t = ('a eval, Thread.t) CoreImpl.State.t
and type thread := Thread.t
and module V := Symbolic_value
end