mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-07-05 12:58:23 -07:00
commit 14f69c6c01
4 changed files with 142 additions and 144 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/int_solver.cpp
View file

@ -103,6 +103,8 @@ namespace lp {
lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int());
// 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l.
rational d = u * t * x1;
// We can prove that x+alpha*d is integral,
// and any other delta, satisfying x+alpha*delta, is equal to d modulo a2.
delta_plus = mod(d, a2);
lp_assert(delta_plus > 0);
delta_minus = delta_plus - a2;

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

@ -1810,7 +1810,12 @@ namespace lp {
else
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
}
// clang-format on
void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
m_columns_with_changed_bounds.insert(j);
TRACE("lar_solver", tout << "column " << j << (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
}
// clang-format off
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
lconstraint_kind kind,
const mpq& right_side,
@ -1900,117 +1905,110 @@ namespace lp {
}
}
// clang-format on
void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed ||
m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed);
m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed);
mpq y_of_bound(0);
switch (kind) {
case LT:
y_of_bound = -1;
case LE:
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
}
break;
case GT:
y_of_bound = 1;
case GE:
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_infeasible_column(j);
}
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
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);
}
break;
case EQ:
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
break;
}
case LT:
y_of_bound = -1;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
} break;
case GT:
y_of_bound = 1;
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_infeasible_column(j);
}
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, ci);
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);
insert_to_columns_with_changed_bounds(j);
default:
UNREACHABLE();
} break;
case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
break;
}
default:
UNREACHABLE();
}
if (m_mpq_lar_core_solver.m_r_upper_bounds[j] == m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
}
}
// clang-format off
void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
mpq y_of_bound(0);
switch (kind) {
case LT:
y_of_bound = -1;
case LE:
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
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);
}
break;
case GT:
y_of_bound = 1;
case GE:
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
}
break;
case EQ:
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
case LT:
y_of_bound = -1;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
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);
insert_to_columns_with_changed_bounds(j);
} break;
case GT:
y_of_bound = 1;
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
} break;
case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
default:
UNREACHABLE();
}
default:
UNREACHABLE();
}
}
// clang-format off
void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
@ -2036,9 +2034,10 @@ namespace lp {
set_infeasible_column(j);
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
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);
insert_to_columns_with_changed_bounds(j);
}
break;
case EQ:
@ -2059,48 +2058,44 @@ namespace lp {
UNREACHABLE();
}
}
// clang-format on
void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
insert_to_columns_with_changed_bounds(j);
mpq y_of_bound(0);
switch (kind) {
case LT:
y_of_bound = -1;
case LE:
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound;
}
break;
case GT:
y_of_bound = 1;
case GE:
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
}
break;
case EQ:
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
}
case LT:
y_of_bound = -1;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound;
} break;
case GT:
y_of_bound = 1;
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
default:
UNREACHABLE();
} break;
case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
}
default:
UNREACHABLE();
}
insert_to_columns_with_changed_bounds(j);
}
// clang-format off
bool lar_solver::column_corresponds_to_term(unsigned j) const {
return tv::is_term(m_var_register.local_to_external(j));
}
@ -2204,8 +2199,8 @@ namespace lp {
}
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq& rs, constraint_index& ci, bool& upper_bound) const {
lp_assert(t.is_term())
unsigned j;
lp_assert(t.is_term());
unsigned j;
bool is_int;
if (!m_var_register.external_is_used(t.index(), j, is_int))
return false; // the term does not have a bound because it does not correspond to a column

3
src/math/lp/lar_solver.h
View file

@ -135,8 +135,7 @@ class lar_solver : public column_namer {
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); }
inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); }
inline void insert_to_columns_with_changed_bounds(unsigned j) { m_columns_with_changed_bounds.insert(j); }
void insert_to_columns_with_changed_bounds(unsigned j);
void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index, unsigned&);
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);
void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);

32
src/math/lp/lp_core_solver_base.h
View file

@ -56,7 +56,7 @@ private:
public:
bool current_x_is_feasible() const {
TRACE("feas",
if (m_inf_heap.size()) {
if (!m_inf_heap.empty()) {
tout << "column " << *m_inf_heap.begin() << " is infeasible" << std::endl;
print_column_info(*m_inf_heap.begin(), tout);
} else {
@ -310,8 +310,7 @@ public:
if (x < m_lower_bounds[j]) {
delta = m_lower_bounds[j] - x;
ret = true;;
}
if (x > m_upper_bounds[j]) {
} else if (x > m_upper_bounds[j]) {
delta = m_upper_bounds[j] - x;
ret = true;
}
@ -554,31 +553,34 @@ public:
}
void update_x(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
m_x[j] = v;
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << (column_is_feasible(j)? " feas":" non-feas") << "\n";);
}
void add_delta_to_x(unsigned j, const X & delta) {
TRACE("lar_solver", tout << "j = " << j << ", delta = " << delta << "\n";);
m_x[j] += delta;
}
// clang-format on
void add_delta_to_x(unsigned j, const X& delta) {
m_x[j] += delta;
TRACE("lar_solver", tout << "j = " << j << " v = " << m_x[j] << " delta = " << delta << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
}
// clang-format off
void track_column_feasibility(unsigned j) {
if (column_is_feasible(j))
remove_column_from_inf_heap(j);
else
insert_column_into_inf_heap(j);
}
void insert_column_into_inf_heap(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
if (!m_inf_heap.contains(j))
void insert_column_into_inf_heap(unsigned j) {
if (!m_inf_heap.contains(j)) {
m_inf_heap.insert(j);
TRACE("lar_solver", tout << "j = " << j << "\n";);
}
lp_assert(!column_is_feasible(j));
}
void remove_column_from_inf_heap(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
if (m_inf_heap.contains(j))
if (m_inf_heap.contains(j)) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
m_inf_heap.erase(j);
}
lp_assert(column_is_feasible(j));
}