simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(msat-solver): profiling probe for conflicts

Browse source
This commit is contained in:
Simon Cruanes 2021-03-24 12:07:11 -04:00
parent f893f14f21
commit 481e8e9e58
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -674,7 +674,12 @@ module Make(A : ARG)
List.iter (fun f->f()) on_exit; List.iter (fun f->f()) on_exit;
in in
self.si.on_progress <- (fun () -> on_progress self); self.si.on_progress <- (fun () -> on_progress self);
let r = Sat_solver.solve ~assumptions (solver self) in let on_conflict =
if Profile.enabled()
then Some (fun _ -> Profile.instant "sat.conflict")
else None
in
let r = Sat_solver.solve ?on_conflict ~assumptions (solver self) in
Stat.incr self.count_solve; Stat.incr self.count_solve;
match r with match r with
| Sat_solver.Sat st -> | Sat_solver.Sat st ->