mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

detect bounds from mod

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

18
src/ast/simplifiers/bound_manager.cpp
View file

@ -193,13 +193,11 @@ void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_
}
bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
expr* x, *y;
if (!m().is_eq(f, x, y)) {
expr* x, *y, *z, *u;
if (!m().is_eq(f, x, y))
return false;
}
if (!is_uninterp_const(x)) {
if (!is_uninterp_const(x))
std::swap(x, y);
}
numeral n;
bool is_int;
if (is_uninterp_const(x) && is_numeral(y, n, is_int)) {
@ -207,9 +205,15 @@ bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
insert_upper(x, false, n, d);
return true;
}
else {
return false;
// x = y mod n => 0 <= x < n
if (m_util.is_mod(y, z, u) && is_numeral(u, n, is_int) && n > 0) {
insert_lower(x, false, rational::zero(), d);
insert_upper(x, false, n - 1, d);
return true;
}
return false;
}
bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {