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

Update theory_finite_set.cpp

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

13
src/smt/theory_finite_set.cpp
View file

@ -46,9 +46,11 @@ namespace smt {
// Track membership atoms (set.in) // Track membership atoms (set.in)
expr* elem = nullptr, *set = nullptr; expr* elem = nullptr, *set = nullptr;
if (u.is_in(atom, elem, set)) { if (u.is_in(atom, elem, set)) {
// add elem to a list of elements if it not there already. auto n = get_enode(elem);
// ctx.trail().push(insert(m_elems, elem)); if (m_elements.contains(n))
// ctx.trail().push(push_back_vector(m_elems)); continue;
m_elements.insert(n);
ctx.trail().push(insert_obj_trail(n));
} }
return true; return true;
@ -97,14 +99,15 @@ namespace smt {
TRACE("finite_set", tout << "final_check_eh\n";); TRACE("finite_set", tout << "final_check_eh\n";);
bool new_clause = false; bool new_clause = false;
#if 0
for (auto elem : m_elements) { for (auto elem : m_elements) {
for (auto p : enode::parents(elem)) {
}
// walk all parents of elem in congruence table. // walk all parents of elem in congruence table.
// if a parent is of the form elem' in S u T, or similar. // if a parent is of the form elem' in S u T, or similar.
// create clauses for elem = elem' => clause. // create clauses for elem = elem' => clause.
// if a new clause was added, return FC_CONTINUE // if a new clause was added, return FC_CONTINUE
} }
#endif
return new_clause ? FC_CONTINUE : FC_DONE; return new_clause ? FC_CONTINUE : FC_DONE;
} }