From 5d33805c8b1f377bfccabe2cc2d56ca35c54ed40 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 10:07:56 +0100 Subject: [PATCH] optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail It avoid doing all the funky watch stuff One extreme Alive2 test case goes from 40s to 28s :) --- src/smt/smt_relevancy.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 649d75737..ce6de3ec3 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -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_ehs; @@ -144,14 +144,18 @@ namespace smt { unsigned m_trail_lim; }; svector 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) {