mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

prepare for throttling gcd test and patching based on cost/success ratio

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-26 19:02:56 -08:00
parent 4f3fbd3c11
commit 11199619a5
6 changed files with 153 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/math/lp/int_gcd_test.cpp
View file

@ -22,15 +22,33 @@ Revision History:
namespace lp {
int_gcd_test::int_gcd_test(int_solver& lia): lia(lia), lra(lia.lra) {}
int_gcd_test::int_gcd_test(int_solver& lia): lia(lia), lra(lia.lra), m_next_gcd(0), m_delay(0) {}
bool int_gcd_test::should_apply() {
if (!lia.settings().m_int_run_gcd_test)
return false;
#if 1
return true;
#else
if (m_delay == 0) {
return true;
}
--m_delay;
return false;
#endif
}
lia_move int_gcd_test::operator()() {
lia.settings().stats().m_gcd_calls++;
TRACE("int_solver", tout << "gcd-test " << lia.settings().stats().m_gcd_calls << "\n";);
if (gcd_test()) {
m_delay = m_next_gcd++;
return lia_move::undef;
}
else {
m_next_gcd = 0;
m_delay = 0;
lia.settings().stats().m_gcd_conflicts++;
TRACE("gcd_test", tout << "gcd conflict\n";);
return lia_move::conflict;

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

@ -34,6 +34,8 @@ namespace lp {
class int_gcd_test {
class int_solver& lia;
class lar_solver& lra;
unsigned m_next_gcd;
unsigned m_delay;
bool gcd_test();
bool gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
@ -47,5 +49,6 @@ namespace lp {
int_gcd_test(int_solver& lia);
~int_gcd_test() {}
lia_move operator()();
bool should_apply();
};
}

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

@ -10,14 +10,113 @@
#include "math/lp/monic.h"
#include "math/lp/gomory.h"
#include "math/lp/int_branch.h"
#include "math/lp/int_gcd_test.h"
#include "math/lp/int_cube.h"
namespace lp {
int_solver::patcher::patcher(int_solver& lia):
lia(lia),
lra(lia.lra),
lrac(lia.lrac),
m_num_nbasic_patches(0),
m_patch_cost(0),
m_delay(0),
m_next_patch(0)
{}
bool int_solver::patcher::should_apply() {
#if 1
return true;
#else
if (m_delay == 0) {
return true;
}
--m_delay;
return false;
#endif
}
lia_move int_solver::patcher::operator()() {
return patch_nbasic_columns();
}
lia_move int_solver::patcher::patch_nbasic_columns() {
lia.settings().stats().m_patches++;
lp_assert(lia.is_feasible());
m_num_nbasic_patches = 0;
m_patch_cost = 0;
for (unsigned j : lia.lrac.m_r_nbasis) {
patch_nbasic_column(j);
}
lp_assert(lia.is_feasible());
if (!lia.has_inf_int()) {
lia.settings().stats().m_patches_success++;
m_delay = 0;
m_next_patch = 0;
return lia_move::sat;
}
if (m_patch_cost > 0 && m_num_nbasic_patches * 10 < m_patch_cost) {
m_delay = std::min(20u, m_next_patch++);
}
else {
m_delay = 0;
m_next_patch = 0;
}
return lia_move::undef;
}
void int_solver::patcher::patch_nbasic_column(unsigned j) {
impq & val = lrac.m_r_x[j];
bool inf_l, inf_u;
impq l, u;
mpq m;
bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
m_patch_cost += lra.A_r().number_of_non_zeroes_in_column(j);
if (!has_free) {
return;
}
bool m_is_one = m.is_one();
bool val_is_int = lia.value_is_int(j);
// check whether value of j is already a multiple of m.
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
return;
}
TRACE("patch_int",
tout << "TARGET j" << j << " -> [";
if (inf_l) tout << "-oo"; else tout << l;
tout << ", ";
if (inf_u) tout << "oo"; else tout << u;
tout << "]";
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {
TRACE("patch_int", tout << "patching with l: " << l << '\n';);
lra.set_value_for_nbasic_column(j, l);
}
else {
--m_num_nbasic_patches;
TRACE("patch_int", tout << "not patching " << l << "\n";);
}
}
else if (!inf_u) {
u = impq(m_is_one ? floor(u) : m * floor(u / m));
lra.set_value_for_nbasic_column(j, u);
TRACE("patch_int", tout << "patching with u: " << u << '\n';);
}
else {
lra.set_value_for_nbasic_column(j, impq(0));
TRACE("patch_int", tout << "patching with 0\n";);
}
++m_num_nbasic_patches;
}
int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv),
lrac(lra.m_mpq_lar_core_solver),
m_gcd(*this),
m_patcher(*this),
m_number_of_calls(0),
m_hnf_cutter(*this),
m_hnf_cut_period(settings().hnf_cut_period()) {
@ -56,18 +155,16 @@ lia_move int_solver::check(lp::explanation * e) {
gomory gc(*this);
int_cube cube(*this);
int_branch branch(*this);
int_gcd_test gcd(*this);
if (should_run_gcd_test()) r = gcd();
if (m_gcd.should_apply()) r = m_gcd();
check_return_helper pc(lra);
if (settings().m_int_pivot_fixed_vars_from_basis)
lra.pivot_fixed_vars_from_basis();
if (r == lia_move::undef) r = patch_nbasic_columns();
++m_number_of_calls;
if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
if (r == lia_move::undef && should_find_cube()) r = cube();
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
if (r == lia_move::undef && should_gomory_cut()) r = gc();
@ -167,9 +264,6 @@ bool int_solver::should_find_cube() {
return m_number_of_calls % settings().m_int_find_cube_period == 0;
}
bool int_solver::should_run_gcd_test() {
return settings().m_int_run_gcd_test;
}
bool int_solver::should_gomory_cut() {
return m_number_of_calls % settings().m_int_gomory_cut_period == 0;
@ -199,62 +293,8 @@ void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const
lra.change_basic_columns_dependend_on_a_given_nb_column(j, delta);
}
void int_solver::patch_nbasic_column(unsigned j) {
impq & val = lrac.m_r_x[j];
bool inf_l, inf_u;
impq l, u;
mpq m;
if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m)) {
return;
}
bool m_is_one = m.is_one();
bool val_is_int = value_is_int(j);
// check whether value of j is already a multiple of m.
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
return;
}
TRACE("patch_int",
tout << "TARGET j" << j << " -> [";
if (inf_l) tout << "-oo"; else tout << l;
tout << ", ";
if (inf_u) tout << "oo"; else tout << u;
tout << "]";
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {
TRACE("patch_int", tout << "patching with l: " << l << '\n';);
lra.set_value_for_nbasic_column(j, l);
}
else {
TRACE("patch_int", tout << "not patching " << l << "\n";);
}
}
else if (!inf_u) {
u = impq(m_is_one ? floor(u) : m * floor(u / m));
lra.set_value_for_nbasic_column(j, u);
TRACE("patch_int", tout << "patching with u: " << u << '\n';);
}
else {
lra.set_value_for_nbasic_column(j, impq(0));
TRACE("patch_int", tout << "patching with 0\n";);
}
}
lia_move int_solver::patch_nbasic_columns() {
settings().stats().m_patches++;
lp_assert(is_feasible());
for (unsigned j : lrac.m_r_nbasis) {
patch_nbasic_column(j);
}
lp_assert(is_feasible());
if (!has_inf_int()) {
settings().stats().m_patches_success++;
return lia_move::sat;
}
return lia_move::undef;
}
bool int_solver::has_lower(unsigned j) const {
@ -327,7 +367,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
TRACE("random_update", tout << "m = " << m << "\n";);
for (const auto &c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break;
if (!inf_l && !inf_u && l >= u) break;
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index];
@ -534,6 +574,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
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];
@ -558,6 +599,5 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
}
return true;
}
}

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

