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

hastwo

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-11-18 15:41:18 -08:00
parent 7ad8c6a6ce
commit cbefe74219
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/euf/euf_ac_plugin.cpp
View file

@ -477,14 +477,13 @@ namespace euf {
void ac_plugin::init_subset_iterator(unsigned eq_id, monomial_t const& m) { void ac_plugin::init_subset_iterator(unsigned eq_id, monomial_t const& m) {
unsigned max_use = 0; unsigned max_use = 0;
node* max_n = nullptr; node* max_n = nullptr;
bool has_two = false;
for (auto n : m) for (auto n : m)
if (n->root->eqs.size() >= max_use) if (n->root->eqs.size() > max_use)
max_n = n, max_use = n->root->eqs.size(); max_n = n->root, max_use = n->root->eqs.size(), has_two |= max_n != nullptr;
// found node that occurs in most eqs
VERIFY(max_n);
m_eq_occurs.reset(); m_eq_occurs.reset();
for (auto n : m) for (auto n : m)
if (n != max_n) if (n->root != max_n && has_two)
m_eq_occurs.append(n->root->eqs); m_eq_occurs.append(n->root->eqs);
compress_eq_occurs(eq_id); compress_eq_occurs(eq_id);
} }