mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity

better equality solving pre-processing with bv

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-12 17:18:26 -07:00
parent d980ac9a05
commit 13c098f4b2
1 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/ast/simplifiers/extract_eqs.cpp
View file

@ -92,7 +92,6 @@ namespace euf {
if (!bv.is_bv_add(x))
return;
expr_ref term(m);
unsigned i = 0;
auto mk_term = [&](unsigned i) {
term = y;
unsigned j = 0;
@ -102,17 +101,40 @@ namespace euf {
++j;
}
};
expr* u = nullptr, *z = nullptr;
rational r;
unsigned i = 0;
for (expr* arg : *to_app(x)) {
if (is_uninterp_const(arg)) {
mk_term(i);
eqs.push_back(dependent_eq(orig, to_app(arg), term, d));
}
else if (bv.is_bv_mul(arg, u, z) && bv.is_numeral(u, r) && is_uninterp_const(z) && r.is_odd()) {
mk_term(i);
unsigned sz = bv.get_bv_size(z);
rational inv_r;
VERIFY(r.mult_inverse(sz, inv_r));
term = bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), term);
eqs.push_back(dependent_eq(orig, to_app(z), term, d));
}
++i;
}
}
void solve_mul(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
expr* u = nullptr, *z = nullptr;
rational r, inv_r;
if (bv.is_bv_mul(x, u, z) && bv.is_numeral(u, r) && is_uninterp_const(z) && r.is_odd()) {
unsigned sz = bv.get_bv_size(z);
VERIFY(r.mult_inverse(sz, inv_r));
auto term = expr_ref(bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), y), m);
eqs.push_back(dependent_eq(orig, to_app(z), term, d));
}
}
void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
solve_add(orig, x, y, d, eqs);
solve_mul(orig, x, y, d, eqs);
}
@ -132,12 +154,9 @@ namespace euf {
}
void pre_process(dependent_expr_state& fmls) override {
if (!m_enabled)
return;
}
void updt_params(params_ref const& p) override {
}
};