mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

roll back add_var api

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-11-08 11:00:12 -08:00
parent 4fa38b5aa2
commit 1d51c5689e
6 changed files with 122 additions and 138 deletions
Download patch file Download diff file Expand all files Collapse all files

110
src/util/lp/lar_solver.cpp
View file

@ -28,6 +28,7 @@ void clear() {lp_assert(false); // not implemented
lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
m_infeasible_column(-1),
m_terms_start_index(1000000),
m_mpq_lar_core_solver(m_settings, *this),
m_int_solver(nullptr)
@ -302,6 +303,15 @@ lp_status lar_solver::solve() {
return m_status;
}
void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{
// this is the case when the lower bound is in conflict with the upper one
const ul_pair & ul = m_columns_to_ul_pairs[m_infeasible_column];
evidence.push_justification(ul.upper_bound_witness(), numeric_traits<mpq>::one());
evidence.push_justification(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
}
unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); }
vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
@ -314,6 +324,7 @@ void lar_solver::push() {
m_simplex_strategy = m_settings.simplex_strategy();
m_simplex_strategy.push();
m_columns_to_ul_pairs.push();
m_infeasible_column.push();
m_mpq_lar_core_solver.push();
m_term_count = m_terms.size();
m_term_count.push();
@ -340,7 +351,7 @@ void lar_solver::pop(unsigned k) {
TRACE("int_solver", tout << "pop" << std::endl;);
TRACE("lar_solver", tout << "k = " << k << std::endl;);
restore_rounded_columns(); // if it is not done now, the basis changes and restore_rounded_columns would now work
m_infeasible_column_index.pop(k);
m_infeasible_column.pop(k);
unsigned n = m_columns_to_ul_pairs.peek_size(k);
m_var_register.shrink(n);
if (m_settings.use_tableau()) {
@ -1197,6 +1208,10 @@ bool lar_solver::has_value(var_index var, mpq& value) const {
void lar_solver::get_infeasibility_explanation(explanation& exp) const {
exp.clear();
if (m_infeasible_column != -1) {
fill_explanation_from_infeasible_column(exp);
return;
}
if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) {
return;
}
@ -1767,17 +1782,17 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig
return right_side.is_int();
}
constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side, explanation& e) {
constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
TRACE("lar_solver", tout << "j = " << j << std::endl;);
constraint_index ci = m_constraints.size();
if (!is_term(j)) { // j is a var
lp_assert(bound_is_integer_for_integer_column(j, right_side));
auto vc = new lar_var_constraint(j, kind, right_side);
m_constraints.push_back(vc);
update_column_type_and_bound(j, kind, right_side, ci, e);
update_column_type_and_bound(j, kind, right_side, ci);
}
else {
add_var_bound_on_constraint_for_term(j, kind, right_side, ci, e);
add_var_bound_on_constraint_for_term(j, kind, right_side, ci);
}
lp_assert(sizes_are_correct());
return ci;
@ -1803,43 +1818,42 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq &
}
void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side,
constraint_index constr_index,
explanation& e) {
constraint_index constr_index) {
if (column_has_upper_bound(j))
update_column_type_and_bound_with_ub(j, kind, right_side, constr_index, e);
update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
else
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index, e);
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
}
void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation & e) {
void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lp_assert(is_term(j));
unsigned adjusted_term_index = adjust_term_index(j);
// lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
unsigned term_j;
if (m_var_register.external_is_used(j, term_j)) {
m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
update_column_type_and_bound(term_j, kind, right_side, ci, e);
update_column_type_and_bound(term_j, kind, right_side, ci);
}
else {
add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side, e);
add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
}
}
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm, explanation & e) {
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
vector<std::pair<mpq, var_index>> left_side;
substitute_terms_in_linear_expression(left_side_with_terms, left_side);
unsigned term_index = add_term(left_side);
constraint_index ci = m_constraints.size();
add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci, e);
add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci);
return ci;
}
void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
lconstraint_kind kind, const mpq & right_side, explanation & e) {
lconstraint_kind kind, const mpq & right_side) {
add_row_from_term_no_constraint(term, term_j);
unsigned j = A_r().column_count() - 1;
update_column_type_and_bound(j, kind, right_side, m_constraints.size(), e);
update_column_type_and_bound(j, kind, right_side, m_constraints.size());
m_constraints.push_back(new lar_term_constraint(term, kind, right_side));
lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
}
@ -1925,26 +1939,26 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
lp_assert(A.is_correct());
}
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) {
SASSERT(column_has_upper_bound(j));
if (column_has_lower_bound(j)) {
update_bound_with_ub_lb(j, kind, right_side, constraint_index, e);
update_bound_with_ub_lb(j, kind, right_side, constraint_index);
} else {
update_bound_with_ub_no_lb(j, kind, right_side, constraint_index, e);
update_bound_with_ub_no_lb(j, kind, right_side, constraint_index);
}
}
void lar_solver::update_column_type_and_bound_with_no_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_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index) {
SASSERT(!column_has_upper_bound(j));
if (column_has_lower_bound(j)) {
update_bound_with_no_ub_lb(j, kind, right_side, constraint_index, e);
update_bound_with_no_ub_lb(j, kind, right_side, constraint_index);
} else {
update_bound_with_no_ub_no_lb(j, kind, right_side, constraint_index, e);
update_bound_with_no_ub_no_lb(j, kind, right_side, constraint_index);
}
}
void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation& e) {
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));
mpq y_of_bound(0);
@ -1955,9 +1969,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_lower_bound_witness(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;
@ -1971,9 +1983,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_upper_bound_witness(j));
set_infeasible_column(j);
}
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
@ -1987,15 +1997,8 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
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]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_upper_bound_witness(j));
}
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_lower_bound_witness(j));
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);
@ -2008,7 +2011,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
lp_unreachable();
}
}
void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation& e) {
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));
mpq y_of_bound(0);
@ -2019,9 +2022,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_lower_bound_witness(j));
set_infeasible_column(j);
}
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
@ -2046,9 +2047,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_lower_bound_witness(j));
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
@ -2064,7 +2063,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
}
void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation& e) {
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));
mpq y_of_bound(0);
@ -2086,9 +2085,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_upper_bound_witness(j));
set_infeasible_column(j);
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
m_columns_with_changed_bound.insert(j);
@ -2100,11 +2097,9 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_status(lp_status::INFEASIBLE);
e.push_justification(ci);
e.push_justification(get_column_upper_bound_witness(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;
@ -2116,7 +2111,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
lp_unreachable();
}
}
void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation&) {
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));
m_columns_with_changed_bound.insert(j);
@ -2180,19 +2175,18 @@ bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& d
return false;
}
}
explanation e;
TRACE("cube", tout << "can tighten";);
if (slv.column_has_upper_bound(j)) {
if (!is_zero(delta.y))
add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x, e);
add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x);
else
add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x, e);
add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x);
}
if (slv.column_has_lower_bound(j)) {
if (!is_zero(delta.y))
add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x, e);
add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x);
else
add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x, e);
add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x);
}
return true;
}

