From bfda3d84c623c2dfc6e4b78b2d55d4fb5261f100 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 12:46:52 +0200 Subject: [PATCH] Refactor membership_atoms and add elements list Renamed membership_atoms to membership_elements and added elements list. --- src/smt/theory_finite_set.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index b80377e49..0bb6f9ac5 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -94,8 +94,8 @@ namespace smt { class theory_finite_set : public theory { finite_set_util u; finite_set_axioms m_axioms; - obj_hashtable m_membership_atoms; // set of all 'x in S' atoms - obj_map> m_set_to_elements; // map from set S to elements x such that 'x in S' exists + obj_hashtable m_membership_elements; // set of all 'x' where there is an 'x in S' atom + ptr_vector m_elements; // list of added x in m_membership_elements protected: // Override relevant methods from smt::theory @@ -120,4 +120,4 @@ namespace smt { ~theory_finite_set() override {} }; -} // namespace smt \ No newline at end of file +} // namespace smt