mirror of
https://github.com/Z3Prover/z3
synced 2025-07-20 03:12:03 +00:00
process conflicts immediately aftep add_var_bound()
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev
Lev Nachmanson
parent
c9be7b89c1
commit
4fa38b5aa2
3 changed files with 4 additions and 308 deletions
|
|
@ -2302,7 +2302,7 @@ public:
|
||||||
int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
|
int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
|
||||||
(void)new_num_of_p;
|
(void)new_num_of_p;
|
||||||
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
|
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
|
||||||
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
|
if (is_infeasible()) {
|
||||||
set_conflict();
|
set_conflict();
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
|
|
@ -2960,7 +2960,7 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
|
void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
|
||||||
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
|
if (is_infeasible()) {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
scoped_internalize_state st(*this);
|
scoped_internalize_state st(*this);
|
||||||
|
|
@ -2993,8 +2993,8 @@ public:
|
||||||
else {
|
else {
|
||||||
ci = m_solver->add_var_bound(vi, k, b.get_value(), m_explanation);
|
ci = m_solver->add_var_bound(vi, k, b.get_value(), m_explanation);
|
||||||
}
|
}
|
||||||
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
|
if (is_infeasible()) {
|
||||||
NOT_IMPLEMENTED_YET();
|
set_conflict1();
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
TRACE("arith", tout << "v" << b.get_var() << "\n";);
|
TRACE("arith", tout << "v" << b.get_var() << "\n";);
|
||||||
|
|
|
||||||
|
|
@ -1925,180 +1925,6 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
|
||||||
lp_assert(A.is_correct());
|
lp_assert(A.is_correct());
|
||||||
}
|
}
|
||||||
|
|
||||||
void lar_solver::update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
|
|
||||||
mpq y_of_bound(0);
|
|
||||||
switch (kind) {
|
|
||||||
case LT:
|
|
||||||
y_of_bound = -1;
|
|
||||||
case LE:
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound;
|
|
||||||
lp_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound);
|
|
||||||
lp_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j);
|
|
||||||
{
|
|
||||||
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, constr_ind);
|
|
||||||
break;
|
|
||||||
case GT:
|
|
||||||
y_of_bound = 1;
|
|
||||||
case GE:
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
|
|
||||||
lp_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j);
|
|
||||||
{
|
|
||||||
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, constr_ind);
|
|
||||||
break;
|
|
||||||
case EQ:
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
|
|
||||||
set_upper_bound_witness(j, constr_ind);
|
|
||||||
set_lower_bound_witness(j, constr_ind);
|
|
||||||
break;
|
|
||||||
|
|
||||||
default:
|
|
||||||
lp_unreachable();
|
|
||||||
|
|
||||||
}
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
}
|
|
||||||
|
|
||||||
void lar_solver::update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci,
|
|
||||||
explanation& e) {
|
|
||||||
lp_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_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_upper_bounds()[j]) {
|
|
||||||
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case GT:
|
|
||||||
y_of_bound = 1;
|
|
||||||
case GE:
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::boxed;
|
|
||||||
{
|
|
||||||
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_columns_with_changed_bound.insert(j);
|
|
||||||
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
e.push_justification(ci);
|
|
||||||
e.push_justification(get_column_lower_bound_witness(j));
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
|
|
||||||
default:
|
|
||||||
lp_unreachable();
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
|
|
||||||
lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_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);
|
|
||||||
if (up < m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
}
|
|
||||||
|
|
||||||
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
if (m_mpq_lar_core_solver.m_r_lower_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j])
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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]) {
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
}
|
|
||||||
else if (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
}
|
|
||||||
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
default:
|
|
||||||
lp_unreachable();
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index, lp::explanation& e) {
|
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index, lp::explanation& e) {
|
||||||
SASSERT(column_has_upper_bound(j));
|
SASSERT(column_has_upper_bound(j));
|
||||||
if (column_has_lower_bound(j)) {
|
if (column_has_lower_bound(j)) {
|
||||||
|
|
@ -2332,127 +2158,6 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void lar_solver::update_lower_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
|
|
||||||
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);
|
|
||||||
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
|
|
||||||
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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]) {
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
|
|
||||||
m_columns_with_changed_bound.insert(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]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
|
|
||||||
}
|
|
||||||
m_columns_with_changed_bound.insert(j);
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
default:
|
|
||||||
lp_unreachable();
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void lar_solver::update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
|
|
||||||
lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_lower_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
|
|
||||||
lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_r_lower_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero()));
|
|
||||||
auto v = numeric_pair<mpq>(right_side, mpq(0));
|
|
||||||
|
|
||||||
mpq y_of_bound(0);
|
|
||||||
switch (kind) {
|
|
||||||
case LT:
|
|
||||||
if (v <= m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case LE:
|
|
||||||
{
|
|
||||||
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case GT:
|
|
||||||
{
|
|
||||||
if (v >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case GE:
|
|
||||||
{
|
|
||||||
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case EQ:
|
|
||||||
{
|
|
||||||
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_upper_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
|
|
||||||
m_status = lp_status::INFEASIBLE;
|
|
||||||
// m_infeasible_column_index = j;
|
|
||||||
set_lower_bound_witness(j, ci);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
default:
|
|
||||||
lp_unreachable();
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool lar_solver::column_corresponds_to_term(unsigned j) const {
|
bool lar_solver::column_corresponds_to_term(unsigned j) const {
|
||||||
return m_var_register.local_to_external(j) >= m_terms_start_index;
|
return m_var_register.local_to_external(j) >= m_terms_start_index;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -226,15 +226,6 @@ public:
|
||||||
// this fills the last row of A_d and sets the basis column: -1 in the last column of the row
|
// this fills the last row of A_d and sets the basis column: -1 in the last column of the row
|
||||||
void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls);
|
void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls);
|
||||||
|
|
||||||
void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind);
|
|
||||||
|
|
||||||
void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation &);
|
|
||||||
|
|
||||||
void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
|
|
||||||
void update_lower_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
|
|
||||||
|
|
||||||
void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
|
|
||||||
|
|
||||||
//end of init region
|
//end of init region
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue