From eac65049bdecfc74b6fb898229bcee0b4e34830e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 16 May 2026 11:01:01 +0000 Subject: [PATCH] util/irep: O(1) SHARING fast-path for irept::compare Under SHARING, return 0 immediately from irept::compare when both instances point to the same node (data == i.data). Structurally-shared expressions are common on hot std::map paths (e.g. smt2_convt's defined_expressions / datatype_map lookups under heavy struct flattening), where the full sub-tree walk is redundant. Co-authored-by: Kiro --- src/util/irep.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 36e103ea8ff..2f35a1feaf4 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -300,6 +300,16 @@ bool irept::ordering(const irept &other) const /// comments are ignored int irept::compare(const irept &i) const { + // Fast path: structurally-shared instances compare equal in O(1). + // Without this, dictionaries / std::map walk the entire + // sub-tree even when both keys point to the same node — this is + // a hot path under heavy SMT struct flattening (smt2_convt's + // defined_expressions / datatype_map lookups). +#ifdef SHARING + if(data == i.data) + return 0; +#endif + int r; r=id().compare(i.id());