From 481e8e9e58f481b14198a8280986677bb9a41ef4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 24 Mar 2021 12:07:11 -0400 Subject: [PATCH] feat(msat-solver): profiling probe for conflicts --- src/msat-solver/Sidekick_msat_solver.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 638ffdc0..02c759ca 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -674,7 +674,12 @@ module Make(A : ARG) List.iter (fun f->f()) on_exit; in 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; match r with | Sat_solver.Sat st ->