mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

formatting hygiene

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 13:50:49 -07:00
parent a7966dc436
commit a6ab0a7d49
2 changed files with 506 additions and 545 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -61,7 +61,6 @@ namespace lp {
// + a1*(delta/t) is integral. Taking into account that t and a1 are
// coprime we have delta = t*k, where k is an integer.
rational t = a2 / x2;
// std::cout << "t = " << t << std::endl;
// Now we have x1/x2 + (a1/x2)*k is integral, or (x1 + a1*k)/x2 is integral.
// It is equivalent to x1 + a1*k = x2*m, where m is an integer
// We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are
@ -69,10 +68,6 @@ namespace lp {
rational u, v;
gcd(a1, x2, u, v);
lp_assert(gcd(a1, x2, u, v).is_one());
// std::cout << "u = " << u << ", v = " << v << std::endl;
// std::cout << "x= " << (x1 / x2) << std::endl;
// std::cout << "x + (a1 / a2) * (-u * t) * x1 = "
// << x + (a1 / a2) * (-u * t) * x1 << std::endl;
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;
@ -103,14 +98,13 @@ namespace lp {
if (!get_patching_deltas(r, a, delta_plus, delta_minus))
return false;
if (lia.random() % 2) {
if (lia.random() % 2)
return try_patch_column(v, c.var(), delta_plus) ||
try_patch_column(v, c.var(), delta_minus);
} else {
else
return try_patch_column(v, c.var(), delta_minus) ||
try_patch_column(v, c.var(), delta_plus);
}
}
bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
const auto & A = lra.A_r();
@ -151,7 +145,7 @@ namespace lp {
}
int_solver::int_solver(lar_solver& lar_slv) :
int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv),
lrac(lra.m_mpq_lar_core_solver),
m_gcd(*this),
@ -160,10 +154,10 @@ int_solver::int_solver(lar_solver& lar_slv) :
m_hnf_cutter(*this),
m_hnf_cut_period(settings().hnf_cut_period()) {
lra.set_int_solver(this);
}
}
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
lar_solver& lra;
bool m_track_touched_rows;
check_return_helper(lar_solver& ls) :
@ -174,9 +168,9 @@ struct check_return_helper {
~check_return_helper() {
lra.track_touched_rows(m_track_touched_rows);
}
};
};
lia_move int_solver::check(lp::explanation * e) {
lia_move int_solver::check(lp::explanation * e) {
SASSERT(lra.ax_is_correct());
if (!has_inf_int()) return lia_move::sat;
@ -201,9 +195,9 @@ lia_move int_solver::check(lp::explanation * e) {
if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this)();
if (r == lia_move::undef) r = int_branch(*this)();
return r;
}
}
std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (column_is_int(v) && !get_value(v).is_int()) {
@ -222,17 +216,17 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
}
out << "num of int infeasible: " << num << "\n";
return out;
}
}
bool int_solver::cut_indices_are_columns() const {
bool int_solver::cut_indices_are_columns() const {
for (lar_term::ival p : m_t) {
if (p.column().index() >= lra.A_r().column_count())
return false;
}
return true;
}
}
bool int_solver::current_solution_is_inf_on_cut() const {
bool int_solver::current_solution_is_inf_on_cut() const {
SASSERT(cut_indices_are_columns());
const auto & x = lrac.m_r_x;
impq v = m_t.apply(x);
@ -242,89 +236,87 @@ bool int_solver::current_solution_is_inf_on_cut() const {
tout << "v = " << v << ", k = " << m_k << std::endl;
);
return v * sign > impq(m_k) * sign;
}
}
bool int_solver::has_inf_int() const {
bool int_solver::has_inf_int() const {
return lra.has_inf_int();
}
}
constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
return lra.get_column_upper_bound_witness(j);
}
}
constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
return lra.get_column_lower_bound_witness(j);
}
}
unsigned int_solver::row_of_basic_column(unsigned j) const {
unsigned int_solver::row_of_basic_column(unsigned j) const {
return lra.row_of_basic_column(j);
}
}
lp_settings& int_solver::settings() {
lp_settings& int_solver::settings() {
return lra.settings();
}
}
const lp_settings& int_solver::settings() const {
const lp_settings& int_solver::settings() const {
return lra.settings();
}
}
bool int_solver::column_is_int(column_index const& j) const {
bool int_solver::column_is_int(column_index const& j) const {
return lra.column_is_int(j);
}
}
bool int_solver::is_real(unsigned j) const {
bool int_solver::is_real(unsigned j) const {
return !column_is_int(j);
}
}
bool int_solver::value_is_int(unsigned j) const {
bool int_solver::value_is_int(unsigned j) const {
return lra.column_value_is_int(j);
}
}
unsigned int_solver::random() {
unsigned int_solver::random() {
return settings().random_next();
}
}
const impq& int_solver::upper_bound(unsigned j) const {
const impq& int_solver::upper_bound(unsigned j) const {
return lra.column_upper_bound(j);
}
}
const impq& int_solver::lower_bound(unsigned j) const {
const impq& int_solver::lower_bound(unsigned j) const {
return lra.column_lower_bound(j);
}
}
bool int_solver::is_term(unsigned j) const {
bool int_solver::is_term(unsigned j) const {
return lra.column_corresponds_to_term(j);
}
}
unsigned int_solver::column_count() const {
unsigned int_solver::column_count() const {
return lra.column_count();
}
}
bool int_solver::should_find_cube() {
bool int_solver::should_find_cube() {
return m_number_of_calls % settings().m_int_find_cube_period == 0;
}
}
bool int_solver::should_gomory_cut() {
bool int_solver::should_gomory_cut() {
return m_number_of_calls % settings().m_int_gomory_cut_period == 0;
}
}
bool int_solver::should_hnf_cut() {
bool int_solver::should_hnf_cut() {
return settings().enable_hnf() && m_number_of_calls % m_hnf_cut_period == 0;
}
}
lia_move int_solver::hnf_cut() {
lia_move int_solver::hnf_cut() {
lia_move r = m_hnf_cutter.make_hnf_cut();
if (r == lia_move::undef) {
if (r == lia_move::undef)
m_hnf_cut_period *= 2;
}
else {
else
m_hnf_cut_period = settings().hnf_cut_period();
}
return r;
}
}
bool int_solver::has_lower(unsigned j) const {
bool int_solver::has_lower(unsigned j) const {
switch (lrac.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
@ -333,9 +325,9 @@ bool int_solver::has_lower(unsigned j) const {
default:
return false;
}
}
}
bool int_solver::has_upper(unsigned j) const {
bool int_solver::has_upper(unsigned j) const {
switch (lrac.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
@ -344,24 +336,24 @@ bool int_solver::has_upper(unsigned j) const {
default:
return false;
}
}
}
static void set_lower(impq & l, bool & inf_l, impq const & v ) {
static void set_lower(impq & l, bool & inf_l, impq const & v ) {
if (inf_l || v > l) {
l = v;
inf_l = false;
}
}
}
static void set_upper(impq & u, bool & inf_u, impq const & v) {
static void set_upper(impq & u, bool & inf_u, impq const & v) {
if (inf_u || v < u) {
u = v;
inf_u = false;
}
}
}
// this function assumes that all basic columns dependend on j are feasible
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
// this function assumes that all basic columns dependend on j are feasible
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
if (lrac.m_r_heading[j] >= 0 || is_fixed(j)) // basic or fixed var
return false;
@ -400,10 +392,8 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
if (column_is_int(i) && !a.is_int() && xi.is_int())
m = lcm(m, denominator(a));
if (!inf_l && !inf_u) {
if (l == u)
if (!inf_l && !inf_u && l == u)
continue;
}
if (a.is_neg()) {
if (has_lower(i))
@ -434,45 +424,45 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
tout << "return " << (inf_l || inf_u || l <= u);
);
return (inf_l || inf_u || l <= u);
}
}
bool int_solver::is_feasible() const {
bool int_solver::is_feasible() const {
lp_assert(
lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() ==
lrac.m_r_solver.current_x_is_feasible());
return lrac.m_r_solver.current_x_is_feasible();
}
}
const impq & int_solver::get_value(unsigned j) const {
const impq & int_solver::get_value(unsigned j) const {
return lrac.m_r_x[j];
}
}
std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
return lrac.m_r_solver.print_column_info(j, out);
}
}
bool int_solver::column_is_int_inf(unsigned j) const {
bool int_solver::column_is_int_inf(unsigned j) const {
return column_is_int(j) && (!value_is_int(j));
}
}
bool int_solver::is_base(unsigned j) const {
bool int_solver::is_base(unsigned j) const {
return lrac.m_r_heading[j] >= 0;
}
}
bool int_solver::is_boxed(unsigned j) const {
bool int_solver::is_boxed(unsigned j) const {
return lrac.m_column_types[j] == column_type::boxed;
}
}
bool int_solver::is_fixed(unsigned j) const {
bool int_solver::is_fixed(unsigned j) const {
return lrac.m_column_types[j] == column_type::fixed;
}
}
bool int_solver::is_free(unsigned j) const {
bool int_solver::is_free(unsigned j) const {
return lrac.m_column_types[j] == column_type::free_column;
}
}
bool int_solver::at_bound(unsigned j) const {
bool int_solver::at_bound(unsigned j) const {
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
@ -487,9 +477,9 @@ bool int_solver::at_bound(unsigned j) const {
default:
return false;
}
}
}
bool int_solver::at_lower(unsigned j) const {
bool int_solver::at_lower(unsigned j) const {
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
@ -499,9 +489,9 @@ bool int_solver::at_lower(unsigned j) const {
default:
return false;
}
}
}
bool int_solver::at_upper(unsigned j) const {
bool int_solver::at_upper(unsigned j) const {
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
@ -511,9 +501,9 @@ bool int_solver::at_upper(unsigned j) const {
default:
return false;
}
}
}
std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rational> const & row) const {
std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rational> const & row) const {
bool first = true;
auto & rslv = lrac.m_r_solver;
for (const auto &c : row) {
@ -530,8 +520,7 @@ std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rationa
first = false;
continue;
}
if (c.coeff().is_one())
{
if (c.coeff().is_one()) {
if (!first)
out << "+";
}
@ -557,15 +546,15 @@ std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rationa
out << "j" << c.var() << " base\n";
}
return out;
}
}
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lrac.m_r_solver;
auto const& row = rslv.m_A.m_rows[row_index];
return display_row(out, row);
}
}
bool int_solver::shift_var(unsigned j, unsigned range) {
bool int_solver::shift_var(unsigned j, unsigned range) {
if (is_fixed(j) || is_base(j))
return false;
if (settings().get_cancel_flag())
@ -586,13 +575,11 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
return true;
}
if (column_is_int(j)) {
if (!inf_l) {
if (!inf_l)
l = impq(ceil(l));
}
if (!inf_u) {
if (!inf_u)
u = impq(floor(u));
}
}
if (!inf_l && !inf_u && l >= u)
return false;
@ -631,35 +618,10 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
SASSERT(l <= new_val && new_val <= u);
lra.set_value_for_nbasic_column(j, new_val);
return true;
}
}
// not used:
bool int_solver::non_basic_columns_are_at_bounds() const {
for (unsigned j : lrac.m_r_nbasis) {
auto & val = lrac.m_r_x[j];
switch (lrac.m_column_types()[j]) {
case column_type::boxed:
if (val != lrac.m_r_lower_bounds()[j] && val != lrac.m_r_upper_bounds()[j])
return false;
break;
case column_type::lower_bound:
if (val != lrac.m_r_lower_bounds()[j])
return false;
break;
case column_type::upper_bound:
if (val != lrac.m_r_upper_bounds()[j])
return false;
break;
default:
if (column_is_int(j) && !val.is_int()) {
return false;
}
}
}
return true;
}
int int_solver::select_int_infeasible_var() {
int int_solver::select_int_infeasible_var() {
int result = -1;
mpq range;
mpq new_range;
@ -718,7 +680,7 @@ int int_solver::select_int_infeasible_var() {
}
return result;
}
}
}

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

@ -109,7 +109,6 @@ private:
bool has_lower(unsigned j) const;
bool has_upper(unsigned j) const;
unsigned row_of_basic_column(unsigned j) const;
bool non_basic_columns_are_at_bounds() const;
bool cut_indices_are_columns() const;
public:
@ -134,5 +133,5 @@ public:
int select_int_infeasible_var();
};
};
}