mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix mbi arithmetic solver for lower bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-26 06:37:47 -07:00
parent 6804329661
commit bf4edef761
1 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/math/simplex/model_based_opt.cpp
View file

@ -52,7 +52,20 @@ namespace opt {
}
}
m_coeff = r.m_coeff;
if (r.m_type == opt::t_lt) m_coeff += m_div;
switch (r.m_type) {
case opt::t_lt:
m_coeff += m_div;
break;
case opt::t_le:
// for: ax >= t, then x := (t + a - 1) div a
if (m_div.is_pos()) {
m_coeff += m_div;
m_coeff -= rational::one();
}
break;
default:
break;
}
normalize();
SASSERT(m_div.is_pos());
}
@ -976,7 +989,7 @@ namespace opt {
// There are only upper or only lower bounds.
if (row_index == UINT_MAX) {
if (compute_def) {
if (lub_index != UINT_MAX) {
if (lub_index != UINT_MAX) {
result = solve_for(lub_index, x, true);
}
else if (glb_index != UINT_MAX) {
@ -998,11 +1011,6 @@ namespace opt {
SASSERT(lub_index != UINT_MAX);
SASSERT(glb_index != UINT_MAX);
if (compute_def) {
#if 0
def d1(m_rows[lub_index], x);
def d2(m_rows[glb_index], x);
result = (d1 + d2)/2;
#else
if (lub_size <= glb_size) {
result = def(m_rows[lub_index], x);
}
@ -1010,7 +1018,6 @@ namespace opt {
result = def(m_rows[glb_index], x);
}
m_var2value[x] = eval(result);
#endif
}
// The number of matching lower and upper bounds is small.