mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-13 09:31:14 +00:00
Code Activity

Add m_lemmas member to theory_finite_set class

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-15 14:46:37 +02:00 • committed by GitHub
parent d7035a25e7
commit 8ec04d2b81
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_finite_set.h
View file

@ -95,6 +95,7 @@ namespace smt {
finite_set_util u; finite_set_util u;
finite_set_axioms m_axioms; finite_set_axioms m_axioms;
obj_hashtable<enode> m_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
vector<expr_ref_vector> m_lemmas;
protected: protected:
// Override relevant methods from smt::theory // Override relevant methods from smt::theory