mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix the race in add_var_bound and add_def_constraint

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-12 12:27:25 -07:00
parent fe0e042e40
commit 06826adec3
3 changed files with 63 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -18,7 +18,7 @@ void clear() {lp_assert(false); // not implemented
} }
lar_solver::lar_solver(const std::function<void(unsigned, unsigned)>& report_equality_of_fixed_vars) : lar_solver::lar_solver() :
m_status(lp_status::UNKNOWN), m_status(lp_status::UNKNOWN),
m_crossed_bounds_column(-1), m_crossed_bounds_column(-1),
m_mpq_lar_core_solver(m_settings, *this), m_mpq_lar_core_solver(m_settings, *this),
@ -26,9 +26,7 @@ lar_solver::lar_solver(const std::function<void(unsigned, unsigned)>& report_equ
m_need_register_terms(false), m_need_register_terms(false),
m_var_register(false), m_var_register(false),
m_term_register(true), m_term_register(true),
m_constraints(*this), m_constraints(*this) {}
m_report_equality_of_fixed_vars(report_equality_of_fixed_vars)
{}
void lar_solver::set_track_pivoted_rows(bool v) { void lar_solver::set_track_pivoted_rows(bool v) {
m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr;
@ -1718,6 +1716,12 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig
return right_side.is_int(); return right_side.is_int();
} }
constraint_index lar_solver::add_var_bound_check_on_equal(var_index j, lconstraint_kind kind, const mpq & right_side, var_index& equal_var) {
constraint_index ci = mk_var_bound(j, kind, right_side);
activate_check_on_equal(ci, equal_var);
return ci;
}
constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
constraint_index ci = mk_var_bound(j, kind, right_side); constraint_index ci = mk_var_bound(j, kind, right_side);
activate(ci); activate(ci);
@ -1735,10 +1739,11 @@ void lar_solver::remove_non_fixed_from_fixed_var_table() {
m_fixed_var_table.erase(p); m_fixed_var_table.erase(p);
} }
void lar_solver::register_in_fixed_var_table(unsigned j) { void lar_solver::register_in_fixed_var_table(unsigned j, unsigned & equal_to_j) {
SASSERT(column_is_fixed(j)); SASSERT(column_is_fixed(j));
equal_to_j = null_lpvar;
const impq& bound = get_lower_bound(j); const impq& bound = get_lower_bound(j);
if (bound.y.is_zero() == false) if (!bound.y.is_zero())
return; return;
value_sort_pair key(bound.x, column_is_int(j)); value_sort_pair key(bound.x, column_is_int(j));
@ -1748,10 +1753,16 @@ void lar_solver::register_in_fixed_var_table(unsigned j) {
return; return;
} }
SASSERT(column_is_fixed(k)); SASSERT(column_is_fixed(k));
if (j != k && column_is_int(j) == column_is_int(k)) if (j != k && column_is_int(j) == column_is_int(k)) {
m_report_equality_of_fixed_vars( equal_to_j = column_to_reported_index(k);
column_to_reported_index(j), TRACE("lar_solver", tout << "found equal column k = " << k <<
column_to_reported_index(k)); ", external = " << equal_to_j << "\n";);
}
}
void lar_solver::activate_check_on_equal(constraint_index ci, unsigned & equal_column) {
auto const& c = m_constraints[ci];
update_column_type_and_bound_check_on_equal(c.column(), c.kind(), c.rhs(), ci, equal_column);
} }
void lar_solver::activate(constraint_index ci) { void lar_solver::activate(constraint_index ci) {
@ -1817,7 +1828,7 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq &
} }
} }
void lar_solver::update_column_type_and_bound(var_index j, void lar_solver::update_column_type_and_bound(unsigned j,
lconstraint_kind kind, lconstraint_kind kind,
const mpq & right_side, const mpq & right_side,
constraint_index constr_index) { constraint_index constr_index) {
@ -1826,8 +1837,17 @@ void lar_solver::update_column_type_and_bound(var_index j,
update_column_type_and_bound_with_ub(j, kind, right_side, constr_index); update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
else else
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
}
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
lconstraint_kind kind,
const mpq & right_side,
constraint_index constr_index,
unsigned& equal_to_j) {
update_column_type_and_bound(j, kind, right_side, constr_index);
equal_to_j = null_lpvar;
if (column_is_fixed(j)) { if (column_is_fixed(j)) {
register_in_fixed_var_table(j); register_in_fixed_var_table(j, equal_to_j);
} }
} }

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

