mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove separate to_add_literal queue

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-29 12:45:43 -08:00
parent e972eb33b2
commit d469c1054e
2 changed files with 14 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/ast/euf/euf_egraph.cpp
View file

@ -88,7 +88,7 @@ namespace euf {
void egraph::queue_literal(enode* p, enode* ante) {
if (m_on_propagate_literal)
m_to_add_literal.push_back({ p, ante });
m_to_merge.push_back({ p, ante });
}
void egraph::force_push() {
@ -352,7 +352,6 @@ namespace euf {
if (num_scopes <= m_num_scopes) {
m_num_scopes -= num_scopes;
m_to_merge.reset();
m_to_add_literal.reset();
return;
}
num_scopes -= m_num_scopes;
@ -435,7 +434,6 @@ namespace euf {
m_scopes.shrink(old_lim);
m_region.pop_scope(num_scopes);
m_to_merge.reset();
m_to_add_literal.reset();
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
@ -588,14 +586,16 @@ namespace euf {
unsigned j = 0;
for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
auto const& w = m_to_merge[i];
merge(w.a, w.b, justification::congruence(w.commutativity, m_congruence_timestamp++));
for (; j < m_to_add_literal.size() && m.limit().inc() && !inconsistent(); ++j) {
auto const& [p, ante] = m_to_add_literal[j];
add_literal(p, ante);
}
switch (w.t) {
case to_merge_plain:
merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++));
break;
case to_add_literal:
add_literal(w.a, w.b);
break;
}
}
m_to_merge.reset();
m_to_add_literal.reset();
return
(m_new_th_eqs_qhead < m_new_th_eqs.size()) ||
inconsistent();

13
src/ast/euf/euf_egraph.h
View file

@ -84,15 +84,13 @@ namespace euf {
typedef ptr_vector<trail> trail_stack;
enum to_merge_t { to_merge_plain, to_merge_comm, to_add_literal };
struct to_merge {
enode* a, * b;
bool commutativity;
to_merge(enode* a, enode* b, bool c) : a(a), b(b), commutativity(c) {}
};
struct to_add_literal {
enode* p, *ante;
to_add_literal(enode* p, enode* ante) : p(p), ante(ante) {}
to_merge_t t;
bool commutativity() const { return t == to_merge_comm; }
to_merge(enode* a, enode* b, bool c) : a(a), b(b), t(c ? to_merge_comm : to_merge_comm) {}
to_merge(enode* p, enode* ante): a(p), b(ante), t(to_add_literal) {}
};
struct stats {
@ -167,7 +165,6 @@ namespace euf {
};
ast_manager& m;
svector<to_merge> m_to_merge;
svector<to_add_literal> m_to_add_literal;
etable m_table;
region m_region;
svector<update_record> m_updates;