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

refactor: stats, small changes

Browse source
This commit is contained in:
Simon Cruanes 2022-08-22 22:09:36 -04:00
parent 279ceade78
commit dde63a9ef2
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/smt/solver_internal.ml
View file

@ -455,9 +455,12 @@ let check_cc_with_acts_ (self : t) (acts : theory_actions) =
(function (function
| CC.Result_action.Act_propagate { lit; reason } -> | CC.Result_action.Act_propagate { lit; reason } ->
let reason = Sidekick_sat.Consequence reason in let reason = Sidekick_sat.Consequence reason in
Stat.incr self.count_propagate;
A.propagate lit reason) A.propagate lit reason)
acts acts
| Error (CC.Result_action.Conflict (lits, pr)) -> A.raise_conflict lits pr | Error (CC.Result_action.Conflict (lits, pr)) ->
Stat.incr self.count_conflict;
A.raise_conflict lits pr
(* handle a literal assumed by the SAT solver *) (* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t) let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
@ -471,16 +474,16 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
self.level self.level
(Util.pp_iter ~sep:"; " Lit.pp) (Util.pp_iter ~sep:"; " Lit.pp)
lits); lits);
(* transmit to CC *)
let cc = cc self in let cc = cc self in
(* transmit to CC *)
if not final then CC.assert_lits cc lits; if not final then CC.assert_lits cc lits;
(* transmit to theories. *)
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
if final then ( if final then (
Perform_delayed_th.top self acts; Perform_delayed_th.top self acts;
(* transmit to theories. *)
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
@ -526,6 +529,7 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
Perform_delayed_th.top self acts Perform_delayed_th.top self acts
) else ( ) else (
(* partial check *)
List.iter (fun f -> f self acts lits) self.on_partial_check; List.iter (fun f -> f self acts lits) self.on_partial_check;
(* re-check CC after theory actions, which might have merged classes *) (* re-check CC after theory actions, which might have merged classes *)
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
@ -563,15 +567,15 @@ let[@inline] final_check (self : t) (acts : Sidekick_sat.acts) : unit =
let push_level self : unit = let push_level self : unit =
self.level <- 1 + self.level; self.level <- 1 + self.level;
CC.push_level (cc self); CC.push_level (cc self);
push_lvl_ self.th_states push_lvl_theories_ self.th_states
let pop_levels self n : unit = let pop_levels self n : unit =
self.last_model <- None; self.last_model <- None;
self.level <- self.level - n; self.level <- self.level - n;
CC.pop_levels (cc self) n; CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states pop_lvls_theories_ n self.th_states
let n_levels self = self.level let[@inline] n_levels self = self.level
let to_sat_plugin (self : t) : (module Sidekick_sat.PLUGIN) = let to_sat_plugin (self : t) : (module Sidekick_sat.PLUGIN) =
(module struct (module struct
@ -587,6 +591,7 @@ let declare_pb_is_incomplete self =
self.complete <- false self.complete <- false
let add_theory_state ~st ~push_level ~pop_levels (self : t) = let add_theory_state ~st ~push_level ~pop_levels (self : t) =
assert (self.level = 0);
self.th_states <- self.th_states <-
Ths_cons { st; push_level; pop_levels; next = self.th_states } Ths_cons { st; push_level; pop_levels; next = self.th_states }