Skip to content

Commit 7641393

Browse files
NikolajBjornerNikolajBjorner
committed
use inlined functions
1 parent 5cc57b8 commit 7641393

File tree

2 files changed

+34
-37
lines changed

2 files changed

+34
-37
lines changed

‎src/math/lp/column.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,10 @@ class column {
4444
public:
4545
lar_term* term() const { return m_term; }
4646

47-
u_dependency*& lower_bound_witness() { return m_lower_bound_witness; }
47+
void set_lower_bound_witness(u_dependency* d) { m_lower_bound_witness = d; }
48+
void set_upper_bound_witness(u_dependency* d) { m_upper_bound_witness = d; }
49+
4850
u_dependency* lower_bound_witness() const { return m_lower_bound_witness; }
49-
u_dependency*& upper_bound_witness() { return m_upper_bound_witness; }
5051
u_dependency* upper_bound_witness() const { return m_upper_bound_witness; }
5152

5253
column() {}

‎src/math/lp/lar_solver.cpp‎

Lines changed: 31 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -576,14 +576,14 @@ namespace lp {
576576

577577
void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) {
578578
m_trail.push(vector_value_trail(m_columns, j));
579-
m_columns[j].upper_bound_witness() = dep;
579+
m_columns[j].set_upper_bound_witness(dep);
580580
m_mpq_lar_core_solver.m_r_upper_bounds[j] = high;
581581
insert_to_columns_with_changed_bounds(j);
582582
}
583583

584584
void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) {
585585
m_trail.push(vector_value_trail(m_columns, j));
586-
m_columns[j].lower_bound_witness() = dep;
586+
m_columns[j].set_lower_bound_witness(dep);
587587
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
588588
insert_to_columns_with_changed_bounds(j);
589589
}
@@ -2072,12 +2072,11 @@ namespace lp {
20722072
Z3_fallthrough;
20732073
case LE: {
20742074
auto up = numeric_pair<mpq>(right_side, y_of_bound);
2075-
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
2075+
if (up < get_lower_bound(j)) {
20762076
set_crossed_bounds_column_and_deps(j, true, dep);
20772077
}
20782078
else {
2079-
impq const& old_up = m_mpq_lar_core_solver.m_r_upper_bounds[j];
2080-
if (up >= old_up)
2079+
if (up >= get_upper_bound(j))
20812080
return;
20822081
set_upper_bound_witness(j, dep, up);
20832082
}
@@ -2088,23 +2087,22 @@ namespace lp {
20882087
Z3_fallthrough;
20892088
case GE: {
20902089
auto low = numeric_pair<mpq>(right_side, y_of_bound);
2091-
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
2090+
if (low > get_upper_bound(j)) {
20922091
set_crossed_bounds_column_and_deps(j, false, dep);
20932092
}
20942093
else {
2095-
impq const& old_low = m_mpq_lar_core_solver.m_r_lower_bounds[j];
2096-
if (low < old_low)
2094+
if (low < get_lower_bound(j))
20972095
return;
20982096
set_lower_bound_witness(j, dep, low);
2099-
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);
2097+
m_mpq_lar_core_solver.m_column_types[j] = (low == get_upper_bound(j) ? column_type::fixed : column_type::boxed);
21002098
}
21012099
break;
21022100
}
21032101
case EQ: {
21042102
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
2105-
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j])
2103+
if (v > get_upper_bound(j))
21062104
set_crossed_bounds_column_and_deps(j, false, dep);
2107-
else if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j])
2105+
else if (v < get_lower_bound(j))
21082106
set_crossed_bounds_column_and_deps(j, true, dep);
21092107
else {
21102108
set_upper_bound_witness(j, dep, v);
@@ -2116,8 +2114,8 @@ namespace lp {
21162114
default:
21172115
UNREACHABLE();
21182116
}
2119-
numeric_pair<mpq> const& lo = m_mpq_lar_core_solver.m_r_lower_bounds[j];
2120-
numeric_pair<mpq> const& hi = m_mpq_lar_core_solver.m_r_upper_bounds[j];
2117+
numeric_pair<mpq> const& lo = get_lower_bound(j);
2118+
numeric_pair<mpq> const& hi = get_upper_bound(j);
21212119
if (lo == hi)
21222120
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
21232121
}
@@ -2133,28 +2131,28 @@ namespace lp {
21332131
Z3_fallthrough;
21342132
case LE: {
21352133
auto up = numeric_pair<mpq>(right_side, y_of_bound);
2136-
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
2134+
if (up < get_lower_bound(j)) {
21372135
set_crossed_bounds_column_and_deps(j, true, dep);
21382136
}
21392137
else {
21402138
set_upper_bound_witness(j, dep, up);
2141-
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);
2139+
m_mpq_lar_core_solver.m_column_types[j] = (up == get_lower_bound(j) ? column_type::fixed : column_type::boxed);
21422140
}
21432141
break;
21442142
}
21452143
case GT:
21462144
y_of_bound = 1;
21472145
case GE: {
21482146
auto low = numeric_pair<mpq>(right_side, y_of_bound);
2149-
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
2147+
if (low < get_lower_bound(j)) {
21502148
return;
21512149
}
21522150
set_lower_bound_witness(j, dep, low);
21532151
break;
21542152
}
21552153
case EQ: {
21562154
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
2157-
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
2155+
if (v < get_lower_bound(j)) {
21582156
set_crossed_bounds_column_and_deps(j, true, dep);
21592157
}
21602158
else {
@@ -2181,7 +2179,7 @@ namespace lp {
21812179
case LE:
21822180
{
21832181
auto up = numeric_pair<mpq>(right_side, y_of_bound);
2184-
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j])
2182+
if (up >= get_upper_bound(j))
21852183
return;
21862184
set_upper_bound_witness(j, dep, up);
21872185
}
@@ -2192,19 +2190,19 @@ namespace lp {
21922190
case GE:
21932191
{
21942192
auto low = numeric_pair<mpq>(right_side, y_of_bound);
2195-
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
2193+
if (low > get_upper_bound(j)) {
21962194
set_crossed_bounds_column_and_deps(j, false, dep);
21972195
}
21982196
else {
21992197
set_lower_bound_witness(j, dep, low);
2200-
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);
2198+
m_mpq_lar_core_solver.m_column_types[j] = (low == get_upper_bound(j) ? column_type::fixed : column_type::boxed);
22012199
}
22022200
}
22032201
break;
22042202
case EQ:
22052203
{
22062204
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
2207-
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
2205+
if (v > get_upper_bound(j)) {
22082206
set_crossed_bounds_column_and_deps(j, false, dep);
22092207
}
22102208
else {
@@ -2265,11 +2263,10 @@ namespace lp {
22652263

22662264
impq ivalue(value);
22672265
auto& lcs = m_mpq_lar_core_solver;
2268-
auto& slv = m_mpq_lar_core_solver.m_r_solver;
22692266

2270-
if (slv.column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue)
2267+
if (column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue)
22712268
return false;
2272-
if (slv.column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue)
2269+
if (column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue)
22732270
return false;
22742271

22752272
set_value_for_nbasic_column(j, ivalue);
@@ -2279,27 +2276,26 @@ namespace lp {
22792276

22802277
bool lar_solver::tighten_term_bounds_by_delta(lpvar j, const impq& delta) {
22812278
SASSERT(column_has_term(j));
2282-
auto& slv = m_mpq_lar_core_solver.m_r_solver;
22832279
TRACE("cube", tout << "delta = " << delta << std::endl;
22842280
m_int_solver->display_column(tout, j); );
2285-
if (slv.column_has_upper_bound(j) && slv.column_has_lower_bound(j)) {
2286-
if (slv.m_upper_bounds[j] - delta < slv.m_lower_bounds[j] + delta) {
2281+
if (column_has_upper_bound(j) && column_has_lower_bound(j)) {
2282+
if (get_upper_bound(j) - delta < get_lower_bound(j) + delta) {
22872283
TRACE("cube", tout << "cannot tighten, delta = " << delta;);
22882284
return false;
22892285
}
22902286
}
22912287
TRACE("cube", tout << "can tighten";);
2292-
if (slv.column_has_upper_bound(j)) {
2293-
if (!is_zero(delta.y) || !is_zero(slv.m_upper_bounds[j].y))
2294-
add_var_bound(j, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x);
2288+
if (column_has_upper_bound(j)) {
2289+
if (!is_zero(delta.y) || !is_zero(get_upper_bound(j).y))
2290+
add_var_bound(j, lconstraint_kind::LT, get_upper_bound(j).x - delta.x);
22952291
else
2296-
add_var_bound(j, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x);
2292+
add_var_bound(j, lconstraint_kind::LE, get_upper_bound(j).x - delta.x);
22972293
}
2298-
if (slv.column_has_lower_bound(j)) {
2299-
if (!is_zero(delta.y) || !is_zero(slv.m_lower_bounds[j].y))
2300-
add_var_bound(j, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x);
2294+
if (column_has_lower_bound(j)) {
2295+
if (!is_zero(delta.y) || !is_zero(get_lower_bound(j).y))
2296+
add_var_bound(j, lconstraint_kind::GT, get_lower_bound(j).x + delta.x);
23012297
else
2302-
add_var_bound(j, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x);
2298+
add_var_bound(j, lconstraint_kind::GE, get_lower_bound(j).x + delta.x);
23032299
}
23042300
return true;
23052301
}

0 commit comments

Comments
 (0)