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

renaming

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-09-07 11:57:20 -07:00
parent 47b64e689c
commit c43b99daae
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1931,7 +1931,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_lower_bounds[j]) { if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column_and_witness(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return; if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
@ -1946,7 +1946,7 @@ 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 > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_infeasible_column_and_witness(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} else { } else {
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return; return;
@ -1962,10 +1962,10 @@ 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_upper_bounds[j]){ if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]){
set_infeasible_column_and_witness(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 < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column_and_witness(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
set_upper_bound_witness(j, dep); set_upper_bound_witness(j, dep);
@ -1995,7 +1995,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_lower_bounds[j]) { if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column_and_witness(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
@ -2020,7 +2020,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 < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column_and_witness(j, true, dep); set_crossed_bounds_column_and_deps(j, true, dep);
} }
else { else {
set_upper_bound_witness(j, dep); set_upper_bound_witness(j, dep);
@ -2059,7 +2059,7 @@ namespace lp {
{ {
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 > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_infeasible_column_and_witness(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} }
else { else {
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
@ -2073,7 +2073,7 @@ namespace lp {
{ {
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 > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_infeasible_column_and_witness(j, false, dep); set_crossed_bounds_column_and_deps(j, false, dep);
} }
else { else {
set_upper_bound_witness(j, dep); set_upper_bound_witness(j, dep);
@ -2360,7 +2360,7 @@ namespace lp {
// Otherwise the new asserted lower bound is is greater than the existing upper bound. // Otherwise the new asserted lower bound is is greater than the existing upper bound.
// dep is the reason for the new bound // dep is the reason for the new bound
void lar_solver::set_infeasible_column_and_witness(unsigned j, bool lower_bound, u_dependency* dep) { void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
SASSERT(m_crossed_bounds_deps == nullptr && m_crossed_bounds_deps == nullptr); SASSERT(m_crossed_bounds_deps == nullptr && m_crossed_bounds_deps == nullptr);
set_status(lp_status::INFEASIBLE); set_status(lp_status::INFEASIBLE);
m_crossed_bounds_column = j; m_crossed_bounds_column = j;

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

@ -164,7 +164,7 @@ class lar_solver : public column_namer {
void register_in_fixed_var_table(unsigned, unsigned&); void register_in_fixed_var_table(unsigned, unsigned&);
void remove_non_fixed_from_fixed_var_table(); void remove_non_fixed_from_fixed_var_table();
constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side); constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side);
void set_infeasible_column_and_witness(unsigned j, bool lower_bound, u_dependency* dep); void set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep);
constraint_index add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, constraint_index add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
lconstraint_kind kind, const mpq& right_side); lconstraint_kind kind, const mpq& right_side);
unsigned row_of_basic_column(unsigned) const; unsigned row_of_basic_column(unsigned) const;