package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file trace_tstp.ml

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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383

(* This file is free software, part of Logtk. See file "license" for more details. *)

(** {1 Trace of a TSTP prover} *)

open Logtk

type id = Ast_tptp.name

module T = STerm
module A = Ast_tptp
module Err = CCResult

type term = STerm.t
type form = STerm.t
type clause = term SLiteral.t list

type t =
  | Axiom of string * string (* filename, axiom name *)
  | Theory of string (* a theory used to do an inference *)
  | InferForm of form * step lazy_t
  | InferClause of clause * step lazy_t
and step = {
  id : id;
  rule : string;
  parents : t array;
  esa : bool;  (** Equisatisfiable step? *)
}

type proof = t

let equal p1 p2 = match p1, p2 with
  | Axiom (f1, n1), Axiom (f2, n2) -> f1 = f2 && n1 = n2
  | Theory s1, Theory s2 -> s1 = s2
  | InferForm (f1, lazy step1), InferForm(f2, lazy step2) ->
    step1.id = step2.id && T.equal f1 f2
  | InferClause (c1, lazy step1), InferClause(c2, lazy step2) ->
    begin try
        step1.id = step2.id && List.for_all2 (SLiteral.equal T.equal) c1 c2
      with Invalid_argument _ -> false
    end
  | _ -> false

let hash p = match p with
  | Axiom _
  | Theory _ -> Hashtbl.hash p
  | InferForm (_, lazy s)
  | InferClause (_, lazy s) -> Hashtbl.hash s.id

let compare p1 p2 = Pervasives.compare p1 p2  (* FIXME *)

(** {2 Constructors and utils} *)

let mk_f_axiom ~id f ~file ~name =
  let step = {id; rule="axiom"; parents = [| Axiom (file,name) |]; esa=false; } in
  InferForm (f, Lazy.from_val step)

let mk_c_axiom ~id c ~file ~name =
  let step = {id; rule="axiom"; parents = [| Axiom (file,name) |]; esa=false; } in
  InferClause (c, Lazy.from_val step)

let mk_f_step ?(esa=false) ~id f ~rule parents =
  assert(rule <> "axiom");
  let step = {id; rule; parents=Array.of_list parents; esa;} in
  InferForm (f, Lazy.from_val step)

let mk_c_step ?(esa=false) ~id c ~rule parents =
  assert(rule <> "axiom");
  let step = {id; rule; parents=Array.of_list parents; esa;} in
  InferClause (c, Lazy.from_val step)

let is_axiom = function
  | Axiom _ -> true
  | _ -> false

let is_theory = function
  | Theory _ -> true
  | _ -> false

let is_step = function
  | InferClause _
  | InferForm _ -> true
  | Axiom _
  | Theory _ -> false

let is_proof_of_false = function
  | InferForm (form, _) when T.equal form T.false_ -> true
  | InferClause([],_) -> true
  | InferClause(l,_) -> List.for_all SLiteral.is_false l
  | _ -> false

let get_id = function
  | InferClause (_, lazy step)
  | InferForm (_, lazy step) -> step.id
  | Axiom (_, name) -> A.NameString name
  | Theory _ -> invalid_arg "Trace_tstp: Theory does not have an ID"

let force = function
  | InferForm (_, step)
  | InferClause (_, step) -> ignore (Lazy.force step)
  | Axiom _
  | Theory _ -> ()

(** {2 Proof traversal} *)

module StepTbl = Hashtbl.Make(struct
    type t = proof
    let equal = equal
    let hash = hash
  end)

type proof_set = unit StepTbl.t

let is_dag proof =
  (* steps currently being explored *)
  let current = StepTbl.create 10 in
  (* steps totally explored *)
  let closed = StepTbl.create 10 in
  (* recursive DFS traversal *)
  let rec check_proof proof =
    if StepTbl.mem closed proof
    then ()  (* ok *)
    else if StepTbl.mem current proof
    then raise Exit  (* we followed a back link! *)
    else begin
      StepTbl.add current proof ();
      begin match proof with
        | InferClause (_, lazy step)
        | InferForm (_, lazy step) ->
          Array.iter check_proof step.parents
        | Axiom _
        | Theory _ -> ()
      end;
      (* proof is now totally explored *)
      StepTbl.remove current proof;
      StepTbl.add closed proof ();
    end
  in
  try
    check_proof proof;  (* check from root *)
    true
  with Exit ->
    false  (* loop detected *)

(** Traverse the proof. Each proof node is traversed only once. *)
let traverse ?(traversed=StepTbl.create 11) proof k =
  (* set of already traversed proof nodes; queue of proof nodes
     yet to traverse *)
  let queue = Queue.create () in
  Queue.push proof queue;
  while not (Queue.is_empty queue) do
    let proof = Queue.take queue in
    if StepTbl.mem traversed proof then ()
    else begin
      StepTbl.add traversed proof ();
      (* traverse premises first *)
      begin match proof with
        | Axiom _
        | Theory _ -> ()
        | InferForm (_, lazy step)
        | InferClause (_, lazy step) ->
          Array.iter (fun proof' -> Queue.push proof' queue) step.parents
      end;
      (* call [k] on the proof *)
      k proof;
    end
  done

let to_iter proof = Iter.from_iter (fun k -> traverse proof k)

(** Depth of a proof, ie max distance between the root and any axiom *)
let depth proof =
  let explored = StepTbl.create 11 in
  let depth = ref 0 in
  let q = Queue.create () in
  Queue.push (proof, 0) q;
  while not (Queue.is_empty q) do
    let (p, d) = Queue.pop q in
    if StepTbl.mem explored proof then () else begin
      StepTbl.add explored proof ();
      match p with
      | Axiom _ -> depth := max d !depth
      | Theory _ -> ()
      | InferForm(_, lazy step)
      | InferClause (_, lazy step) ->
        (* explore parents *)
        Array.iter (fun p -> Queue.push (p, d+1) q) step.parents
    end
  done;
  !depth

let size proof = Iter.length (to_iter proof)

(** {2 IO} *)

type 'a or_error = ('a, string) CCResult.t