@ -109,7 +109,6 @@ class lar_solver : public column_namer {
unsigned, unsigned,
value_sort_pair_hash, value_sort_pair_hash,
default_eq<value_sort_pair>> m_fixed_var_table; default_eq<value_sort_pair>> m_fixed_var_table;
std::function <void(unsigned, unsigned)> m_report_equality_of_fixed_vars;
// end of fields // end of fields
////////////////// methods //////////////////////////////// ////////////////// methods ////////////////////////////////
@ -143,14 +142,15 @@ class lar_solver : public column_namer {
const impq& get_value(column_index const& j) const { return get_column_value(j); } const impq& get_value(column_index const& j) const { return get_column_value(j); }
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_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); 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_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_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_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_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 update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
void register_in_fixed_var_table(var_index); 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);
inline void set_infeasible_column(unsigned j) { inline void set_infeasible_column(unsigned j) {
@ -342,7 +342,8 @@ public:
} }
// lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
void activate(constraint_index ci); void activate_check_on_equal(constraint_index, var_index&);
void activate(constraint_index);
void random_update(unsigned sz, var_index const * vars); void random_update(unsigned sz, var_index const * vars);
template <typename T> template <typename T>
void propagate_bounds_for_touched_rows(lp_bound_propagator<T> & bp) { void propagate_bounds_for_touched_rows(lp_bound_propagator<T> & bp) {
@ -361,7 +362,9 @@ public:
bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side); bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i); var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i);
void register_existing_terms(); void register_existing_terms();
constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ; constraint_index add_var_bound(var_index, lconstraint_kind, const mpq &);
constraint_index add_var_bound_check_on_equal(var_index, lconstraint_kind, const mpq &, var_index&);
var_index add_var(unsigned ext_j, bool is_integer); var_index add_var(unsigned ext_j, bool is_integer);
void set_cut_strategy(unsigned cut_frequency); void set_cut_strategy(unsigned cut_frequency);
inline unsigned column_count() const { return A_r().column_count(); } inline unsigned column_count() const { return A_r().column_count(); }
@ -593,7 +596,7 @@ public:
void fill_explanation_from_crossed_bounds_column(explanation & evidence) const; void fill_explanation_from_crossed_bounds_column(explanation & evidence) const;
bool term_is_used_as_row(unsigned term) const; bool term_is_used_as_row(unsigned term) const;
bool tighten_term_bounds_by_delta(tv const& t, const impq&); bool tighten_term_bounds_by_delta(tv const& t, const impq&);
lar_solver(const std::function <void(unsigned, unsigned)>& report_equality_of_fixed_vars); lar_solver();
void set_track_pivoted_rows(bool v); void set_track_pivoted_rows(bool v);
bool get_track_pivoted_rows() const; bool get_track_pivoted_rows() const;
virtual ~lar_solver(); virtual ~lar_solver();

33
src/smt/theory_lra.cpp
View file

