mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fix axiomatization for sdiv

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 13:10:00 -08:00
parent 0ca94b9c2f
commit 477db7d8bd
4 changed files with 39 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_proof.cpp
View file

@ -92,7 +92,7 @@ namespace euf {
m_egraph.explain_eq<size_t>(m_explain, &m_explain_cc, a, b);
m_egraph.end_explain();
// Detect shortcut if equality is explained directly by a theory
if (m_explain.size() == 1 && !is_literal(m_explain[0])) {
if (m_explain.size() == 1 && is_justification(m_explain[0])) {
auto const& [x, y] = th_explain::from_index(get_justification(m_explain[0])).eq_consequent();
if (x == a && y == b)
continue;

31
src/sat/smt/polysat_internalize.cpp
View file

@ -427,8 +427,8 @@ namespace polysat {
unsigned sz = bv.get_bv_size(x);
expr* u = bv.mk_bv_urem(x, y);
rational N = rational::power_of_two(bv.get_bv_size(x));
expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x);
expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y);
sat::literal lsignx = mk_literal(signx);
sat::literal lsigny = mk_literal(signy);
sat::literal u_eq0 = eq_internalize(u, bv.mk_zero(sz));
@ -443,6 +443,22 @@ namespace polysat {
add_axiom(name, { y_eq0, lsignx, lsigny, eq_internalize(e, u) });
}
expr_ref solver::mk_ite(expr* c, expr* t, expr* e) {
expr_ref _c(c, m), _t(t, m), _e(e, m);
if (m.is_true(c))
return _t;
if (m.is_false(c))
return _e;
return expr_ref(m.mk_ite(c, t, e), m);
}
expr_ref solver::mk_ule(expr* l, expr* r) {
expr_ref res(bv.mk_ule(l, r), m);
ctx.get_rewriter()(res);
return res;
}
// d = udiv(abs(x), abs(y))
// y = 0, x > 0 -> 1
@ -455,17 +471,19 @@ namespace polysat {
void solver::axiomatize_sdiv(app* e, expr* x, expr* y) {
unsigned sz = bv.get_bv_size(x);
rational N = rational::power_of_two(bv.get_bv_size(x));
expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x);
expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y);
expr_ref absx = mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
expr_ref absy = mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
expr* d = bv.mk_bv_udiv(absx, absy);
sat::literal lsignx = mk_literal(signx);
sat::literal lsigny = mk_literal(signy);
sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
sat::literal x_eq0 = eq_internalize(x, bv.mk_zero(sz));
auto name = "sdiv";
add_axiom(name, { ~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz)) });
add_axiom(name, { ~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N - 1, sz)) });
add_axiom(name, { y_eq0, ~x_eq0, eq_internalize(e, bv.mk_zero(sz)) });
add_axiom(name, { y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d)) });
add_axiom(name, { y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d)) });
add_axiom(name, { y_eq0, lsignx, lsigny, eq_internalize(e, d) });
@ -499,6 +517,7 @@ namespace polysat {
euf::enode* rn = expr2enode(rem);
auto& m = a.manager();
unsigned sz = m.power_of_2();
verbose_stream() << "quot-rem " << a << " " << b << "\n";
if (b.is_zero()) {
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
internalize_set(quot, m.mk_val(m.max_value()));

13
src/sat/smt/polysat_solver.cpp
View file

@ -424,13 +424,22 @@ namespace polysat {
if (q.is_zero() && p.has_unit(x)) {
auto l = pdd2expr(x);
auto r = pdd2expr(x - p);
result = m.mk_eq(l, r);
if (m.are_equal(l, r))
result = m.mk_true();
else if (m.are_distinct(l, r))
result = m.mk_false();
else
result = m.mk_eq(l, r);
}
else {
auto l = pdd2expr(p);
auto r = pdd2expr(q);
if (p == q)
if (m.are_equal(l, r))
result = m.mk_true();
else if (m.is_value(l) && m.is_value(r)) {
result = bv.mk_ule(l, r);
ctx.get_rewriter()(result);
}
else if (q.is_zero())
result = m.mk_eq(l, r);
else

2
src/sat/smt/polysat_solver.h
View file

@ -187,6 +187,8 @@ namespace polysat {
void axiomatize_bv2int(app* e, expr* x);
void axioms_for_extract(app* e);
void axioms_for_concat(app* e);
expr_ref mk_ite(expr* c, expr* t, expr* e);
expr_ref mk_ule(expr* l, expr* r);
expr* rotate_left(app* e, unsigned n, expr* x);
unsigned m_delayed_axioms_qhead = 0;
ptr_vector<app> m_delayed_axioms;