mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail

Browse source 
It avoid doing all the funky watch stuff
One extreme Alive2 test case goes from 40s to 28s :)
This commit is contained in:
Nuno Lopes 2023-08-20 10:07:56 +01:00
parent 5e3df9ee77
commit 5d33805c8b
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_relevancy.cpp
View file

@ -123,7 +123,7 @@ namespace smt {
}
struct relevancy_propagator_imp : public relevancy_propagator {
unsigned m_qhead;
unsigned m_qhead = 0;
expr_ref_vector m_relevant_exprs;
uint_set m_is_relevant;
typedef list<relevancy_eh *> relevancy_ehs;
@ -144,14 +144,18 @@ namespace smt {
unsigned m_trail_lim;
};
svector<scope> m_scopes;
bool m_propagating;
bool m_propagating = false;
relevancy_propagator_imp(context & ctx):
relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()),
m_propagating(false) {}
relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {}
~relevancy_propagator_imp() override {
undo_trail(0);
ast_manager & m = get_manager();
unsigned i = m_trail.size();
while (i != 0) {
--i;
m.dec_ref(m_trail[i].get_node());
}
}
relevancy_ehs * get_handlers(expr * n) {