@ -338,8 +338,8 @@ class theory_lra::imp {
theory_var v = mk_var(cnst); theory_var v = mk_var(cnst);
var = lp().add_var(v, is_int); var = lp().add_var(v, is_int);
lp().push(); lp().push();
add_def_constraint(lp().add_var_bound(var, lp::GE, rational(c))); add_def_constraint_and_equality(var, lp::GE, rational(c));
add_def_constraint(lp().add_var_bound(var, lp::LE, rational(c))); add_def_constraint_and_equality(var, lp::LE, rational(c));
TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";); TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";);
return var; return var;
} }
@ -771,6 +771,17 @@ class theory_lra::imp {
return lp().get_status() == lp::lp_status::INFEASIBLE; return lp().get_status() == lp::lp_status::INFEASIBLE;
} }
void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind,
const rational& bound) {
lpvar vi_equal;
lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal);
add_def_constraint(ci);
if (vi_equal != lp::null_lpvar) {
report_equality_of_fixed_vars(vi, vi_equal);
}
}
void internalize_eq(theory_var v1, theory_var v2) { void internalize_eq(theory_var v1, theory_var v2) {
app_ref term(m.mk_fresh_const("eq", a.mk_real()), m); app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
scoped_internalize_state st(*this); scoped_internalize_state st(*this);
@ -780,12 +791,12 @@ class theory_lra::imp {
st.coeffs().push_back(rational::minus_one()); st.coeffs().push_back(rational::minus_one());
theory_var z = internalize_linearized_def(term, st); theory_var z = internalize_linearized_def(term, st);
lpvar vi = register_theory_var_in_lar_solver(z); lpvar vi = register_theory_var_in_lar_solver(z);
add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero())); add_def_constraint_and_equality(vi, lp::LE, rational::zero());
if (is_infeasible()) { if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";); IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here? // process_conflict(); // exit here?
} }
add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); add_def_constraint_and_equality(vi, lp::GE, rational::zero());
if (is_infeasible()) { if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";); IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here? // process_conflict(); // exit here?
@ -885,8 +896,8 @@ class theory_lra::imp {
} }
if (m_left_side.empty()) { if (m_left_side.empty()) {
vi = lp().add_var(v, a.is_int(term)); vi = lp().add_var(v, a.is_int(term));
add_def_constraint(lp().add_var_bound(vi, lp::GE, rational(0))); add_def_constraint_and_equality(vi, lp::GE, rational(0));
add_def_constraint(lp().add_var_bound(vi, lp::LE, rational(0))); add_def_constraint_and_equality(vi, lp::LE, rational(0));
} }
else { else {
vi = lp().add_term(m_left_side, v); vi = lp().add_term(m_left_side, v);
@ -937,7 +948,7 @@ public:
if (m_solver) return; if (m_solver) return;
reset_variable_values(); reset_variable_values();
m_solver = alloc(lp::lar_solver, [&](unsigned j, unsigned k) { report_equality_of_fixed_vars(j, k); }); m_solver = alloc(lp::lar_solver);
// initialize 0, 1 variables: // initialize 0, 1 variables:
get_one(true); get_one(true);
get_one(false); get_one(false);
@ -1274,10 +1285,10 @@ public:
theory_var z = internalize_def(term); theory_var z = internalize_def(term);
lpvar zi = register_theory_var_in_lar_solver(z); lpvar zi = register_theory_var_in_lar_solver(z);
lpvar vi = register_theory_var_in_lar_solver(v); lpvar vi = register_theory_var_in_lar_solver(v);
add_def_constraint(lp().add_var_bound(zi, lp::GE, rational::zero())); add_def_constraint_and_equality(zi, lp::GE, rational::zero());
add_def_constraint(lp().add_var_bound(zi, lp::LE, rational::zero())); add_def_constraint_and_equality(zi, lp::LE, rational::zero());
add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); add_def_constraint_and_equality(vi, lp::GE, rational::zero());
add_def_constraint(lp().add_var_bound(vi, lp::LT, abs(r))); add_def_constraint_and_equality(vi, lp::LT, abs(r));
SASSERT(!is_infeasible()); SASSERT(!is_infeasible());
TRACE("arith", tout << term << "\n" << lp().constraints();); TRACE("arith", tout << term << "\n" << lp().constraints(););
} }