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

Change membership elements to use enode type

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-15 12:58:02 +02:00 • committed by GitHub
parent bfda3d84c6
commit 05e599b55a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_finite_set.h
View file

@ -94,8 +94,7 @@ 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_elements; // set of all 'x' where there is an 'x in S' atom obj_hashtable<enode> m_elements; // set of all 'x' where there is an 'x in S' atom
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