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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2026 OCamlPro *)
(* Written by the Owi programmers *)
type trap =
{ err : Result.err
; model : Smtml.Model.t
; state : Thread.t
}
type assertion =
{ assertion : Symbolic_boolean.t
; model : Smtml.Model.t
; state : Thread.t
}
type t =
[ `Trap of trap
| `Assertion of assertion
| `Prune
]
let is_trap = function `Assertion _ | `Prune -> false | `Trap _ -> true
let is_assertion = function `Assertion _ -> true | `Prune | `Trap _ -> false
let is_prune = function `Prune -> true | `Assertion _ | `Trap _ -> false
let get_state : [ `Trap of trap | `Assertion of assertion ] -> Thread.t =
function
| `Trap { state; _ } | `Assertion { state; _ } -> state
let get_model : [ `Trap of trap | `Assertion of assertion ] -> Smtml.Model.t =
function
| `Trap { model; _ } | `Assertion { model; _ } -> model
let compare_breadcrumbs (bug1 : [ `Trap of trap | `Assertion of assertion ])
(bug2 : [ `Trap of trap | `Assertion of assertion ]) =
let s1 = get_state bug1 in
let s2 = get_state bug2 in
let breadcrumbs1 = List.rev @@ s1.breadcrumbs in
let breadcrumbs2 = List.rev @@ s2.breadcrumbs in
List.compare compare breadcrumbs1 breadcrumbs2
let sort_seq_if b (seq : [ `Trap of trap | `Assertion of assertion ] Seq.t) =
if b then List.of_seq seq |> List.sort compare_breadcrumbs |> List.to_seq
else seq