From a2a5924e5c3986331545ba9ab19ae1e0b4841da5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jan 2022 14:14:09 -0800 Subject: [PATCH] purge more --- src/sat/smt/euf_solver.h | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 77fce4a20..3a48ae3b1 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -371,13 +371,9 @@ namespace euf { bool enable_ackerman_axioms(expr* n) const; // relevancy - bool m_relevancy_enabled = true; - ptr_vector m_auto_relevant; - unsigned_vector m_auto_relevant_lim; - unsigned m_auto_relevant_scopes = 0; - bool relevancy_enabled() const { return m_relevancy_enabled && get_config().m_relevancy_lvl > 0; } - void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy_enabled = false; } + bool relevancy_enabled() const { return m_relevancy.enabled(); } + void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy.set_enabled(false); } void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); } void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); } void add_root(sat::literal lit) { add_root(1, &lit); }