mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
move some functionality from int_solver to int_solver::imp
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
889292472e
commit
a1a01b9da6
|
|
@ -406,7 +406,7 @@ public:
|
|||
unsigned n = static_cast<unsigned>(sorted_vars.size());
|
||||
|
||||
while (num_cuts-- && n > 0) {
|
||||
unsigned k = lia.random() % n;
|
||||
unsigned k = lia.settings().random_next() % n;
|
||||
|
||||
double k_ratio = k / (double) n;
|
||||
k_ratio *= k_ratio*k_ratio; // square k_ratio to make it smaller
|
||||
|
|
@ -496,7 +496,7 @@ public:
|
|||
auto _check_feasible = [&](void) {
|
||||
lra.find_feasible_solution();
|
||||
if (!lra.is_feasible() && !lia.settings().get_cancel_flag()) {
|
||||
lra.get_infeasibility_explanation(*lia.m_ex);
|
||||
lra.get_infeasibility_explanation(*(lia.explanation()));
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
|
@ -507,7 +507,7 @@ public:
|
|||
SASSERT(is_gomory_cut_target(j));
|
||||
unsigned row_index = lia.row_of_basic_column(j);
|
||||
const row_strip<mpq>& row = lra.get_row(row_index);
|
||||
create_cut cc(lia.m_t, lia.m_k, lia.m_ex, j, row, lia);
|
||||
create_cut cc(lia.get_term(), lia.offset(), lia.explanation(), j, row, lia);
|
||||
auto r = cc.cut();
|
||||
if (r != lia_move::cut) {
|
||||
if (r == lia_move::conflict)
|
||||
|
|
@ -520,7 +520,7 @@ public:
|
|||
else if (cc.m_polarity == row_polarity::MIN)
|
||||
lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE, ceil(lra.get_column_value(j).x), add_deps(cc.m_dep, row, j));
|
||||
|
||||
if (!is_small_cut(lia.m_t)) {
|
||||
if (!is_small_cut(lia.get_term())) {
|
||||
big_cuts.push_back({cc.m_t, cc.m_k, cc.m_dep});
|
||||
continue;
|
||||
}
|
||||
|
|
@ -548,7 +548,7 @@ public:
|
|||
if (lra.get_status() == lp_status::CANCELLED)
|
||||
return lia_move::cancelled;
|
||||
|
||||
if (!lia.has_inf_int())
|
||||
if (!lra.has_inf_int())
|
||||
return lia_move::sat;
|
||||
|
||||
if (has_small_cut || big_cuts.size())
|
||||
|
|
|
|||
|
|
@ -260,7 +260,7 @@ branch y_i >= ceil(y0_i) is impossible.
|
|||
#ifdef Z3DEBUG
|
||||
vector<mpq> x0 = transform_to_local_columns(lra.r_x());
|
||||
#endif
|
||||
lia_move r = create_cut(lia.m_t, lia.m_k, lia.m_ex, lia.m_upper
|
||||
lia_move r = create_cut(lia.get_term(), lia.offset(), lia.explanation(), lia.is_upper()
|
||||
#ifdef Z3DEBUG
|
||||
, x0
|
||||
#endif
|
||||
|
|
@ -268,18 +268,18 @@ branch y_i >= ceil(y0_i) is impossible.
|
|||
|
||||
if (r == lia_move::cut) {
|
||||
TRACE("hnf_cut",
|
||||
lra.print_term(lia.m_t, tout << "cut:");
|
||||
tout << " <= " << lia.m_k << std::endl;
|
||||
lra.print_term(lia.get_term(), tout << "cut:");
|
||||
tout << " <= " << lia.offset() << std::endl;
|
||||
for (auto* dep : constraints_for_explanation())
|
||||
for (auto ci : lra.flatten(dep))
|
||||
lra.constraints().display(tout, ci);
|
||||
);
|
||||
lp_assert(lia.current_solution_is_inf_on_cut());
|
||||
lia.settings().stats().m_hnf_cuts++;
|
||||
lia.m_ex->clear();
|
||||
lia.explanation()->clear();
|
||||
for (u_dependency* dep : constraints_for_explanation())
|
||||
for (auto ci : lia.lra.flatten(dep))
|
||||
lia.m_ex->push_back(ci);
|
||||
lia.explanation()->push_back(ci);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -31,22 +31,22 @@ lia_move int_branch::operator()() {
|
|||
|
||||
lia_move int_branch::create_branch_on_column(int j) {
|
||||
TRACE("check_main_int", tout << "branching" << std::endl;);
|
||||
lia.m_t.clear();
|
||||
lia.get_term().clear();
|
||||
|
||||
lp_assert(j != -1);
|
||||
lia.m_t.add_monomial(mpq(1), j);
|
||||
lia.get_term().add_monomial(mpq(1), j);
|
||||
if (lia.is_free(j)) {
|
||||
lia.m_upper = lia.random() % 2;
|
||||
lia.m_k = mpq(0);
|
||||
lia.is_upper() = lia.settings().random_next() % 2;
|
||||
lia.offset() = mpq(0);
|
||||
}
|
||||
else {
|
||||
lia.m_upper = lia.random() % 2;
|
||||
lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));
|
||||
lia.is_upper() = lia.settings().random_next() % 2;
|
||||
lia.offset() = lia.is_upper()? floor(lia.get_value(j)) : ceil(lia.get_value(j));
|
||||
}
|
||||
|
||||
TRACE("int_solver",
|
||||
lia.display_column(tout << "branching v" << j << " = " << lia.get_value(j) << "\n", j);
|
||||
tout << "k = " << lia.m_k << std::endl;);
|
||||
tout << "k = " << lia.offset() << std::endl;);
|
||||
return lia_move::branch;
|
||||
}
|
||||
|
||||
|
|
@ -86,7 +86,7 @@ int int_branch::find_inf_int_base_column() {
|
|||
result = j;
|
||||
prev_usage = usage;
|
||||
n = 1;
|
||||
} else if (usage == prev_usage && (lia.random() % (++n) == 0)) {
|
||||
} else if (usage == prev_usage && (lia.settings().random_next() % (++n) == 0)) {
|
||||
result = j;
|
||||
}
|
||||
}
|
||||
|
|
@ -103,7 +103,7 @@ int int_branch::find_inf_int_base_column() {
|
|||
n = 1;
|
||||
result = j;
|
||||
range = new_range;
|
||||
} else if (new_range == range && (lia.random() % (++n) == 0)) {
|
||||
} else if (new_range == range && (lia.settings().random_next() % (++n) == 0)) {
|
||||
result = j;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -252,7 +252,7 @@ namespace lp {
|
|||
void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
|
||||
auto* deps = lra.get_bound_constraint_witnesses_for_column(j);
|
||||
for (auto d : lra.flatten(deps))
|
||||
lia.m_ex->push_back(d);
|
||||
lia.explanation()->push_back(d);
|
||||
}
|
||||
|
||||
bool int_gcd_test::accumulate_parity(const row_strip<mpq> & row, unsigned least_idx) {
|
||||
|
|
|
|||
|
|
@ -13,13 +13,70 @@
|
|||
namespace lp {
|
||||
bool get_patching_deltas(const rational& x, const rational& alpha,
|
||||
rational& delta_plus, rational& delta_minus);
|
||||
class imp {
|
||||
// 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) :
|
||||
lra(ls),
|
||||
m_track_touched_rows(lra.touched_rows_are_tracked()) {
|
||||
lra.track_touched_rows(false);
|
||||
}
|
||||
~check_return_helper() {
|
||||
lra.track_touched_rows(m_track_touched_rows);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
struct imp {
|
||||
int_solver& lia;
|
||||
lar_solver& lra;
|
||||
lar_core_solver& lrac;
|
||||
public:
|
||||
imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac) {}
|
||||
bool should_apply() const { return true; }
|
||||
unsigned m_number_of_calls = 0;
|
||||
lar_term m_t; // the term to return in the cut
|
||||
bool m_upper; // cut is an upper bound
|
||||
explanation *m_ex; // the conflict explanation
|
||||
mpq m_k; // the right side of the cut
|
||||
hnf_cutter m_hnf_cutter;
|
||||
unsigned m_hnf_cut_period;
|
||||
unsigned_vector m_cut_vars; // variables that should not be selected for cuts
|
||||
int_gcd_test m_gcd;
|
||||
|
||||
bool column_is_int_inf(unsigned j) const {
|
||||
return lra.column_is_int(j) && (!lia.value_is_int(j));
|
||||
}
|
||||
|
||||
imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_gcd(lia) {}
|
||||
|
||||
bool has_lower(unsigned j) const {
|
||||
switch (lrac.m_column_types()[j]) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::lower_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool has_upper(unsigned j) const {
|
||||
switch (lrac.m_column_types()[j]) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
const impq& upper_bound(unsigned j) const {
|
||||
return lra.column_upper_bound(j);
|
||||
}
|
||||
|
||||
const impq& lower_bound(unsigned j) const {
|
||||
return lra.column_lower_bound(j);
|
||||
}
|
||||
|
||||
void patch_basic_column(unsigned v) {
|
||||
SASSERT(!lia.is_fixed(v));
|
||||
for (auto const& c : lra.basic2row(v))
|
||||
|
|
@ -29,7 +86,7 @@ namespace lp {
|
|||
bool try_patch_column(unsigned v, unsigned j, mpq const& delta) {
|
||||
const auto & A = lra.A_r();
|
||||
if (delta < 0) {
|
||||
if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
|
||||
if (has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
|
|
@ -41,9 +98,9 @@ namespace lp {
|
|||
unsigned bj = lrac.m_r_basis[row_index];
|
||||
auto old_val = lia.get_value(bj);
|
||||
auto new_val = old_val - impq(c.coeff()*delta);
|
||||
if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj))
|
||||
if (has_lower(bj) && new_val < lra.get_lower_bound(bj))
|
||||
return false;
|
||||
if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj))
|
||||
if (has_upper(bj) && new_val > lra.get_upper_bound(bj))
|
||||
return false;
|
||||
if (old_val.is_int() && !new_val.is_int()){
|
||||
return false; // do not waste resources on this case
|
||||
|
|
@ -57,12 +114,16 @@ namespace lp {
|
|||
return true;
|
||||
}
|
||||
|
||||
unsigned count_non_int() {
|
||||
unsigned non_int = 0;
|
||||
for (auto j : lra.r_basis())
|
||||
if (lra.column_is_int(j) && !lra.column_value_is_int(j))
|
||||
++non_int;
|
||||
return non_int;
|
||||
|
||||
unsigned random() {
|
||||
return settings().random_next();
|
||||
}
|
||||
|
||||
bool all_columns_are_integral() const {
|
||||
for (lpvar j = 0; j < lra.number_of_vars(); j++)
|
||||
if (!lra.column_is_int(j))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c) {
|
||||
|
|
@ -80,7 +141,7 @@ namespace lp {
|
|||
if (!get_patching_deltas(r, a, delta_plus, delta_minus))
|
||||
return false;
|
||||
|
||||
if (lia.random() % 2)
|
||||
if (random() % 2)
|
||||
return try_patch_column(v, c.var(), delta_plus) ||
|
||||
try_patch_column(v, c.var(), delta_minus);
|
||||
else
|
||||
|
|
@ -95,19 +156,213 @@ namespace lp {
|
|||
for (unsigned j : lra.r_basis())
|
||||
if (!lra.get_value(j).is_int() && lra.column_is_int(j) && !lia.is_fixed(j))
|
||||
patch_basic_column(j);
|
||||
if (!lia.has_inf_int()) {
|
||||
if (!lra.has_inf_int()) {
|
||||
lia.settings().stats().m_patches_success++;
|
||||
return lia_move::sat;
|
||||
}
|
||||
return lia_move::undef;
|
||||
}
|
||||
|
||||
bool should_solve_dioph_eq() { return lia.settings().dioph_eq(); }
|
||||
void init_dioph_eq() {
|
||||
}
|
||||
|
||||
lia_move solve_dioph_eq() {
|
||||
init_dioph_eq();
|
||||
return lia_move::undef;
|
||||
}
|
||||
|
||||
lp_settings& settings() { return lra.settings(); }
|
||||
|
||||
bool should_find_cube() {
|
||||
return m_number_of_calls % settings().m_int_find_cube_period == 0;
|
||||
}
|
||||
|
||||
bool should_gomory_cut() {
|
||||
return m_number_of_calls % settings().m_int_gomory_cut_period == 0;
|
||||
}
|
||||
|
||||
bool should_solve_dioph_eq() {
|
||||
return lia.settings().dioph_eq() && m_number_of_calls % settings().m_dioph_eq_period == 0;
|
||||
}
|
||||
|
||||
bool should_hnf_cut() {
|
||||
return settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0;
|
||||
}
|
||||
|
||||
lia_move hnf_cut() {
|
||||
lia_move r = m_hnf_cutter.make_hnf_cut();
|
||||
if (r == lia_move::undef)
|
||||
m_hnf_cut_period *= 2;
|
||||
else
|
||||
m_hnf_cut_period = settings().hnf_cut_period();
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
lia_move check(lp::explanation * e) {
|
||||
SASSERT(lra.ax_is_correct());
|
||||
if (!lra.has_inf_int())
|
||||
return lia_move::sat;
|
||||
|
||||
m_t.clear();
|
||||
m_k.reset();
|
||||
m_ex = e;
|
||||
m_ex->clear();
|
||||
m_upper = false;
|
||||
m_cut_vars.reset();
|
||||
|
||||
lia_move r = lia_move::undef;
|
||||
|
||||
if (m_gcd.should_apply())
|
||||
r = m_gcd();
|
||||
|
||||
check_return_helper pc(lra);
|
||||
|
||||
if (settings().get_cancel_flag())
|
||||
return lia_move::undef;
|
||||
|
||||
++m_number_of_calls;
|
||||
if (r == lia_move::undef) r = patch_basic_columns();
|
||||
if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)();
|
||||
if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
|
||||
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
|
||||
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
|
||||
|
||||
if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2);
|
||||
|
||||
if (r == lia_move::undef) r = int_branch(lia)();
|
||||
if (settings().get_cancel_flag()) r = lia_move::undef;
|
||||
return r;
|
||||
}
|
||||
|
||||
bool cut_indices_are_columns() const {
|
||||
for (lar_term::ival p : m_t) {
|
||||
if (p.j() >= lra.A_r().column_count())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool 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);
|
||||
mpq sign = m_upper ? one_of_type<mpq>() : -one_of_type<mpq>();
|
||||
CTRACE("current_solution_is_inf_on_cut", v * sign <= impq(m_k) * sign,
|
||||
tout << "m_upper = " << m_upper << std::endl;
|
||||
tout << "v = " << v << ", k = " << m_k << std::endl;
|
||||
tout << "term:";lra.print_term(m_t, tout) << "\n";
|
||||
);
|
||||
return v * sign > impq(m_k) * sign;
|
||||
}
|
||||
|
||||
int select_int_infeasible_var() {
|
||||
int r_small_box = -1;
|
||||
int r_small_value = -1;
|
||||
int r_any_value = -1;
|
||||
unsigned n_small_box = 1;
|
||||
unsigned n_small_value = 1;
|
||||
unsigned n_any_value = 1;
|
||||
mpq range;
|
||||
mpq new_range;
|
||||
mpq small_value(1024);
|
||||
unsigned prev_usage = 0;
|
||||
|
||||
auto add_column = [&](bool improved, int& result, unsigned& n, unsigned j) {
|
||||
if (result == -1)
|
||||
result = j;
|
||||
else if (improved && ((random() % (++n)) == 0))
|
||||
result = j;
|
||||
};
|
||||
|
||||
for (unsigned j : lra.r_basis()) {
|
||||
if (!column_is_int_inf(j))
|
||||
continue;
|
||||
if (m_cut_vars.contains(j))
|
||||
continue;
|
||||
|
||||
SASSERT(!lia.is_fixed(j));
|
||||
|
||||
unsigned usage = lra.usage_in_terms(j);
|
||||
if (lia.is_boxed(j) && (new_range = lra.bound_span_x(j) - rational(2*usage)) <= small_value) {
|
||||
|
||||
bool improved = new_range <= range || r_small_box == -1;
|
||||
if (improved)
|
||||
range = new_range;
|
||||
add_column(improved, r_small_box, n_small_box, j);
|
||||
continue;
|
||||
}
|
||||
impq const& value = lia.get_value(j);
|
||||
if (abs(value.x) < small_value ||
|
||||
(lra.column_has_upper_bound(j) && small_value > upper_bound(j).x - value.x) ||
|
||||
(has_lower(j) && small_value > value.x - lower_bound(j).x)) {
|
||||
TRACE("int_solver", tout << "small j" << j << "\n");
|
||||
add_column(true, r_small_value, n_small_value, j);
|
||||
continue;
|
||||
}
|
||||
TRACE("int_solver", tout << "any j" << j << "\n");
|
||||
add_column(usage >= prev_usage, r_any_value, n_any_value, j);
|
||||
if (usage > prev_usage)
|
||||
prev_usage = usage;
|
||||
}
|
||||
|
||||
if (r_small_box != -1 && (random() % 3 != 0))
|
||||
return r_small_box;
|
||||
if (r_small_value != -1 && (random() % 3) != 0)
|
||||
return r_small_value;
|
||||
if (r_any_value != -1)
|
||||
return r_any_value;
|
||||
if (r_small_box != -1)
|
||||
return r_small_box;
|
||||
return r_small_value;
|
||||
}
|
||||
|
||||
std::ostream & 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) {
|
||||
if (lia.is_fixed(c.var())) {
|
||||
if (!lia.get_value(c.var()).is_zero()) {
|
||||
impq val = lia.get_value(c.var()) * c.coeff();
|
||||
if (!first && val.is_pos())
|
||||
out << "+";
|
||||
if (val.y.is_zero())
|
||||
out << val.x << " ";
|
||||
else
|
||||
out << val << " ";
|
||||
}
|
||||
first = false;
|
||||
continue;
|
||||
}
|
||||
if (c.coeff().is_one()) {
|
||||
if (!first)
|
||||
out << "+";
|
||||
}
|
||||
else if (c.coeff().is_minus_one())
|
||||
out << "-";
|
||||
else {
|
||||
if (c.coeff().is_pos() && !first)
|
||||
out << "+";
|
||||
if (c.coeff().is_big())
|
||||
out << " b*";
|
||||
else
|
||||
out << c.coeff();
|
||||
}
|
||||
out << rslv.column_name(c.var()) << " ";
|
||||
first = false;
|
||||
}
|
||||
out << "\n";
|
||||
for (const auto &c : row) {
|
||||
if (lia.is_fixed(c.var()))
|
||||
continue;
|
||||
rslv.print_column_info(c.var(), out);
|
||||
if (lia.is_base(c.var()))
|
||||
out << "j" << c.var() << " base\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
|
@ -157,67 +412,21 @@ namespace lp {
|
|||
|
||||
int_solver::int_solver(lar_solver& lar_slv) :
|
||||
lra(lar_slv),
|
||||
lrac(lra.m_mpq_lar_core_solver),
|
||||
m_gcd(*this),
|
||||
m_number_of_calls(0),
|
||||
m_hnf_cutter(*this),
|
||||
m_hnf_cut_period(settings().hnf_cut_period()) {
|
||||
lrac(lra.m_mpq_lar_core_solver) {
|
||||
m_imp = alloc(imp, *this);
|
||||
lra.set_int_solver(this);
|
||||
}
|
||||
|
||||
int_solver::~int_solver() { dealloc(m_imp); }
|
||||
int_solver::~int_solver() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
// 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) :
|
||||
lra(ls),
|
||||
m_track_touched_rows(lra.touched_rows_are_tracked()) {
|
||||
lra.track_touched_rows(false);
|
||||
}
|
||||
~check_return_helper() {
|
||||
lra.track_touched_rows(m_track_touched_rows);
|
||||
}
|
||||
};
|
||||
|
||||
lia_move int_solver::check(lp::explanation * e) {
|
||||
SASSERT(lra.ax_is_correct());
|
||||
if (!has_inf_int())
|
||||
return lia_move::sat;
|
||||
|
||||
m_t.clear();
|
||||
m_k.reset();
|
||||
m_ex = e;
|
||||
m_ex->clear();
|
||||
m_upper = false;
|
||||
m_cut_vars.reset();
|
||||
|
||||
lia_move r = lia_move::undef;
|
||||
|
||||
if (m_gcd.should_apply())
|
||||
r = m_gcd();
|
||||
|
||||
check_return_helper pc(lra);
|
||||
|
||||
if (settings().get_cancel_flag())
|
||||
return lia_move::undef;
|
||||
|
||||
++m_number_of_calls;
|
||||
if (r == lia_move::undef && m_imp->should_apply()) r = m_imp->patch_basic_columns();
|
||||
if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
|
||||
if (r == lia_move::undef && m_imp->should_solve_dioph_eq()) r = m_imp->solve_dioph_eq();
|
||||
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
|
||||
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
|
||||
|
||||
if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this).get_gomory_cuts(2);
|
||||
|
||||
if (r == lia_move::undef) r = int_branch(*this)();
|
||||
if (settings().get_cancel_flag()) r = lia_move::undef;
|
||||
return r;
|
||||
return m_imp->check(e);
|
||||
}
|
||||
|
||||
|
||||
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++) {
|
||||
|
|
@ -239,30 +448,6 @@ namespace lp {
|
|||
return out;
|
||||
}
|
||||
|
||||
bool int_solver::cut_indices_are_columns() const {
|
||||
for (lar_term::ival p : m_t) {
|
||||
if (p.j() >= lra.A_r().column_count())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
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);
|
||||
mpq sign = m_upper ? one_of_type<mpq>() : -one_of_type<mpq>();
|
||||
CTRACE("current_solution_is_inf_on_cut", v * sign <= impq(m_k) * sign,
|
||||
tout << "m_upper = " << m_upper << std::endl;
|
||||
tout << "v = " << v << ", k = " << m_k << std::endl;
|
||||
tout << "term:";lra.print_term(m_t, tout) << "\n";
|
||||
);
|
||||
return v * sign > impq(m_k) * sign;
|
||||
}
|
||||
|
||||
bool int_solver::has_inf_int() const {
|
||||
return lra.has_inf_int();
|
||||
}
|
||||
|
||||
u_dependency* int_solver::column_upper_bound_constraint(unsigned j) const {
|
||||
return lra.get_column_upper_bound_witness(j);
|
||||
|
|
@ -296,18 +481,6 @@ namespace lp {
|
|||
return lra.column_value_is_int(j);
|
||||
}
|
||||
|
||||
unsigned int_solver::random() {
|
||||
return settings().random_next();
|
||||
}
|
||||
|
||||
const impq& int_solver::upper_bound(unsigned j) const {
|
||||
return lra.column_upper_bound(j);
|
||||
}
|
||||
|
||||
const impq& int_solver::lower_bound(unsigned j) const {
|
||||
return lra.column_lower_bound(j);
|
||||
}
|
||||
|
||||
bool int_solver::is_term(unsigned j) const {
|
||||
return lra.column_has_term(j);
|
||||
}
|
||||
|
|
@ -316,49 +489,6 @@ namespace lp {
|
|||
return lra.column_count();
|
||||
}
|
||||
|
||||
bool int_solver::should_find_cube() {
|
||||
return m_number_of_calls % settings().m_int_find_cube_period == 0;
|
||||
}
|
||||
|
||||
bool int_solver::should_gomory_cut() {
|
||||
return m_number_of_calls % settings().m_int_gomory_cut_period == 0;
|
||||
}
|
||||
|
||||
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 r = m_hnf_cutter.make_hnf_cut();
|
||||
if (r == lia_move::undef)
|
||||
m_hnf_cut_period *= 2;
|
||||
else
|
||||
m_hnf_cut_period = settings().hnf_cut_period();
|
||||
return r;
|
||||
}
|
||||
|
||||
bool int_solver::has_lower(unsigned j) const {
|
||||
switch (lrac.m_column_types()[j]) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::lower_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool int_solver::has_upper(unsigned j) const {
|
||||
switch (lrac.m_column_types()[j]) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
static void set_lower(impq & l, bool & inf_l, impq const & v ) {
|
||||
if (inf_l || v > l) {
|
||||
l = v;
|
||||
|
|
@ -463,10 +593,6 @@ namespace lp {
|
|||
return lrac.m_r_solver.print_column_info(j, out);
|
||||
}
|
||||
|
||||
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 {
|
||||
return lrac.m_r_heading[j] >= 0;
|
||||
}
|
||||
|
|
@ -524,50 +650,6 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
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) {
|
||||
if (is_fixed(c.var())) {
|
||||
if (!get_value(c.var()).is_zero()) {
|
||||
impq val = get_value(c.var()) * c.coeff();
|
||||
if (!first && val.is_pos())
|
||||
out << "+";
|
||||
if (val.y.is_zero())
|
||||
out << val.x << " ";
|
||||
else
|
||||
out << val << " ";
|
||||
}
|
||||
first = false;
|
||||
continue;
|
||||
}
|
||||
if (c.coeff().is_one()) {
|
||||
if (!first)
|
||||
out << "+";
|
||||
}
|
||||
else if (c.coeff().is_minus_one())
|
||||
out << "-";
|
||||
else {
|
||||
if (c.coeff().is_pos() && !first)
|
||||
out << "+";
|
||||
if (c.coeff().is_big())
|
||||
out << " b*";
|
||||
else
|
||||
out << c.coeff();
|
||||
}
|
||||
out << rslv.column_name(c.var()) << " ";
|
||||
first = false;
|
||||
}
|
||||
out << "\n";
|
||||
for (const auto &c : row) {
|
||||
if (is_fixed(c.var()))
|
||||
continue;
|
||||
rslv.print_column_info(c.var(), out);
|
||||
if (is_base(c.var()))
|
||||
out << "j" << c.var() << " base\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
|
||||
auto & rslv = lrac.m_r_solver;
|
||||
|
|
@ -575,6 +657,10 @@ namespace lp {
|
|||
return display_row(out, row);
|
||||
}
|
||||
|
||||
std::ostream & int_solver::display_row(std::ostream & out, vector<row_cell<rational>> const & row) const {
|
||||
return m_imp->display_row(out, row);
|
||||
}
|
||||
|
||||
bool int_solver::shift_var(unsigned j, unsigned range) {
|
||||
if (is_fixed(j) || is_base(j))
|
||||
return false;
|
||||
|
|
@ -591,7 +677,7 @@ namespace lp {
|
|||
// x, the value of j column, might be shifted on a multiple of m
|
||||
|
||||
if (inf_l && inf_u) {
|
||||
impq new_val = m * impq(random() % (range + 1)) + x;
|
||||
impq new_val = m * impq(lra.settings().random_next() % (range + 1)) + x;
|
||||
lra.set_value_for_nbasic_column(j, new_val);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -607,14 +693,14 @@ namespace lp {
|
|||
|
||||
if (inf_u) {
|
||||
SASSERT(!inf_l);
|
||||
impq new_val = x + m * impq(random() % (range + 1));
|
||||
impq new_val = x + m * impq(lra.settings().random_next() % (range + 1));
|
||||
lra.set_value_for_nbasic_column(j, new_val);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (inf_l) {
|
||||
SASSERT(!inf_u);
|
||||
impq new_val = x - m * impq(random() % (range + 1));
|
||||
impq new_val = x - m * impq(lra.settings().random_next() % (range + 1));
|
||||
lra.set_value_for_nbasic_column(j, new_val);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -633,7 +719,7 @@ namespace lp {
|
|||
if (r < mpq(range))
|
||||
range = static_cast<unsigned>(r.get_uint64());
|
||||
|
||||
mpq s = b + mpq(random() % (range + 1));
|
||||
mpq s = b + mpq(lra.settings().random_next() % (range + 1));
|
||||
impq new_val = x + m * impq(s);
|
||||
TRACE("int_solver", tout << "new_val = " << new_val << "\n";);
|
||||
SASSERT(l <= new_val && new_val <= u);
|
||||
|
|
@ -642,67 +728,6 @@ namespace lp {
|
|||
}
|
||||
|
||||
|
||||
int int_solver::select_int_infeasible_var() {
|
||||
int r_small_box = -1;
|
||||
int r_small_value = -1;
|
||||
int r_any_value = -1;
|
||||
unsigned n_small_box = 1;
|
||||
unsigned n_small_value = 1;
|
||||
unsigned n_any_value = 1;
|
||||
mpq range;
|
||||
mpq new_range;
|
||||
mpq small_value(1024);
|
||||
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
|
||||
unsigned prev_usage = 0;
|
||||
|
||||
auto add_column = [&](bool improved, int& result, unsigned& n, unsigned j) {
|
||||
if (result == -1)
|
||||
result = j;
|
||||
else if (improved && ((random() % (++n)) == 0))
|
||||
result = j;
|
||||
};
|
||||
|
||||
for (unsigned j : lra.r_basis()) {
|
||||
if (!column_is_int_inf(j))
|
||||
continue;
|
||||
if (m_cut_vars.contains(j))
|
||||
continue;
|
||||
|
||||
SASSERT(!is_fixed(j));
|
||||
|
||||
unsigned usage = lra.usage_in_terms(j);
|
||||
if (is_boxed(j) && (new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
|
||||
|
||||
bool improved = new_range <= range || r_small_box == -1;
|
||||
if (improved)
|
||||
range = new_range;
|
||||
add_column(improved, r_small_box, n_small_box, j);
|
||||
continue;
|
||||
}
|
||||
impq const& value = get_value(j);
|
||||
if (abs(value.x) < small_value ||
|
||||
(has_upper(j) && small_value > upper_bound(j).x - value.x) ||
|
||||
(has_lower(j) && small_value > value.x - lower_bound(j).x)) {
|
||||
TRACE("int_solver", tout << "small j" << j << "\n");
|
||||
add_column(true, r_small_value, n_small_value, j);
|
||||
continue;
|
||||
}
|
||||
TRACE("int_solver", tout << "any j" << j << "\n");
|
||||
add_column(usage >= prev_usage, r_any_value, n_any_value, j);
|
||||
if (usage > prev_usage)
|
||||
prev_usage = usage;
|
||||
}
|
||||
|
||||
if (r_small_box != -1 && (random() % 3 != 0))
|
||||
return r_small_box;
|
||||
if (r_small_value != -1 && (random() % 3) != 0)
|
||||
return r_small_value;
|
||||
if (r_any_value != -1)
|
||||
return r_any_value;
|
||||
if (r_small_box != -1)
|
||||
return r_small_box;
|
||||
return r_small_value;
|
||||
}
|
||||
|
||||
void int_solver::simplify(std::function<bool(unsigned)>& is_root) {
|
||||
return;
|
||||
|
|
@ -841,7 +866,29 @@ namespace lp {
|
|||
|
||||
#endif
|
||||
}
|
||||
lar_term const& int_solver::get_term() const { return m_imp->m_t; }
|
||||
lar_term & int_solver::get_term() { return m_imp->m_t; }
|
||||
mpq const& int_solver::offset() const { return m_imp->m_k; }
|
||||
mpq & int_solver::offset() { return m_imp->m_k; }
|
||||
|
||||
bool int_solver::is_upper() const { return m_imp->m_upper; }
|
||||
bool& int_solver::is_upper() { return m_imp->m_upper; }
|
||||
explanation* int_solver::explanation() { return m_imp->m_ex; }
|
||||
bool int_solver::column_is_int_inf(unsigned j) const {
|
||||
return m_imp->column_is_int_inf(j);
|
||||
}
|
||||
|
||||
bool int_solver::has_lower(unsigned j) const {
|
||||
return m_imp->has_lower(j);
|
||||
}
|
||||
|
||||
bool int_solver::has_upper(unsigned j) const {
|
||||
return m_imp->has_upper(j);
|
||||
}
|
||||
|
||||
int int_solver::select_int_infeasible_var() { return m_imp->select_int_infeasible_var(); }
|
||||
bool int_solver::current_solution_is_inf_on_cut() const { return m_imp->current_solution_is_inf_on_cut(); }
|
||||
const impq & int_solver::lower_bound(unsigned j) const { return m_imp->lower_bound(j);}
|
||||
const impq & int_solver::upper_bound(unsigned j) const { return m_imp->upper_bound(j);}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ Revision History:
|
|||
namespace lp {
|
||||
class lar_solver;
|
||||
class lar_core_solver;
|
||||
class imp;
|
||||
struct imp;
|
||||
class int_solver {
|
||||
friend struct create_cut;
|
||||
friend class gomory;
|
||||
|
|
@ -39,31 +39,23 @@ class int_solver {
|
|||
friend class int_branch;
|
||||
friend class int_gcd_test;
|
||||
friend class hnf_cutter;
|
||||
friend class imp;
|
||||
friend struct imp;
|
||||
|
||||
lar_solver& lra;
|
||||
lar_core_solver& lrac;
|
||||
int_gcd_test m_gcd;
|
||||
imp *m_imp;
|
||||
unsigned m_number_of_calls;
|
||||
lar_term m_t; // the term to return in the cut
|
||||
mpq m_k; // the right side of the cut
|
||||
bool m_upper; // cut is an upper bound
|
||||
explanation *m_ex; // the conflict explanation
|
||||
hnf_cutter m_hnf_cutter;
|
||||
unsigned m_hnf_cut_period;
|
||||
unsigned_vector m_cut_vars; // variables that should not be selected for cuts
|
||||
|
||||
imp* m_imp;
|
||||
vector<equality> m_equalities;
|
||||
public:
|
||||
int_solver(lar_solver& lp);
|
||||
~int_solver();
|
||||
// main function to check that the solution provided by lar_solver is valid for integral values,
|
||||
// or provide a way of how it can be adjusted.
|
||||
// the function that doing the main job
|
||||
lia_move check(explanation *);
|
||||
lar_term const& get_term() const { return m_t; }
|
||||
mpq const& get_offset() const { return m_k; }
|
||||
bool is_upper() const { return m_upper; }
|
||||
lar_term const& get_term() const;
|
||||
lar_term & get_term();
|
||||
mpq const& offset() const;
|
||||
mpq & offset();
|
||||
bool is_upper() const;
|
||||
bool& is_upper();
|
||||
bool is_base(unsigned j) const;
|
||||
bool is_real(unsigned j) const;
|
||||
const impq & lower_bound(unsigned j) const;
|
||||
|
|
@ -84,9 +76,6 @@ private:
|
|||
bool is_feasible() const;
|
||||
bool column_is_int_inf(unsigned j) const;
|
||||
std::ostream& display_inf_rows(std::ostream&) const;
|
||||
bool should_find_cube();
|
||||
bool should_gomory_cut();
|
||||
bool should_hnf_cut();
|
||||
|
||||
lp_settings& settings();
|
||||
const lp_settings& settings() const;
|
||||
|
|
@ -94,7 +83,7 @@ private:
|
|||
bool has_lower(unsigned j) const;
|
||||
bool has_upper(unsigned j) const;
|
||||
unsigned row_of_basic_column(unsigned j) const;
|
||||
bool cut_indices_are_columns() const;
|
||||
|
||||
|
||||
public:
|
||||
bool is_fixed(unsigned j) const;
|
||||
|
|
@ -107,15 +96,10 @@ public:
|
|||
std::ostream& display_row_info(std::ostream & out, unsigned row_index) const;
|
||||
std::ostream & display_row(std::ostream & out, vector<row_cell<rational>> const & row) const;
|
||||
|
||||
private:
|
||||
unsigned random();
|
||||
bool has_inf_int() const;
|
||||
public:
|
||||
bool is_term(unsigned j) const;
|
||||
unsigned column_count() const;
|
||||
lia_move hnf_cut();
|
||||
|
||||
int select_int_infeasible_var();
|
||||
|
||||
explanation * explanation();
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -217,6 +217,7 @@ public:
|
|||
unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000;
|
||||
unsigned m_int_gomory_cut_period = 4;
|
||||
unsigned m_int_find_cube_period = 4;
|
||||
unsigned m_dioph_eq_period = 4;
|
||||
private:
|
||||
unsigned m_hnf_cut_period = 4;
|
||||
bool m_int_run_gcd_test = true;
|
||||
|
|
|
|||
|
|
@ -1176,7 +1176,7 @@ namespace arith {
|
|||
TRACE("arith", tout << "branch\n";);
|
||||
app_ref b(m);
|
||||
bool u = m_lia->is_upper();
|
||||
auto const& k = m_lia->get_offset();
|
||||
auto const& k = m_lia->offset();
|
||||
rational offset;
|
||||
expr_ref t(m);
|
||||
b = mk_bound(m_lia->get_term(), k, !u, offset, t);
|
||||
|
|
@ -1199,7 +1199,7 @@ namespace arith {
|
|||
set_evidence(ev.ci());
|
||||
// The call mk_bound() can set the m_infeasible_column in lar_solver
|
||||
// so the explanation is safer to take before this call.
|
||||
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
|
||||
app_ref b = mk_bound(m_lia->get_term(), m_lia->offset(), !m_lia->is_upper());
|
||||
IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
|
||||
literal lit = expr2literal(b);
|
||||
assign(lit, m_core, m_eqs, explain(hint_type::cut_h, lit));
|
||||
|
|
|
|||
|
|
@ -1888,7 +1888,7 @@ public:
|
|||
case lp::lia_move::branch: {
|
||||
TRACE("arith", tout << "branch\n";);
|
||||
bool u = m_lia->is_upper();
|
||||
auto const & k = m_lia->get_offset();
|
||||
auto const & k = m_lia->offset();
|
||||
rational offset;
|
||||
expr_ref t(m);
|
||||
expr_ref b = mk_bound(m_lia->get_term(), k, !u, offset, t);
|
||||
|
|
@ -1919,13 +1919,13 @@ public:
|
|||
}
|
||||
// The call mk_bound() can set the m_infeasible_column in lar_solver
|
||||
// so the explanation is safer to take before this call.
|
||||
expr_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
|
||||
expr_ref b = mk_bound(m_lia->get_term(), m_lia->offset(), !m_lia->is_upper());
|
||||
if (m.has_trace_stream()) {
|
||||
th.log_axiom_instantiation(b);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
|
||||
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_explanation, m_lia->is_upper()););
|
||||
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->offset(), m_explanation, m_lia->is_upper()););
|
||||
literal lit(ctx().get_bool_var(b), false);
|
||||
TRACE("arith",
|
||||
ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
|
||||
|
|
|
|||
Loading…
Reference in a new issue