From ef60d1466fdce8405810c80551c1e7a05fa36aea Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 21:23:02 -0600 Subject: [PATCH] feat: better debug message --- src/msat-solver/Sidekick_msat_solver.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index ce2fdc6f..be1a4be8 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -168,6 +168,7 @@ module Make(A : ARG) mutable th_states : th_states; (** Set of theories *) mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list; mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list; + mutable level: int; } and preprocess_hook = @@ -289,18 +290,20 @@ module Make(A : ARG) | Ths_cons r -> r.pop_levels r.st n; pop_lvls_ n r.next let push_level (self:t) : unit = + self.level <- 1 + self.level; CC.push_level (cc self); push_lvl_ self.th_states let pop_levels (self:t) n : unit = + self.level <- self.level - n; CC.pop_levels (cc self) n; pop_lvls_ n self.th_states (* handle a literal assumed by the SAT solver *) let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit = Msat.Log.debugf 2 - (fun k->k "(@[@{msat-solver.assume_lits@}%s@ %a@])" - (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits); + (fun k->k "(@[@{msat-solver.assume_lits@}%s[lvl=%d]@ %a@])" + (if final then "[final]" else "") self.level (Util.pp_seq ~sep:"; " Lit.pp) lits); (* transmit to CC *) let cc = cc self in if not final then ( @@ -369,6 +372,7 @@ module Make(A : ARG) count_conflict = Stat.mk_int stat "solver.th-conflicts"; on_partial_check=[]; on_final_check=[]; + level=0; } in ignore (Lazy.force @@ self.cc : CC.t); self