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

remove unused functions

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-22 21:46:31 -07:00
parent 4c4810c611
commit bcb33a5b3a
2 changed files with 2 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/sat/smt/bv_internalize.cpp
View file

@ -165,10 +165,7 @@ namespace bv {
#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
#define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
#define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
#define internalize_int(B, U) \
ibin = [&](expr* x, expr* y) { return B(x, y); }; \
iun = [&](expr* x) { return U(x); }; \
internalize_interp(a, ibin, iun);
#define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
switch (a->get_decl_kind()) {
case OP_BV_NUM: internalize_num(a); break;
@ -527,22 +524,6 @@ namespace bv {
internalize_binary(a, bin);
}
void solver::internalize_udiv(app* n) {
bv_rewriter_params p(s().params());
expr* arg1 = n->get_arg(0);
expr* arg2 = n->get_arg(1);
mk_bits(get_th_var(n));
if (p.hi_div0()) {
add_unit(eq_internalize(n, bv.mk_bv_udiv_i(arg1, arg2)));
return;
}
unsigned sz = bv.get_bv_size(n);
expr_ref zero(bv.mk_numeral(0, sz), m);
expr_ref eq(m.mk_eq(arg2, zero), m);
expr_ref udiv(m.mk_ite(eq, bv.mk_bv_udiv0(arg1), bv.mk_bv_udiv_i(arg1, arg2)), m);
add_unit(eq_internalize(n, udiv));
}
void solver::internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& iun) {
bv_rewriter_params p(s().params());
expr* arg1 = n->get_arg(0);
@ -557,23 +538,6 @@ namespace bv {
expr_ref eq(m.mk_eq(arg2, zero), m);
expr_ref ite(m.mk_ite(eq, iun(arg1), ibin(arg1, arg2)), m);
add_unit(eq_internalize(n, ite));
}
void solver::internalize_sdiv(app* n) {
bv_rewriter_params p(s().params());
expr* arg1 = n->get_arg(0);
expr* arg2 = n->get_arg(1);
mk_bits(get_th_var(n));
if (p.hi_div0()) {
add_unit(eq_internalize(n, bv.mk_bv_sdiv_i(arg1, arg2)));
return;
}
unsigned sz = bv.get_bv_size(n);
expr_ref zero(bv.mk_numeral(0, sz), m);
expr_ref eq(m.mk_eq(arg2, zero), m);
expr_ref sdiv(m.mk_ite(eq, bv.mk_bv_sdiv0(arg1), bv.mk_bv_sdiv_i(arg1, arg2)), m);
add_unit(eq_internalize(n, sdiv));
}
void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {

4
src/sat/smt/bv_solver.h
View file

@ -239,6 +239,7 @@ namespace bv {
void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
void internalize_num(app * n);
void internalize_concat(app * n);
void internalize_bv2int(app* n);
@ -249,9 +250,6 @@ namespace bv {
void internalize_sub(app* n);
void internalize_extract(app* n);
void internalize_bit2bool(app* n);
void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
void internalize_udiv(app* n);
void internalize_sdiv(app* n);
void internalize_udiv_i(app* n);
template<bool Signed, bool Reverse, bool Negated>
void internalize_le(app* n);