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

Some more info in debug logging

Browse source
This commit is contained in:
Guillaume Bury 2016-11-22 17:00:39 +01:00
parent 73ea4fea30
commit 9a393c130a
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/core/external.ml
View file

@ -56,10 +56,10 @@ module Make
| Sat of (St.term,St.formula) sat_state
| Unsat of (St.clause,Proof.proof) unsat_state
let pp_all lvl =
let pp_all lvl status =
Log.debugf lvl
"@[<v>Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,]@."
(fun k -> k
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
(fun k -> k status
(Vec.print ~sep:"" St.pp) (S.trail ())
(Vec.print ~sep:"" St.pp_clause) (S.temp ())
(Vec.print ~sep:"" St.pp_clause) (S.hyps ())
@ -67,7 +67,7 @@ module Make
)
let mk_sat () : (_,_) sat_state =
pp_all 99;
pp_all 99 "SAT";
let t = S.trail () in
let iter f f' =
Vec.iter (function
@ -83,7 +83,7 @@ module Make
}
let mk_unsat () : (_,_) unsat_state =
pp_all 99;
pp_all 99 "UNSAT";
let unsat_conflict () =
match S.unsat_conflict () with
| None -> assert false