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
open Solver_types
type t = premise
let prefix p = match p with
| Hyp -> "H"
| Lemma _ -> "T"
| Simplify _ | P_raw_steps _ | P_steps _ -> "L"
| _ -> "C"
let[@inline] pp_clause_name out { c_name=s; c_premise=p; _ } =
Format.fprintf out "%s%d" (prefix p) s
let[@inline] pp_term_id out {t_id;_} = Fmt.int out t_id
let[@inline] atom_is_pos (a:atom) : bool = match a.a_term.t_var with
| Var_bool { pa; _ } -> a==pa
| Var_none | Var_semantic _ -> assert false
let[@inline] pp_atom_id out a =
Fmt.fprintf out "%s%d" (if atom_is_pos a then "+" else "-") a.a_term.t_id
let[@inline] raw_steps l : t =
assert (match l with []|[_] -> false | _ -> true);
P_raw_steps l
let[@inline] raw_steps_or_simplify l = match l with
| [c] -> Simplify c
| [] -> assert false
| _ -> P_raw_steps l
let[@inline] steps init steps =
assert (steps<>[]);
P_steps {init;steps}
let[@inline] pp_raw_premise_step out c = pp_clause_name out c
let[@inline] pp_premise_step out = function
| Step_resolve {c;_} -> pp_clause_name out c
let pp out = function
| Hyp -> Format.fprintf out "hyp"
| Local -> Format.fprintf out "local"
| Lemma l ->
Format.fprintf out "@[th_lemma@ %a@]" Lemma.pp l
| Simplify c -> Format.fprintf out "simpl %a" pp_clause_name c
| P_raw_steps l ->
Fmt.fprintf out "steps{@[%a@]}"
(Util.pp_list ~sep:"," pp_raw_premise_step) l
| P_steps {init;steps} ->
Format.fprintf out "hyper_res{@[%a;@,%a@]}"
pp_clause_name init (Util.pp_list ~sep:";" pp_premise_step) steps