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

Better logging in proofs

Browse source
This commit is contained in:
Guillaume Bury 2016-07-29 12:58:21 +02:00
parent d6c6331d85
commit 51c76479b9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/res.ml
View file

@ -115,7 +115,7 @@ module Make(St : Solver_types.S) = struct
let rec chain_res (c, cl) = function let rec chain_res (c, cl) = function
| d :: r -> | d :: r ->
Log.debugf 7 "@[<v4> Resolving clauses : %a@,%a@]" Log.debugf 7 " Resolving clauses : @[%a@\n%a@]"
(fun k -> k St.pp_clause c St.pp_clause d); (fun k -> k St.pp_clause c St.pp_clause d);
let dl = to_list d in let dl = to_list d in
begin match resolve (merge cl dl) with begin match resolve (merge cl dl) with
@ -132,7 +132,7 @@ module Make(St : Solver_types.S) = struct
| _ -> assert false | _ -> assert false
let rec expand conclusion = let rec expand conclusion =
Log.debugf 5 "@[Expanding : %a@]" (fun k -> k St.pp_clause conclusion); Log.debugf 5 "Expanding : @[%a@]" (fun k -> k St.pp_clause conclusion);
match conclusion.St.cpremise with match conclusion.St.cpremise with
| St.Lemma l -> | St.Lemma l ->
{conclusion; step = Lemma l; } {conclusion; step = Lemma l; }