mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

add comment on derivation of bound

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-18 17:39:59 -10:00 • committed by Lev Nachmanson
parent dd19b381d8
commit f181e3aa81
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/lp/bound_analyzer_on_row.h
View file

@ -171,6 +171,28 @@ namespace lp {
}
}
// total := - sum_{a_j > 0} a_j * ub(x_j) - sum_{a_j < 0} a_j * lb(x_j)
//
// for each a_j* x_j in row,
// bound := total / a_j + ub(x_j) = (total + (a_j * ub(x_j))) / a_j if a_j > 0
// bound := total / a_j + lb(x_j) = (total + (a_j * lb(x_j))) / a_j if a_j < 0
// example
// 3x + 2y + z = 0
// x <= 1, y <= 2, z <= 1
// total = - (3*1 + 2*2 + 1) = -8
// bound := -8/1 + 1 = -7
// => z >= -7
// If all variables are integer (or if x_j is integer).
// let K = lcm(a_j)
//
// totalK = K*total
// sum without x_j: bound := totalK + K * a_j * ub(x_j)
// K*a_j x >= bound
// x >= ceil(bound / K*a_j) = ceil ((total + a_j * ub(x_j)) / a_j) = ceil ((total / a_j) + ub(x_j))
//
void limit_all_monoids_from_below() {
int strict = 0;
m_total = m_rs.x;