Source file phases_impl.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
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
(** {1 Implementation of Phases} *)
open Logtk
open Logtk_parsers
open Logtk_proofs
open Libzipperposition
open Libzipperposition_calculi
open Phases.Infix
module T = Term
module O = Ordering
module Lit = Literal
let section = Const.section
let _db_w = ref 1
let _lmb_w = ref 1
let _kbo_wf = ref "invfreqrank"
let _lift_lambdas = ref false
let setup_alarm timeout =
let handler _ =
Format.printf "%% SZS status ResourceOut@.";
exit 0
in
ignore (Sys.signal Sys.sigalrm (Sys.Signal_handle handler));
Unix.alarm (max 1 (int_of_float timeout))
let print_version ~params =
if params.Params.version then (
Format.printf "zipperposition %s@." Const.version;
exit 0
)
let load_extensions =
let open Libzipperposition_calculi in
Phases.start_phase Phases.LoadExtensions >>= fun () ->
Extensions.register Superposition.extension;
Extensions.register AC.extension;
Extensions.register Heuristics.extension;
Extensions.register Avatar.extension;
Extensions.register EnumTypes.extension;
Extensions.register Induction.extension;
Extensions.register Rewriting.extension;
Extensions.register Arith_int.extension;
Extensions.register Arith_rat.extension;
Extensions.register Ind_types.extension;
Extensions.register Fool.extension;
Extensions.register Booleans.extension;
Extensions.register Higher_order.extension;
Extensions.register App_encode.extension;
let l = Extensions.extensions () in
Phases.return_phase l
let do_extensions ~x ~field =
Extensions.extensions ()
|> Phases.fold_l ~x:()
~f:(fun () e ->
Phases.fold_l (field e) ~x:()
~f:(fun () f -> Phases.update ~f:(f x)))
let apply_modifiers ~field o =
Extensions.extensions ()
|> CCList.fold_left (fun o e -> field e |> CCList.fold_left (fun o m -> m o) o) o
let start_file file =
Phases.start_phase Phases.Start_file >>= fun () ->
Util.debugf ~section 1 "@[@{<Yellow>### process file@ `%s` ###@}@]"
(fun k->k file);
do_extensions ~field:(fun e -> e.Extensions.start_file_actions)
~x:file >>= fun () ->
Phases.return_phase ()
let parse_prelude (params:Params.t) =
Phases.start_phase Phases.Parse_prelude >>= fun () ->
let prelude_files = params.Params.prelude in
let res =
if CCVector.is_empty prelude_files
then CCResult.return Iter.empty
else (
CCVector.to_list prelude_files
|> CCResult.map_l
(fun file ->
Util.debugf ~section 1 "@[@{<Yellow>### parse prelude file@ `%s` ###@}@]"
(fun k->k file);
let fmt = Parsing_utils.guess_input file in
Parsing_utils.parse_file fmt file)
|> CCResult.map Iter.of_list
|> CCResult.map Iter.flatten
)
in
Phases.return_phase_err res
let parse_file file =
Phases.start_phase Phases.Parse_file >>= fun () ->
let input = Parsing_utils.input_of_file file in
Parsing_utils.parse_file input file >>?= fun parsed ->
do_extensions ~field:(fun e -> e.Extensions.post_parse_actions)
~x:parsed >>= fun () ->
Phases.return_phase (input,parsed)
let typing ~file prelude (input,stmts) =
Phases.start_phase Phases.Typing >>= fun () ->
Phases.get_key Params.key >>= fun params ->
let def_as_rewrite = params.Params.def_as_rewrite in
TypeInference.infer_statements
~on_var:(Input_format.on_var input)
~on_undef:(Input_format.on_undef_id input)
~on_shadow:(Input_format.on_shadow input)
~implicit_ty_args:(Input_format.implicit_ty_args input)
~def_as_rewrite ?ctx:None ~file
(Iter.append prelude stmts)
>>?= fun stmts ->
Util.debugf ~section 3 "@[<hv2>@{<green>typed statements@}@ %a@]"
(fun k->k (Util.pp_seq Statement.pp_input) (CCVector.to_seq stmts));
do_extensions ~field:(fun e -> e.Extensions.post_typing_actions)
~x:stmts >>= fun () ->
Phases.return_phase stmts
let cnf ~sk_ctx decls =
Phases.start_phase Phases.CNF >>= fun () ->
let stmts =
decls
|> CCVector.to_seq
|> (if not !_lift_lambdas then CCFun.id
else Iter.flat_map Statement.lift_lambdas)
|> Cnf.cnf_of_seq ~ctx:sk_ctx
|> CCVector.to_seq
|> apply_modifiers ~field:(fun e -> e.Extensions.post_cnf_modifiers)
|> Cnf.convert
in
do_extensions ~field:(fun e -> e.Extensions.post_cnf_actions)
~x:stmts >>= fun () ->
Phases.return_phase stmts
let compute_prec ~signature stmts =
Phases.start_phase Phases.Compute_prec >>= fun () ->
Phases.get >>= fun state ->
let cp =
Extensions.extensions ()
|> List.fold_left
(fun cp e -> List.fold_left (fun cp f -> f state cp) cp e.Extensions.prec_actions)
Compute_prec.empty
|> Compute_prec.add_constr 10 Classify_cst.prec_constr
|> Compute_prec.set_weight_rule (
fun stmts ->
let sym_depth =
stmts
|> Iter.flat_map Statement.Seq.terms
|> Iter.flat_map (fun t -> Term.Seq.subterms_depth t
|> Iter.filter_map (fun (st,d) ->
CCOpt.map (fun id -> (id,d)) (Term.head st))) in
Precedence.weight_fun_of_string ~signature !_kbo_wf sym_depth)
|> Compute_prec.add_constr_rule 90
(fun seq ->
seq
|> Iter.flat_map Statement.Seq.terms
|> Iter.flat_map Term.Seq.symbols
|> Precedence.Constr.invfreq)
in
let prec = Compute_prec.mk_precedence ~db_w:!_db_w ~lmb_w:!_lmb_w cp stmts in
Phases.return_phase prec
let compute_ord_select precedence =
Phases.start_phase Phases.Compute_ord_select >>= fun () ->
Phases.get_key Params.key >>= fun params ->
let ord = Ordering.by_name params.Params.ord precedence in
Util.debugf ~section 2 "@[<2>ordering %s@]" (fun k->k (Ordering.name ord));
let select = Selection.from_string ~ord params.Params.select in
do_extensions ~field:(fun e->e.Extensions.ord_select_actions)
~x:(ord,select) >>= fun () ->
Util.debugf ~section 2 "@[<2>selection function:@ %s@]" (fun k->k params.Params.select);
Phases.return_phase (ord, select)
let make_ctx ~signature ~ord ~select ~eta ~sk_ctx () =
Phases.start_phase Phases.MakeCtx >>= fun () ->
let module Res = struct
let signature = signature
let ord = ord
let select = select
let eta = eta
let sk_ctx = sk_ctx
end in
let module MyCtx = Ctx.Make(Res) in
let ctx = (module MyCtx : Ctx_intf.S) in
Phases.get >>= fun st ->
let lost_comp = Flex_state.get_or ~or_:false Ctx.Key.lost_completeness st in
if lost_comp then MyCtx.lost_completeness ();
do_extensions ~field:(fun e->e.Extensions.ctx_actions)
~x:ctx >>= fun () ->
Phases.return_phase ctx
let make_env ~ctx:(module Ctx : Ctx_intf.S) ~params stmts =
Phases.start_phase Phases.MakeEnv >>= fun () ->
Phases.get >>= fun state ->
let module MyEnv = Env.Make(struct
module Ctx = Ctx
let params = params
let flex_state = state
end) in
let env1 = (module MyEnv : Env.S) in
Extensions.extensions ()
|> List.iter
(fun e -> List.iter (fun f -> f env1) e.Extensions.env_actions);
let c_sets = MyEnv.convert_input_statements stmts in
let env2 = (module MyEnv : Env.S with type C.t = MyEnv.C.t) in
Phases.return_phase (Phases.Env_clauses (env2, c_sets))
let has_goal_ = ref false
let print_stats_env (type c) (module Env : Env.S with type C.t = c) =
let = Options.comment() in
let print_hashcons_stats what (sz, num, sum_length, small, median, big) =
Format.printf
"@[<h>%shashcons stats for %s: size %d, num %d, sum length %d, \
buckets: small %d, median %d, big %d@]@."
comment what sz num sum_length small median big
and print_state_stats (num_active, num_passive, num_simpl) =
Format.printf "%sproof state stats: {active %d, passive %d, simpl %d}@."
comment num_active num_passive num_simpl;
in
if Env.params.Params.stats then (
print_hashcons_stats "terms" (InnerTerm.hashcons_stats ());
print_state_stats (Env.stats ());
)
let print_stats () =
Phases.start_phase Phases.Print_stats >>= fun () ->
Signal.send Signals.on_print_stats ();
let = Options.comment() in
let print_gc () =
let stats = Gc.stat () in
Format.printf
"@[<h>%sGC: minor words %.0f; major_words: %.0f; max_heap: %d; \
minor collections %d; major collections %d@]@."
comment
stats.Gc.minor_words stats.Gc.major_words stats.Gc.top_heap_words
stats.Gc.minor_collections stats.Gc.major_collections;
in
Phases.get_key Params.key >>= fun params ->
if params.Params.stats then (
print_gc ();
Util.print_global_stats ~comment ();
);
Phases.return_phase ()
let presaturate_clauses (type c)
(module Env : Env.S with type C.t = c)
(c_sets : c Clause.sets) =
Phases.start_phase Phases.Pre_saturate >>= fun () ->
let module Sat = Saturate.Make(Env) in
let num_clauses = CCVector.length c_sets.Clause.c_set in
if Env.params.Params.presaturate
then (
Util.debug ~section 1 "presaturate initial clauses";
Env.add_passive (CCVector.to_seq c_sets.Clause.c_set);
let result, num = Sat.presaturate () in
Util.debugf ~section 1 "initial presaturation in %d steps" (fun k->k num);
let c_set = Env.get_active() |> CCVector.of_seq |> CCVector.freeze in
let clauses = {c_sets with Clause.c_set; } in
Env.remove_active (CCVector.to_seq c_set);
Env.remove_passive (CCVector.to_seq c_set);
Util.debugf ~section 2 "@[<2>%d clauses pre-saturated into:@ @[<hv>%a@]@]"
(fun k->k num_clauses (Util.pp_seq ~sep:" " Env.C.pp) (CCVector.to_seq c_set));
Phases.return_phase (result, clauses)
)
else Phases.return_phase (Saturate.Unknown, c_sets)
let try_to_refute (type c) (module Env : Env.S with type C.t = c) clauses result =
Phases.start_phase Phases.Saturate >>= fun () ->
let module Sat = Saturate.Make(Env) in
if not (CCVector.is_empty clauses.Clause.c_sos) then (
Env.Ctx.lost_completeness();
);
Env.add_active (CCVector.to_seq clauses.Clause.c_sos);
Env.add_passive (CCVector.to_seq clauses.Clause.c_set);
let steps = if Env.params.Params.steps < 0
then None
else (
Util.debugf ~section 1 "run for %d steps" (fun k->k Env.params.Params.steps);
Some Env.params.Params.steps
)
and timeout = if Env.params.Params.timeout = 0.
then None
else (
Util.debugf ~section 1 "run for %.3f s" (fun k->k Env.params.Params.timeout);
ignore (setup_alarm Env.params.Params.timeout);
Some (Util.total_time_s () +. Env.params.Params.timeout -. 0.25)
)
in
Signal.send Env.on_start ();
let result, num = match result with
| Saturate.Unsat _ -> result, 0
| _ -> Sat.given_clause ~generating:true ?steps ?timeout ()
in
let = Options.comment() in
Format.printf "%sdone %d iterations in %.3fs@." comment num (Util.total_time_s());
Util.debugf ~section 1 "@[<2>final precedence:@ @[%a@]@]"
(fun k->k Precedence.pp (Env.precedence ()));
Phases.return_phase result
let print_dots (type c)
(module Env : Env_intf.S with type C.t = c)
(result : Saturate.szs_status) =
Phases.start_phase Phases.Print_dot >>= fun () ->
Signal.send Signals.on_dot_output ();
begin match Env.params.Params.dot_file, result with
| Some dot_f, Saturate.Unsat proof ->
let name = "unsat_graph" in
let proof =
if Env.params.Params.dot_all_roots
then
Env.(Iter.append (get_active()) (get_passive()))
|> Iter.filter_map
(fun c ->
if Literals.is_absurd (Env.C.lits c)
then Some (Env.C.proof c)
else None)
else Iter.singleton proof
in
Proof.S.pp_dot_seq_file ~name dot_f proof
| Some dot_f, (Saturate.Sat | Saturate.Unknown) when Env.params.Params.dot_sat ->
let name = "sat_set" in
let seq = Iter.append (Env.get_active ()) (Env.get_passive ()) in
let seq = Iter.map Env.C.proof seq in
Proof.S.pp_dot_seq_file ~name dot_f seq
| _ -> ()
end;
Phases.return_phase ()
let sat_to_str () =
if !has_goal_ then "CounterSatisfiable" else "Satisfiable"
let unsat_to_str () =
if !has_goal_ then "Theorem" else "Unsatisfiable"
let print_szs_result (type c) ~file
(module Env : Env_intf.S with type C.t = c)
(result : Saturate.szs_status) =
Phases.start_phase Phases.Print_result >>= fun () ->
let = Options.comment() in
begin match result with
| Saturate.Unknown
| Saturate.Timeout ->
Format.printf "%sSZS status ResourceOut for '%s'@." comment file
| Saturate.Error s ->
Format.printf "%sSZS status InternalError for '%s'@." comment file;
Util.debugf ~section 1 "error is:@ %s" (fun k->k s);
| Saturate.Sat when Env.Ctx.is_completeness_preserved () ->
Format.printf "%sSZS status %s for '%s'@." comment (sat_to_str ()) file
| Saturate.Sat ->
Format.printf "%sSZS status GaveUp for '%s'@." comment file;
begin match !Options.output with
| Options.O_none -> ()
| Options.O_zf -> failwith "not implemented: printing in ZF"
| Options.O_tptp ->
Util.debugf ~section 1 "@[<2>saturated set:@ @[<hv>%a@]@]"
(fun k->k (Util.pp_seq ~sep:" " Env.C.pp_tstp_full) (Env.get_active ()))
| Options.O_normal ->
Util.debugf ~section 1 "@[<2>saturated set:@ @[<hv>%a@]@]"
(fun k->k (Util.pp_seq ~sep:" " Env.C.pp) (Env.get_active ()))
end
| Saturate.Unsat proof ->
Format.printf "%sSZS status %s for '%s'@." comment (unsat_to_str ()) file;
Format.printf "%sSZS output start Refutation@." comment;
Format.printf "%a@." (Proof.S.pp_in !Options.output) proof;
Format.printf "%sSZS output end Refutation@." comment;
end;
Phases.return_phase ()
let pp_weight prec out s =
Format.fprintf out "w(%a)=%a"
ID.pp s Precedence.Weight.pp (Precedence.weight prec s)
let has_goal_decls_ decls =
CCVector.exists
(fun st -> match Statement.view st with
| Statement.Goal _ -> true
| _ -> false)
decls
let parse_cli =
Phases.start_phase Phases.Parse_CLI >>= fun () ->
CCFormat.set_color_default true;
let params = Params.parse_args () in
let files = CCVector.to_list params.Params.files in
Phases.set_key Params.key params >>= fun () ->
print_version ~params;
Phases.return_phase (files, params)
let syms_in_conj decls =
let open Iter in
decls
|> CCVector.to_seq
|> flat_map (fun st ->
let pr = Statement.proof_step st in
if CCOpt.is_some (Proof.Step.distance_to_goal pr) then (
Statement.Seq.symbols st
) else empty)
let process_file ?(prelude=Iter.empty) file =
start_file file >>= fun () ->
parse_file file >>= fun stmts ->
typing ~file prelude stmts >>= fun decls ->
CCVector.iter Statement.scan_simple_stmt_for_ind_ty decls;
let has_goal = has_goal_decls_ decls in
Util.debugf ~section 1 "parsed %d declarations (%s goal(s))"
(fun k->k (CCVector.length decls) (if has_goal then "some" else "no"));
let quant_transformer =
if !Booleans._quant_rename then Booleans.preprocess_booleans
else CCFun.id in
let transformed = Rewriting.unfold_def_before_cnf (quant_transformer decls) in
let sk_ctx = Skolem.create () in
cnf ~sk_ctx transformed >>= fun stmts ->
let stmts = Booleans.preprocess_cnf_booleans stmts in
let conj_syms = syms_in_conj stmts in
let signature = Statement.signature ~conj_syms:conj_syms (CCVector.to_seq stmts) in
compute_prec ~signature (CCVector.to_seq stmts) >>= fun precedence ->
Util.debugf ~section 1 "@[<2>precedence:@ @[%a@]@]" (fun k->k Precedence.pp precedence);
compute_ord_select precedence >>= fun (ord, select) ->
Phases.get_key Params.key >>= fun params ->
let eta = params.Params.eta in
make_ctx ~signature ~ord ~select ~eta ~sk_ctx () >>= fun ctx ->
make_env ~params ~ctx stmts >>= fun (Phases.Env_clauses (env,clauses)) ->
has_goal_ := has_goal;
presaturate_clauses env clauses >>= fun (result, clauses) ->
try_to_refute env clauses result >>= fun result ->
Phases.return (Phases.Env_result (env, result))
let print file env result =
print_stats_env env;
print_szs_result ~file env result >>= fun () ->
print_dots env result
let check res =
Phases.start_phase Phases.Check_proof >>= fun () ->
Phases.get_key Params.key >>= fun params ->
let = Options.comment() in
let errcode = match res with
| Saturate.Unsat p when params.Params.check ->
Util.debug ~section 1 "start checking proof…";
let p' = LLProof_conv.conv p in
let start = Util.total_time_s () in
let dot_prefix = params.Params.dot_check in
let res, stats = LLProof_check.check ?dot_prefix p' in
let stop = Util.total_time_s () in
Format.printf "%s(@[<h>proof_check@ :res %a@ :stats %a :time %.3fs@])@."
comment LLProof_check.pp_res res LLProof_check.pp_stats stats (stop-.start);
begin match params.Params.dot_llproof with
| None -> ()
| Some file ->
Util.debugf ~section 2 "print LLProof into `%s`"(fun k->k file);
LLProof.Dot.pp_dot_file file p';
end;
if res = LLProof_check.R_fail then 15 else 0
| _ -> 0
in
Phases.return_phase errcode
let setup_gc =
Phases.start_phase Phases.Setup_gc >>= fun () ->
let gc = Gc.get () in
Gc.set { gc with Gc.space_overhead=150; };
Phases.return_phase ()
let setup_signal =
Phases.start_phase Phases.Setup_signal >>= fun () ->
Signal.set_exn_handler
(fun e ->
let stack = Printexc.get_backtrace () in
let msg = Printexc.to_string e in
output_string stderr ("exception raised in signal: " ^ msg ^ "\n");
output_string stderr stack;
flush stderr;
raise e);
Phases.return_phase ()
let process_files_and_print ?(params=Params.default) files =
parse_prelude params >>= fun prelude ->
let f file =
process_file ~prelude file >>= fun (Phases.Env_result (env, res)) ->
print file env res >>= fun () ->
check res
in
let phases = List.map f files in
Phases.run_parallel phases >>= fun r ->
print_stats () >>= fun () ->
Phases.return r
let main_cli ?setup_gc:(gc=true) () =
let open Phases.Infix in
(if gc then setup_gc else Phases.return ()) >>= fun () ->
setup_signal >>= fun () ->
parse_cli >>= fun (files, params) ->
load_extensions >>= fun _ ->
process_files_and_print ~params files >>= fun errcode ->
Phases.exit >|= fun () ->
errcode
let skip_parse_cli ?(params=Params.default) file =
Phases.start_phase Phases.Parse_CLI >>= fun () ->
CCFormat.set_color_default true;
Phases.set_key Params.key params >>= fun () ->
Phases.return_phase ([file], params)
let main ?setup_gc:(gc=true) ?params file =
let open Phases.Infix in
(if gc then setup_gc else Phases.return ()) >>= fun () ->
skip_parse_cli ?params file >>= fun (files, params) ->
load_extensions >>= fun _ ->
process_files_and_print ~params files >>= fun errcode ->
Phases.exit >|= fun () ->
errcode
let () =
let open Libzipperposition in
Params.add_opts [
"--de-bruijn-weight"
, Arg.Set_int _db_w
, " Set weight of de Bruijn index for KBO";
"--lift-lambdas"
, Arg.Bool (fun v -> _lift_lambdas := v)
, " Turn lambda lifting on or off.";
"--lambda-weight"
, Arg.Set_int _lmb_w
, " Set weight of lambda symbol for KBO";
"--kbo-weight-fun"
, Arg.Set_string _kbo_wf
, " Set the function for symbol weight calculation.";
];
Params.add_to_mode "ho-pragmatic" (fun () ->
_lmb_w := 20;
_db_w := 10;
);
Params.add_to_mode "ho-complete-basic" (fun () ->
_lmb_w := 20;
_db_w := 10;
);
Params.add_to_mode "ho-competitive" (fun () ->
_lmb_w := 20;
_db_w := 10;
);