mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

gc perf fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-06 14:26:51 -07:00
parent f4ec63f39c
commit a51e40a6cd
3 changed files with 46 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/smt_context.cpp
View file

@ -2007,12 +2007,38 @@ namespace smt {
Reduce the size of v to old_size.
*/
void context::del_clauses(clause_vector & v, unsigned old_size) {
SASSERT(old_size <= v.size());
unsigned num_collect = v.size() - old_size;
if (num_collect == 0)
return;
clause_vector::iterator begin = v.begin() + old_size;
clause_vector::iterator it = v.end();
while (it != begin) {
--it;
del_clause(false, *it);
if (num_collect > 1000) {
uint_set watches;
while (it != begin) {
--it;
clause* c = *it;
remove_lit_occs(*c, get_num_bool_vars());
if (!c->deleted()) {
c->mark_as_deleted(m);
}
watches.insert((~c->get_literal(0)).index());
watches.insert((~c->get_literal(1)).index());
}
for (auto w: watches) {
m_watches[w].remove_deleted();
}
for (it = v.end(); it != begin; ) {
--it;
(*it)->deallocate(m);
}
m_stats.m_num_del_clause += (v.size() - old_size);
}
else {
while (it != begin) {
--it;
del_clause(false, *it);
}
}
v.shrink(old_size);
}

14
src/smt/watch_list.cpp
View file

@ -94,6 +94,20 @@ namespace smt {
}
end_cls_core() -= sizeof(clause *);
}
void watch_list::remove_deleted() {
clause_iterator end = end_clause();
clause_iterator it = begin_clause();
clause_iterator prev = it;
unsigned num_deleted = 0;
for (; it != end; ++it) {
if ((*it)->deleted())
++num_deleted;
else
*prev++ = *it;
}
end_cls_core() -= num_deleted * sizeof(clause *);
}
void watch_list::remove_literal(literal l) {
literal * begin = begin_literals();

2
src/smt/watch_list.h
View file

@ -171,6 +171,8 @@ namespace smt {
}
void remove_clause(clause * c);
void remove_deleted();
void remove_literal(literal l);