mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-07 14:55:06 +00:00
Code Activity

Refactor membership_atoms and add elements list

Browse source 
Renamed membership_atoms to membership_elements and added elements list.
This commit is contained in:
Nikolaj Bjorner 2025-10-15 12:46:52 +02:00 • committed by GitHub
parent a40e4f1cf3
commit bfda3d84c6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_finite_set.h
View file

@ -94,8 +94,8 @@ namespace smt {
class theory_finite_set : public theory { class theory_finite_set : public theory {
finite_set_util u; finite_set_util u;
finite_set_axioms m_axioms; finite_set_axioms m_axioms;
obj_hashtable<expr> m_membership_atoms; // set of all 'x in S' atoms obj_hashtable<expr> m_membership_elements; // set of all 'x' where there is an 'x in S' atom
obj_map<expr, ptr_vector<expr>> m_set_to_elements; // map from set S to elements x such that 'x in S' exists ptr_vector<expr> m_elements; // list of added x in m_membership_elements
protected: protected:
// Override relevant methods from smt::theory // Override relevant methods from smt::theory