mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

use inlined functions

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-23 14:28:31 -07:00
parent 5cc57b8958
commit 7641393f8a
2 changed files with 34 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/column.h
View file

@ -44,9 +44,10 @@ class column {
public: public:
lar_term* term() const { return m_term; } lar_term* term() const { return m_term; }
u_dependency*& lower_bound_witness() { return m_lower_bound_witness; } void set_lower_bound_witness(u_dependency* d) { m_lower_bound_witness = d; }
void set_upper_bound_witness(u_dependency* d) { m_upper_bound_witness = d; }
u_dependency* lower_bound_witness() const { return m_lower_bound_witness; } u_dependency* lower_bound_witness() const { return m_lower_bound_witness; }
u_dependency*& upper_bound_witness() { return m_upper_bound_witness; }
u_dependency* upper_bound_witness() const { return m_upper_bound_witness; } u_dependency* upper_bound_witness() const { return m_upper_bound_witness; }
column() {} column() {}

66
src/math/lp/lar_solver.cpp
View file

@ -576,14 +576,14 @@ namespace lp {
void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) { void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) {
m_trail.push(vector_value_trail(m_columns, j)); m_trail.push(vector_value_trail(m_columns, j));
m_columns[j].upper_bound_witness() = dep; m_columns[j].set_upper_bound_witness(dep);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = high; m_mpq_lar_core_solver.m_r_upper_bounds[j] = high;
insert_to_columns_with_changed_bounds(j); insert_to_columns_with_changed_bounds(j);
} }
void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) { void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) {
m_trail.push(vector_value_trail(m_columns, j)); m_trail.push(vector_value_trail(m_columns, j));
m_columns[j].lower_bound_witness() = dep; m_columns[j].set_lower_bound_witness(dep);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j); insert_to_columns_with_changed_bounds(j);
} }
@ -2072,12 +2072,11 @@ namespace lp {
Z3_fallthrough; Z3_fallthrough;
case LE: { case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound); auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (up < get_lower_bound(j)) {
set_crossed_bounds_column_and_deps(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
impq const& old_up = m_mpq_lar_core_solver.m_r_upper_bounds[j]; if (up >= get_upper_bound(j))
if (up >= old_up)
return; return;
set_upper_bound_witness(j, dep, up); set_upper_bound_witness(j, dep, up);
} }
@ -2088,23 +2087,22 @@ namespace lp {
Z3_fallthrough; Z3_fallthrough;
case GE: { case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound); auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { if (low > get_upper_bound(j)) {
set_crossed_bounds_column_and_deps(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} }
else { else {
impq const& old_low = m_mpq_lar_core_solver.m_r_lower_bounds[j]; if (low < get_lower_bound(j))
if (low < old_low)
return; return;
set_lower_bound_witness(j, dep, low); set_lower_bound_witness(j, dep, low);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (low == get_upper_bound(j) ? column_type::fixed : column_type::boxed);
} }
break; break;
} }
case EQ: { case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>()); auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) if (v > get_upper_bound(j))
set_crossed_bounds_column_and_deps(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
else if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) else if (v < get_lower_bound(j))
set_crossed_bounds_column_and_deps(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
else { else {
set_upper_bound_witness(j, dep, v); set_upper_bound_witness(j, dep, v);
@ -2116,8 +2114,8 @@ namespace lp {
default: default:
UNREACHABLE(); UNREACHABLE();
} }
numeric_pair<mpq> const& lo = m_mpq_lar_core_solver.m_r_lower_bounds[j]; numeric_pair<mpq> const& lo = get_lower_bound(j);
numeric_pair<mpq> const& hi = m_mpq_lar_core_solver.m_r_upper_bounds[j]; numeric_pair<mpq> const& hi = get_upper_bound(j);
if (lo == hi) if (lo == hi)
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
} }
@ -2133,12 +2131,12 @@ namespace lp {
Z3_fallthrough; Z3_fallthrough;
case LE: { case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound); auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (up < get_lower_bound(j)) {
set_crossed_bounds_column_and_deps(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
set_upper_bound_witness(j, dep, up); set_upper_bound_witness(j, dep, up);
m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j] ? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (up == get_lower_bound(j) ? column_type::fixed : column_type::boxed);
} }
break; break;
} }
@ -2146,7 +2144,7 @@ namespace lp {
y_of_bound = 1; y_of_bound = 1;
case GE: { case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound); auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (low < get_lower_bound(j)) {
return; return;
} }
set_lower_bound_witness(j, dep, low); set_lower_bound_witness(j, dep, low);
@ -2154,7 +2152,7 @@ namespace lp {
} }
case EQ: { case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>()); auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (v < get_lower_bound(j)) {
set_crossed_bounds_column_and_deps(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
@ -2181,7 +2179,7 @@ namespace lp {
case LE: case LE:
{ {
auto up = numeric_pair<mpq>(right_side, y_of_bound); auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) if (up >= get_upper_bound(j))
return; return;
set_upper_bound_witness(j, dep, up); set_upper_bound_witness(j, dep, up);
} }
@ -2192,19 +2190,19 @@ namespace lp {
case GE: case GE:
{ {
auto low = numeric_pair<mpq>(right_side, y_of_bound); auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { if (low > get_upper_bound(j)) {
set_crossed_bounds_column_and_deps(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} }
else { else {
set_lower_bound_witness(j, dep, low); set_lower_bound_witness(j, dep, low);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (low == get_upper_bound(j) ? column_type::fixed : column_type::boxed);
} }
} }
break; break;
case EQ: case EQ:
{ {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>()); auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { if (v > get_upper_bound(j)) {
set_crossed_bounds_column_and_deps(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} }
else { else {
@ -2265,11 +2263,10 @@ namespace lp {
impq ivalue(value); impq ivalue(value);
auto& lcs = m_mpq_lar_core_solver; auto& lcs = m_mpq_lar_core_solver;
auto& slv = m_mpq_lar_core_solver.m_r_solver;
if (slv.column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue) if (column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue)
return false; return false;
if (slv.column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue) if (column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue)
return false; return false;
set_value_for_nbasic_column(j, ivalue); set_value_for_nbasic_column(j, ivalue);
@ -2279,27 +2276,26 @@ namespace lp {
bool lar_solver::tighten_term_bounds_by_delta(lpvar j, const impq& delta) { bool lar_solver::tighten_term_bounds_by_delta(lpvar j, const impq& delta) {
SASSERT(column_has_term(j)); SASSERT(column_has_term(j));
auto& slv = m_mpq_lar_core_solver.m_r_solver;
TRACE("cube", tout << "delta = " << delta << std::endl; TRACE("cube", tout << "delta = " << delta << std::endl;
m_int_solver->display_column(tout, j); ); m_int_solver->display_column(tout, j); );
if (slv.column_has_upper_bound(j) && slv.column_has_lower_bound(j)) { if (column_has_upper_bound(j) && column_has_lower_bound(j)) {
if (slv.m_upper_bounds[j] - delta < slv.m_lower_bounds[j] + delta) { if (get_upper_bound(j) - delta < get_lower_bound(j) + delta) {
TRACE("cube", tout << "cannot tighten, delta = " << delta;); TRACE("cube", tout << "cannot tighten, delta = " << delta;);
return false; return false;
} }
} }
TRACE("cube", tout << "can tighten";); TRACE("cube", tout << "can tighten";);
if (slv.column_has_upper_bound(j)) { if (column_has_upper_bound(j)) {
if (!is_zero(delta.y) || !is_zero(slv.m_upper_bounds[j].y)) if (!is_zero(delta.y) || !is_zero(get_upper_bound(j).y))
add_var_bound(j, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x); add_var_bound(j, lconstraint_kind::LT, get_upper_bound(j).x - delta.x);
else else
add_var_bound(j, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x); add_var_bound(j, lconstraint_kind::LE, get_upper_bound(j).x - delta.x);
} }
if (slv.column_has_lower_bound(j)) { if (column_has_lower_bound(j)) {
if (!is_zero(delta.y) || !is_zero(slv.m_lower_bounds[j].y)) if (!is_zero(delta.y) || !is_zero(get_lower_bound(j).y))
add_var_bound(j, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x); add_var_bound(j, lconstraint_kind::GT, get_lower_bound(j).x + delta.x);
else else
add_var_bound(j, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x); add_var_bound(j, lconstraint_kind::GE, get_lower_bound(j).x + delta.x);
} }
return true; return true;
} }