simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

small perf change

Browse source
This commit is contained in:
Simon Cruanes 2015-02-06 17:47:29 +01:00
parent ce8920bf88
commit c2cfa14e86
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
solver/res.ml
View file

@ -273,14 +273,14 @@ module Make(St : Solver_types.S) = struct
aux (to_list c, to_list d) aux (to_list c, to_list d)
let unsat_core proof = let unsat_core proof =
let rec aux proof = let rec aux acc proof =
let p = proof () in let p = proof () in
match p.step with match p.step with
| Hypothesis | Lemma _ -> [p.conclusion] | Hypothesis | Lemma _ -> p.conclusion :: acc
| Resolution (proof1, proof2, _) -> | Resolution (proof1, proof2, _) ->
List.rev_append (aux proof1) (aux proof2) aux (aux acc proof1) proof2
in in
List.sort_uniq compare_cl (aux proof) List.sort_uniq compare_cl (aux [] proof)
(* Print proof graph *) (* Print proof graph *)
let _i = ref 0 let _i = ref 0