mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

rename bit_blaster class to bit_blaster_simplifier to avoid name clash

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-30 18:39:02 -08:00
parent 0d05e0649b
commit 5f6f2fc758
3 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/simplifiers/bit_blaster.cpp
View file

@ -18,12 +18,12 @@ Author:
#include "ast/simplifiers/bit_blaster.h" #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_params.append(p);
m_rewriter.updt_params(m_params); 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_memory(r);
insert_max_steps(r); insert_max_steps(r);
r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders)."); 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."); 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(); m_rewriter.start_rewrite();
expr_ref new_curr(m); expr_ref new_curr(m);
proof_ref new_pr(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); st.update("bit-blaster-num-steps", m_num_steps);
} }
void bit_blaster::push() { void bit_blaster_simplifier::push() {
m_rewriter.push(); m_rewriter.push();
dependent_expr_simplifier::push(); dependent_expr_simplifier::push();
} }
void bit_blaster::pop(unsigned n) { void bit_blaster_simplifier::pop(unsigned n) {
dependent_expr_simplifier::pop(n); dependent_expr_simplifier::pop(n);
m_rewriter.pop(n); m_rewriter.pop(n);
} }

4
src/ast/simplifiers/bit_blaster.h
View file

@ -21,14 +21,14 @@ Author:
#include "ast/simplifiers/dependent_expr_state.h" #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; bit_blaster_rewriter m_rewriter;
unsigned m_num_steps = 0; unsigned m_num_steps = 0;
params_ref m_params; params_ref m_params;
public: 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), dependent_expr_simplifier(m, s),
m_rewriter(m, p) { m_rewriter(m, p) {
updt_params(p); updt_params(p);

2
src/sat/sat_solver/sat_smt_preprocess.cpp
View file

@ -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(card2bv, m, p, st));
s.add_simplifier(alloc(rewriter_simplifier, m, simp1_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(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)); s.add_simplifier(alloc(rewriter_simplifier, m, simp2_p, st));
} }
} }