let of_decls decls =
  let steps = Hashtbl.create 16 in (* maps names to steps *)
  let root = ref None in (* (one) root of proof *)
  (* find a proof name *)
  let find_step name =
    try
      Hashtbl.find steps name
    with Not_found ->
      failwith (CCFormat.sprintf "proof step %a not found in derivation" A.pp_name name)
  in
  (* read information about the source of the clause/formula *)
  let read_info info = match info with
    | A.GList [A.GString ("'proof'" | "proof")] -> `Proof
    | A.GNode("inference", [A.GString rule;
                            A.GList [A.GNode ("status", [A.GString status])];
                            A.GList parents]) ->
      (* lazily lookup parent steps by their name in the derivation *)
      let parents = lazy
        (Array.map
           (fun data -> match data with
              | A.GInt i -> find_step (A.NameInt i)
              | A.GString s -> find_step (A.NameString s)
              | A.GNode ("theory", [A.GString th]) -> Theory th
              | _ -> failwith (CCFormat.sprintf "not a valid parent: %a" A.pp_general data))
           (Array.of_list parents))
      in
      let esa = status <> "thm" in
      `Parents (rule, esa, parents)
    | A.GNode ("file", (A.GString file :: A.GString name :: _)) ->
      let parents = Lazy.from_val [|(Axiom (file,name))|] in
      `Parents ("axiom", false, parents)
    | A.GNode ("trivial", _) ->
      `Parents ("trivial", false, Lazy.from_val [||])
    | A.GInt i ->
      let parent = find_step (A.NameInt i) in
      `Parents ("trivial", false, Lazy.from_val [|parent|])
    | A.GString s ->
      let parent = find_step (A.NameString s) in
      `Parents ("trivial", false, Lazy.from_val [|parent|])
    | _ ->
      Util.debugf 1 "not a valid proof step: %a" (fun k->k A.pp_general_debugf info);
      `NoIdea
  in
  (* what to do if a step is read *)
  let add_step id step = match step with
    | InferForm _
    | InferClause _ ->
      if is_proof_of_false step && !root = None
      then root := Some step;
      Util.debugf 3 "add step %a (root? %B)" (fun k->k A.pp_name id (is_proof_of_false step));
      Hashtbl.replace steps id step;
    | Axiom _
    | Theory _ -> ()
  in
  (* traverse declarations *)
  Iter.iter
    begin fun decl -> match decl with
      | A.CNF (_name, _role, _c, info :: _) ->
        Util.debugf 3 "@[<2>convert step@ @[%a@]@]" (fun k->k (A.pp T.pp) decl);
        begin match read_info info with
          | `Proof
          | `NoIdea -> ()
          | `Parents (_rule, _esa, _parents) ->
            assert false
            (* FIXME
               let step = lazy {id=name; esa; rule; parents=Lazy.force parents} in
               let c = List.map SLiteral.of_form c in
               let p = InferClause (c, step) in
               add_step name p
            *)
        end
      | A.FOF(name, _role, f, info :: _)
      | A.TFF (name, _role, f, info :: _) ->
        Util.debugf 3 "convert step %a" (fun k->k (A.pp T.pp) decl);
        begin match read_info info with
          | `Proof
          | `NoIdea -> ()
          | `Parents (rule, esa, parents) ->
            let step = lazy{id=name; esa; rule; parents=Lazy.force parents} in
            let p = InferForm (f, step) in
            add_step name p
        end
      | A.TypeDecl _
      | A.FOF _
      | A.CNF _
      | A.TFF _
      | A.THF _
      | A.Include _
      | A.IncludeOnly _
      | A.NewType _ -> ()
    end
    decls;
  match !root with
  | None -> Err.fail "could not find the root of the TSTP proof"
  | Some p ->
    try
      (* force proofs to trigger errors here *)
      traverse p force;
      Err.return p
    with Failure msg -> Err.fail msg

let parse ?(recursive=true) filename =
  Err.(
    Util_tptp.parse_file ~recursive filename
    >>= fun decls ->
    Util.debugf 1 "@[<2>decls:@ @[<hv>%a@]@]"
      (fun k->k (Util.pp_iter ~sep:"" (A.pp T.pp)) decls);
    of_decls decls
  )

let _extract_axiom proof = match proof with
  | Axiom (f,n) -> f,n
  | _ -> assert false

let _pp_clause out c = match c with
  | [] -> T.pp out T.false_
  | _ ->
    Format.fprintf out "@[%a@]"
      (Util.pp_list ~sep:" | " (SLiteral.pp T.pp)) c

let _print_parent p = match p with
  | InferForm _
  | InferClause _ -> CCFormat.to_string A.pp_name (get_id  p)
  | Theory s -> CCFormat.sprintf "theory(%s)" s
  | Axiom (f,n) -> CCFormat.sprintf "file('%s', %s)" f n

(* pure fof? (no types but $i/$o) *)
let _form_is_fof _f = false (* FIXME *)

let pp_tstp out proof =
  traverse proof
    (fun p ->
       match p with
       | Axiom _ -> ()
       | Theory s -> CCFormat.fprintf out "theory(%s)" s
       | InferClause(c, lazy ({rule="axiom";_} as step)) when is_axiom step.parents.(0)->
         let id = get_id p in
         let f,n = _extract_axiom step.parents.(0) in
         Format.fprintf out "cnf(%a, axiom, (%a), file('%s', %s)).\n"
           A.pp_name id _pp_clause c f n
       | InferForm(f, lazy ({rule="axiom"; _} as step)) when is_axiom step.parents.(0)->
         let id = get_id p in
         let file,n = _extract_axiom step.parents.(0) in
         Format.fprintf out "tff(%a, axiom, %a, file('%s', %s)).\n"
           A.pp_name id T.pp f file n
       | InferForm(f, lazy step) ->
         let id = get_id p in
         let ids = Array.map _print_parent step.parents in
         let status = if step.esa then "esa" else "thm" in
         let kind = if _form_is_fof f then "fof" else "tff" in
         Format.fprintf out
           "%s(%a, plain, %a, inference('%s', [status(%s)], [%a])).\n"
           kind A.pp_name id T.pp (T.close_all Binder.Forall f) step.rule status
           (CCFormat.array CCFormat.string) ids
       | InferClause(c, lazy step) ->
         let id = get_id p in
         let ids = Array.map _print_parent step.parents in
         let status = if step.esa then "esa" else "thm" in
         Format.fprintf out
           "cnf(%a, plain, %a, inference('%s', [status(%s)], [%a])).\n"
           A.pp_name id _pp_clause c step.rule status
           (CCFormat.array CCFormat.string) ids
    )

let pp0 out proof = match proof with
  | Axiom (f,n) -> Format.fprintf out "axiom(%s, %s)" f n
  | Theory s -> Format.fprintf out "theory(%s)" s
  | InferClause (c, _) ->
    Format.fprintf out "proof for %a (id %a)" _pp_clause c A.pp_name (get_id proof)
  | InferForm (f, _) ->
    Format.fprintf out "proof for %a (id %a)" T.pp f A.pp_name (get_id proof)

let pp1 out proof = match proof with
  | Axiom (f,n) -> Format.fprintf out "axiom(%s, %s)" f n
  | Theory s -> Format.fprintf out "theory(%s)" s
  | InferClause (c, lazy step) ->
    Format.fprintf out "proof for %a (id %a) from\n  %a"
      _pp_clause c A.pp_name (get_id proof)
      CCFormat.(array ~sep:(return "@.  ") pp0) step.parents
  | InferForm (f, lazy step) ->
    Format.fprintf out "proof for %a (id %a) from\n %a"
      T.pp f A.pp_name (get_id proof)
      CCFormat.(array ~sep:(return "@.  ") pp0) step.parents

let pp = pp0
let to_string = CCFormat.to_string pp
OCaml

Innovation. Community. Security.