@ -24,6 +24,7 @@ Revision History:
#include "math/lp/lar_term.h"
#include "math/lp/lar_constraints.h"
#include "math/lp/hnf_cutter.h"
#include "math/lp/int_gcd_test.h"
#include "math/lp/lia_move.h"
#include "math/lp/explanation.h"
@ -39,8 +40,27 @@ class int_solver {
friend class int_gcd_test;
friend class hnf_cutter;
class patcher {
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
unsigned m_num_nbasic_patches;
unsigned m_patch_cost;
unsigned m_next_patch;
unsigned m_delay;
public:
patcher(int_solver& lia);
bool should_apply();
lia_move operator()();
void patch_nbasic_column(unsigned j);
private:
lia_move patch_nbasic_columns();
};
lar_solver& lra;
lar_core_solver& lrac;
int_gcd_test m_gcd;
patcher m_patcher;
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
@ -68,19 +88,17 @@ public:
bool at_upper(unsigned j) const;
private:
lia_move patch_nbasic_columns();
// lia_move patch_nbasic_columns();
bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
bool is_boxed(unsigned j) const;
bool is_fixed(unsigned j) const;
bool is_free(unsigned j) const;
bool value_is_int(unsigned j) const;
void set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val);
bool non_basic_columns_are_at_bounds() const;
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_run_gcd_test();
bool should_gomory_cut();
bool should_hnf_cut();
@ -90,6 +108,8 @@ 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;
public:
std::ostream& display_column(std::ostream & out, unsigned j) const;
@ -108,6 +128,6 @@ public:
bool all_columns_are_bounded() const;
void find_feasible_solution();
lia_move hnf_cut();
void patch_nbasic_column(unsigned j);
void patch_nbasic_column(unsigned j) { m_patcher.patch_nbasic_column(j); }
};
}

2
src/opt/maxres.cpp
View file

@ -286,7 +286,7 @@ public:
lbool is_sat = l_true;
if (m_hill_climb) {
/**
Give preference to cores that have large minmal values.
Give preference to cores that have large minimal values.
*/
sort_assumptions(asms);
m_last_index = std::min(m_last_index, asms.size()-1);

4
src/smt/theory_lra.cpp
View file

@ -2094,7 +2094,7 @@ public:
th.log_axiom_instantiation(body);
m.trace_stream() << "[end-of-instance]\n";
}
IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
IF_VERBOSE(4, verbose_stream() << "branch " << b << "\n";);
// branch on term >= k + 1
// branch on term <= k
// TBD: ctx().force_phase(ctx().get_literal(b));
@ -2113,7 +2113,7 @@ public:
th.log_axiom_instantiation(b);
m.trace_stream() << "[end-of-instance]\n";
}
IF_VERBOSE(2, verbose_stream() << "cut " << b << "\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()););
m_eqs.reset();
m_core.reset();