From 5f6f2fc758bd68836ab2db1c9a3f580a25b9f75c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Dec 2022 18:39:02 -0800 Subject: [PATCH] rename bit_blaster class to bit_blaster_simplifier to avoid name clash --- src/ast/simplifiers/bit_blaster.cpp | 12 ++++++------ src/ast/simplifiers/bit_blaster.h | 4 ++-- src/sat/sat_solver/sat_smt_preprocess.cpp | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/ast/simplifiers/bit_blaster.cpp b/src/ast/simplifiers/bit_blaster.cpp index c66cef826da..eed751f3958 100644 --- a/src/ast/simplifiers/bit_blaster.cpp +++ b/src/ast/simplifiers/bit_blaster.cpp @@ -18,12 +18,12 @@ Module Name: #include "ast/simplifiers/bit_blaster.h" -void bit_blaster::updt_params(params_ref const & p) { +void bit_blaster_simplifier::updt_params(params_ref const & p) { m_params.append(p); m_rewriter.updt_params(m_params); } -void bit_blaster::collect_param_descrs(param_descrs & r) { +void bit_blaster_simplifier::collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders)."); @@ -32,7 +32,7 @@ void bit_blaster::collect_param_descrs(param_descrs & r) { r.insert("blast_full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms."); } -void bit_blaster::reduce() { +void bit_blaster_simplifier::reduce() { m_rewriter.start_rewrite(); expr_ref new_curr(m); proof_ref new_pr(m); @@ -61,16 +61,16 @@ void bit_blaster::reduce() { } -void bit_blaster::collect_statistics(statistics& st) const { +void bit_blaster_simplifier::collect_statistics(statistics& st) const { st.update("bit-blaster-num-steps", m_num_steps); } -void bit_blaster::push() { +void bit_blaster_simplifier::push() { m_rewriter.push(); dependent_expr_simplifier::push(); } -void bit_blaster::pop(unsigned n) { +void bit_blaster_simplifier::pop(unsigned n) { dependent_expr_simplifier::pop(n); m_rewriter.pop(n); } diff --git a/src/ast/simplifiers/bit_blaster.h b/src/ast/simplifiers/bit_blaster.h index 231a1ca68ed..5724cc07599 100644 --- a/src/ast/simplifiers/bit_blaster.h +++ b/src/ast/simplifiers/bit_blaster.h @@ -21,14 +21,14 @@ Module Name: #include "ast/simplifiers/dependent_expr_state.h" -class bit_blaster : public dependent_expr_simplifier { +class bit_blaster_simplifier : public dependent_expr_simplifier { bit_blaster_rewriter m_rewriter; unsigned m_num_steps = 0; params_ref m_params; public: - bit_blaster(ast_manager & m, params_ref const & p, dependent_expr_state& s): + bit_blaster_simplifier(ast_manager & m, params_ref const & p, dependent_expr_state& s): dependent_expr_simplifier(m, s), m_rewriter(m, p) { updt_params(p); diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp index 7c716c48160..31888251c89 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ b/src/sat/sat_solver/sat_smt_preprocess.cpp @@ -98,7 +98,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep s.add_simplifier(alloc(card2bv, m, p, st)); s.add_simplifier(alloc(rewriter_simplifier, m, simp1_p, st)); s.add_simplifier(mk_max_bv_sharing(m, p, st)); - s.add_simplifier(alloc(bit_blaster, m, p, st)); + s.add_simplifier(alloc(bit_blaster_simplifier, m, p, st)); s.add_simplifier(alloc(rewriter_simplifier, m, simp2_p, st)); } }