mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 13:56:03 +00:00
Code Activity

Add friend class declaration for testing

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

4
src/smt/theory_finite_set.h
View file

@ -92,6 +92,7 @@ theory_finite_set.cpp.
namespace smt { namespace smt {
class theory_finite_set : public theory { class theory_finite_set : public theory {
friend class theory_finite_set_test;
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
@ -114,6 +115,9 @@ namespace smt {
// Helper methods for axiom instantiation // Helper methods for axiom instantiation
void instantiate_axioms(expr* elem, expr* set); void instantiate_axioms(expr* elem, expr* set);
void add_clause(expr_ref_vector const& clause); void add_clause(expr_ref_vector const& clause);
void instantiate_false_lemma();
void instantiate_unit_propagation();
void instantiate_free_lemma();
public: public:
theory_finite_set(context& ctx); theory_finite_set(context& ctx);