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

detect bounds from mod

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-22 14:40:36 -08:00
parent 021ef699af
commit e2a6376ddf
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/arith/propagate_ineqs_tactic.cpp
View file

@ -226,6 +226,7 @@ struct propagate_ineqs_tactic::imp {
} }
expr * lhs = to_app(t)->get_arg(0); expr * lhs = to_app(t)->get_arg(0);
expr * rhs = to_app(t)->get_arg(1); expr * rhs = to_app(t)->get_arg(1);
expr* a, *b;
if (m_util.is_numeral(lhs)) { if (m_util.is_numeral(lhs)) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
if (k == LE) if (k == LE)
@ -235,6 +236,16 @@ struct propagate_ineqs_tactic::imp {
} }
rational c; rational c;
// x = y mod c => 0 <= x < c
if (k == EQ && m_util.is_mod(rhs, a, b) && m_util.is_numeral(b, c) && c > 0) {
a_var x = mk_linear_pol(lhs);
mpq c_prime;
nm.set(c_prime, (c-1).to_mpq());
bp.assert_lower(x, mpq(0), false);
bp.assert_upper(x, c_prime, false);
nm.del(c_prime);
return lhs == a;
}
if (!m_util.is_numeral(rhs, c)) if (!m_util.is_numeral(rhs, c))
return false; return false;
a_var x = mk_linear_pol(lhs); a_var x = mk_linear_pol(lhs);