29
src/util/lp/lar_solver.h
View file

@ -193,25 +193,29 @@ public:
void add_basic_var_to_core_fields();
constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side, explanation&) ;
constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ;
bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side);
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs);
void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&);
void update_column_type_and_bound(var_index 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);
void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation&);
void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
void set_infeasible_column(unsigned j) {
set_status(lp_status::INFEASIBLE);
m_infeasible_column = j;
}
void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
lconstraint_kind kind, const mpq & right_side, explanation&);
lconstraint_kind kind, const mpq & right_side);
unsigned row_of_basic_column(unsigned) const;
@ -313,6 +317,9 @@ public:
lp_status solve();
void fill_explanation_from_infeasible_column(explanation & evidence) const;
unsigned get_total_iterations() const;
// see http://research.microsoft.com/projects/z3/smt07.pdf
// This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find
@ -442,7 +449,7 @@ public:
bool all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side);
constraint_index add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm, explanation &);
constraint_index add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm);
bool all_constraints_hold() const;
bool constraint_holds(const lar_base_constraint & constr, std::unordered_map<var_index, mpq> & var_map) const;
bool the_relations_are_of_same_type(const vector<std::pair<mpq, unsigned>> & evidence, lconstraint_kind & the_kind_of_sum) const;

12
src/util/lp/mps_reader.h
View file

@ -817,7 +817,6 @@ public:
}
void fill_lar_solver_on_row(row * row, lar_solver *solver) {
explanation e;
if (row->m_name != m_cost_row_name) {
auto kind = get_lar_relation_from_row(row->m_type);
vector<std::pair<mpq, var_index>> ls;
@ -825,7 +824,7 @@ public:
var_index i = solver->add_var(get_var_index(s.first), false);
ls.push_back(std::make_pair(s.second, i));
}
solver->add_constraint(ls, kind, row->m_right_side, e);
solver->add_constraint(ls, kind, row->m_right_side);
} else {
// ignore the cost row
}
@ -842,24 +841,21 @@ public:
vector<std::pair<mpq, var_index>> ls;
var_index i = solver->add_var(col->m_index, false);
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
explanation e;
solver->add_constraint(ls, GE, b->m_low, e);
solver->add_constraint(ls, GE, b->m_low);
}
void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
explanation e;
solver->add_constraint(ls, LE, b->m_upper, e);
solver->add_constraint(ls, LE, b->m_upper);
}
void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
explanation e;
solver->add_constraint(ls, EQ, b->m_fixed_value, e);
solver->add_constraint(ls, EQ, b->m_fixed_value);
}
void fill_lar_solver_on_columns(lar_solver * solver) {