mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
a60295020b
commit
c1ab7987f6
|
@ -378,7 +378,8 @@ namespace opt {
|
|||
}
|
||||
else if ((value == lub_val && r.m_type == opt::t_lt) ||
|
||||
(is_pos && value < lub_val) ||
|
||||
(!is_pos && value > lub_val)) {
|
||||
|
||||
(!is_pos && value > lub_val)) {
|
||||
m_above.push_back(bound_row_index);
|
||||
lub_val = value;
|
||||
bound_row_index = row_id;
|
||||
|
@ -794,7 +795,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
std::ostream& model_based_opt::display(std::ostream& out, row const& r) {
|
||||
out << (r.m_alive?"+":"-") << " ";
|
||||
out << (r.m_alive?"a":"d") << " ";
|
||||
display(out, r.m_vars, r.m_coeff);
|
||||
if (r.m_type == opt::t_mod) {
|
||||
out << r.m_type << " " << r.m_mod << " = 0; value: " << r.m_value << "\n";
|
||||
|
@ -1192,7 +1193,9 @@ namespace opt {
|
|||
SASSERT(a.is_pos());
|
||||
if (ty == t_lt) {
|
||||
SASSERT(compute_def);
|
||||
m_rows[row_id1].m_coeff += a;
|
||||
m_rows[row_id1].m_coeff += a;
|
||||
m_rows[row_id1].m_type = t_le;
|
||||
m_rows[row_id1].m_value += a;
|
||||
}
|
||||
if (m_var2is_int[x] && !a.is_one()) {
|
||||
row& r1 = m_rows[row_id1];
|
||||
|
@ -1208,19 +1211,19 @@ namespace opt {
|
|||
if (!visited.contains(row_id2)) {
|
||||
visited.insert(row_id2);
|
||||
b = get_coefficient(row_id2, x);
|
||||
if (!b.is_zero()) {
|
||||
row& dst = m_rows[row_id2];
|
||||
switch (dst.m_type) {
|
||||
case t_eq:
|
||||
case t_lt:
|
||||
case t_le:
|
||||
solve(row_id1, a, row_id2, x);
|
||||
break;
|
||||
case t_mod:
|
||||
// mod reduction already done.
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
if (b.is_zero())
|
||||
continue;
|
||||
row& dst = m_rows[row_id2];
|
||||
switch (dst.m_type) {
|
||||
case t_eq:
|
||||
case t_lt:
|
||||
case t_le:
|
||||
solve(row_id1, a, row_id2, x);
|
||||
break;
|
||||
case t_mod:
|
||||
// mod reduction already done.
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue