From 88269edd4b9e50005f03f6b675ec642444f63727 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Nov 2025 07:56:42 -0800 Subject: [PATCH] fixup bv operators Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 6 ++++- src/ast/rewriter/arith_rewriter.cpp | 12 ++++++++++ src/smt/theory_lra.cpp | 35 +++++++++++++++++++++-------- 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index db927e431..4bd82ea47 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -636,6 +636,10 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("/0",OP_DIV0)); op_names.push_back(builtin_name("div0",OP_IDIV0)); op_names.push_back(builtin_name("mod0",OP_MOD0)); + op_names.push_back(builtin_name(bv_symbol(OP_ARITH_BAND).bare_str(), OP_ARITH_BAND)); + op_names.push_back(builtin_name(bv_symbol(OP_ARITH_SHL).bare_str(), OP_ARITH_SHL)); + op_names.push_back(builtin_name(bv_symbol(OP_ARITH_LSHR).bare_str(), OP_ARITH_LSHR)); + op_names.push_back(builtin_name(bv_symbol(OP_ARITH_ASHR).bare_str(), OP_ARITH_ASHR)); } } @@ -643,7 +647,7 @@ bool arith_decl_plugin::is_value(app * e) const { return is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) || - is_app_of(e, m_family_id, OP_PI) || + is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_E); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d5ad70a1f..14c95f8f2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1600,8 +1600,13 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr N = rational::power_of_two(sz); if (is_num_x) x = mod(x, N); + if (is_num_y && y >= sz) { + result = m_util.mk_int(0); + return BR_DONE; + } if (is_num_y) y = mod(y, N); + if (is_num_x && x == 0) { result = m_util.mk_int(0); return BR_DONE; @@ -1619,6 +1624,13 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr } return BR_DONE; } + + if (is_num_y) { + result = m_util.mk_mod(arg1, m_util.mk_int(N)); + //result = arg1; // unsound + result = m_util.mk_idiv(result, m_util.mk_int(rational::power_of_two(y.get_unsigned()))); + return BR_DONE; + } return BR_FAILED; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 475dcfc79..49b09d5a5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2522,11 +2522,15 @@ public: found_unsupported(n); return true; } - rational N = rational::power_of_two(sz); + rational N = rational::power_of_two(sz), r; valx = mod(valx, N); valy = mod(valy, N); expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); + if (a.is_numeral(_x, r)) + x = a.mk_int(mod(r, N)); + if (a.is_numeral(_y, r)) + y = a.mk_int(mod(r, N)); SASSERT(0 <= valn && valn < N); // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. @@ -2559,9 +2563,12 @@ public: return true; unsigned k = valy.get_unsigned(); sat::literal eq = th.mk_eq(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)), false); + ctx().mark_as_relevant(eq); if (ctx().get_assignment(eq) == l_true) return true; - ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq); + sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false); + ctx().mark_as_relevant(y_eq_k); + ctx().mk_th_axiom(get_id(), ~y_eq_k, eq); IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n"); return false; } @@ -2571,10 +2578,12 @@ public: return true; unsigned k = valy.get_unsigned(); sat::literal eq = th.mk_eq(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))), false); + ctx().mark_as_relevant(eq); if (ctx().get_assignment(eq) == l_true) return true; - ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq); - IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n"); + sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false); + ctx().mark_as_relevant(y_eq_k); + ctx().mk_th_axiom(get_id(), ~y_eq_k, eq); return false; } if (a.is_ashr(n)) { @@ -2590,6 +2599,7 @@ public: // x < 0 & y = k -> n = (x div 2^k - 2^{N-k}) mod 2^N xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k))); eq = th.mk_eq(n, a.mk_mod(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), a.mk_int(N)), false); + ctx().mark_as_relevant(eq); if (ctx().get_assignment(eq) == l_true) return true; break; @@ -2597,6 +2607,7 @@ public: // x >= 0 & y = k -> n = x div 2^k xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k))); eq = th.mk_eq(n, xdiv2k, false); + ctx().mark_as_relevant(eq); if (ctx().get_assignment(eq) == l_true) return true; break; @@ -2604,7 +2615,9 @@ public: ctx().mark_as_relevant(signx); return false; } - ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), ~signx, eq); + sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false); + ctx().mark_as_relevant(y_eq_k); + ctx().mk_th_axiom(get_id(), ~y_eq_k, ~signx, eq); return false; } return true; @@ -2622,9 +2635,13 @@ public: unsigned sz = 0; expr* _x = nullptr, * _y = nullptr; VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y)); - rational N = rational::power_of_two(sz); + rational N = rational::power_of_two(sz), r; expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); + if (a.is_numeral(_x, r)) + x = a.mk_int(mod(r, N)); + if (a.is_numeral(_y, r)) + y = a.mk_int(mod(r, N)); // 0 <= n < 2^sz @@ -2657,9 +2674,9 @@ public: // y >= sz & x >= 2^{sz-1} => n = -1 // y = 0 => n = x auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); - ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0)))); - ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1)))); - ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0)))); + ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1)))); + ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x))); } else UNREACHABLE();