From 23e70a192a20a4ba30d232b09869606d64bead6b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 14 Aug 2022 22:32:28 -0400 Subject: [PATCH] perf(cc): more inlining; remove dead code --- src/cc/CC.ml | 9 +++++---- src/cc/Sidekick_cc.ml | 3 ++- src/cc/Sidekick_cc.mli | 2 +- src/cc/signature.ml | 11 ++--------- src/cc/sigs.ml | 4 ---- src/cc/view.ml | 0 src/cc/view.mli | 0 src/core/CC_view.ml | 4 ++-- 8 files changed, 12 insertions(+), 21 deletions(-) delete mode 100644 src/cc/sigs.ml delete mode 100644 src/cc/view.ml delete mode 100644 src/cc/view.mli diff --git a/src/cc/CC.ml b/src/cc/CC.ml index 0af10dca..417e2253 100644 --- a/src/cc/CC.ml +++ b/src/cc/CC.ml @@ -180,14 +180,15 @@ let add_signature self (s : signature) (n : e_node) : unit = on_backtrack self (fun () -> Sig_tbl.remove self.signatures_tbl s); Sig_tbl.add self.signatures_tbl s n -let push_pending self t : unit = +let[@inline] push_pending self t : unit = Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" E_node.pp t); Vec.push self.pending t -let push_action self (a : Handler_action.t) : unit = +let[@inline] push_action self (a : Handler_action.t) : unit = Vec.push self.combine (CT_act a) -let push_action_l self (l : _ list) : unit = List.iter (push_action self) l +let[@inline] push_action_l self (l : _ list) : unit = + List.iter (push_action self) l let merge_classes self t u e : unit = if t != u && not (same_class t u) then ( @@ -544,7 +545,7 @@ and task_pending_ self (n : e_node) : unit = ) | Some s0 -> (* update the signature by using [find] on each sub-e_node *) - let s = update_sig s0 in + let s = (update_sig [@inlined]) s0 in (match find_signature self s with | None -> (* add to the signature table [sig(n) --> n] *) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 49cb02fe..f5357948 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -1,4 +1,5 @@ -module View = View +open Sidekick_core +module View = CC_view module E_node = E_node module Expl = Expl module Signature = Signature diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 9d2e149e..feed0665 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -4,7 +4,7 @@ module type DYN_MONOID_PLUGIN = Sigs_plugin.DYN_MONOID_PLUGIN module type MONOID_PLUGIN_ARG = Sigs_plugin.MONOID_PLUGIN_ARG module type MONOID_PLUGIN_BUILDER = Sigs_plugin.MONOID_PLUGIN_BUILDER -module View = View +module View = Sidekick_core.CC_view module E_node = E_node module Expl = Expl module Signature = Signature diff --git a/src/cc/signature.ml b/src/cc/signature.ml index fa1adf7c..8678ba04 100644 --- a/src/cc/signature.ml +++ b/src/cc/signature.ml @@ -19,14 +19,7 @@ let equal (s1 : t) s2 : bool = E_node.equal a1 a2 && E_node.equal b1 b2 && E_node.equal c1 c2 | Eq (a1, b1), Eq (a2, b2) -> E_node.equal a1 a2 && E_node.equal b1 b2 | Opaque u1, Opaque u2 -> E_node.equal u1 u2 - | Bool _, _ - | App_fun _, _ - | App_ho _, _ - | If _, _ - | Eq _, _ - | Opaque _, _ - | Not _, _ -> - false + | (Bool _ | App_fun _ | App_ho _ | If _ | Eq _ | Opaque _ | Not _), _ -> false let hash (s : t) : int = let module H = CCHash in @@ -40,7 +33,7 @@ let hash (s : t) : int = H.combine4 60 (E_node.hash a) (E_node.hash b) (E_node.hash c) | Not u -> H.combine2 70 (E_node.hash u) -let pp out = function +let[@inline never] pp out = function | Bool b -> Fmt.bool out b | App_fun (f, []) -> Const.pp out f | App_fun (f, l) -> diff --git a/src/cc/sigs.ml b/src/cc/sigs.ml deleted file mode 100644 index fd0fbed3..00000000 --- a/src/cc/sigs.ml +++ /dev/null @@ -1,4 +0,0 @@ -(** Main types for congruence closure *) - -open Sidekick_core -module View = View diff --git a/src/cc/view.ml b/src/cc/view.ml deleted file mode 100644 index e69de29b..00000000 diff --git a/src/cc/view.mli b/src/cc/view.mli deleted file mode 100644 index e69de29b..00000000 diff --git a/src/core/CC_view.ml b/src/core/CC_view.ml index e319f5ef..91050870 100644 --- a/src/core/CC_view.ml +++ b/src/core/CC_view.ml @@ -8,7 +8,7 @@ type ('f, 't, 'ts) t = | Opaque of 't (* do not enter *) -let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t = +let[@inline] map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t = match v with | Bool b -> Bool b | App_fun (f, args) -> App_fun (f_f f, f_ts args) @@ -18,7 +18,7 @@ let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t = | Eq (a, b) -> Eq (f_t a, f_t b) | Opaque t -> Opaque (f_t t) -let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit = +let[@inline] iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit = match v with | Bool _ -> () | App_fun (f, args) ->