mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add parameters to control grobner's explosure

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-09 16:56:07 -08:00
parent 7a2dc6e69e
commit bb6511b425
8 changed files with 63 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/grobner/pdd_simplifier.cpp
View file

@ -152,7 +152,7 @@ namespace dd {
s.push_equation(solver::to_simplify, dst);
}
// v has been eliminated.
SASSERT(!dst->poly().free_vars().contains(v));
// SASSERT(!dst->poly().free_vars().contains(v));
add_to_use(dst, use_list);
}
if (all_reduced) {

12
src/math/grobner/pdd_solver.cpp
View file

@ -70,26 +70,22 @@ namespace dd {
}
void solver::set_thresholds() {
void solver::set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth) {
IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
if (m_to_simplify.size() == 0)
return;
m_config.m_eqs_threshold = static_cast<unsigned>(10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size());
m_config.m_eqs_threshold = static_cast<unsigned>(eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size());
m_config.m_expr_size_limit = 0;
m_config.m_expr_degree_limit = 0;
for (equation* e: m_to_simplify) {
m_config.m_expr_size_limit = std::max(m_config.m_expr_size_limit, (unsigned)e->poly().tree_size());
m_config.m_expr_degree_limit = std::max(m_config.m_expr_degree_limit, e->poly().degree());
}
m_config.m_expr_size_limit *= 2;
m_config.m_expr_degree_limit *= 2;
m_config.m_expr_size_limit *= expr_size_growth;
m_config.m_expr_degree_limit *= expr_degree_growth;;
IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold to 10 * " << 10 * ceil(log(m_to_simplify.size())) << "* " << m_to_simplify.size() << " = " << m_config.m_eqs_threshold << "\n";
verbose_stream() << "set m_config.m_expr_size_limit to " << m_config.m_expr_size_limit << "\n";
verbose_stream() << "set m_config.m_expr_degree_limit to " << m_config.m_expr_degree_limit << "\n";
);
m_config.m_max_steps = 700;
m_config.m_max_simplified = 7000;
}
void solver::saturate() {

2
src/math/grobner/pdd_solver.h
View file

@ -138,7 +138,7 @@ public:
std::ostream& display_statistics(std::ostream& out) const;
const stats& get_stats() const { return m_stats; }
stats& get_stats() { return m_stats; }
void set_thresholds();
void set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth);
private:
bool step();

53
src/math/lp/nla_core.cpp
View file

@ -1289,7 +1289,7 @@ lbool core::inner_check(bool constraint_derived) {
clear_and_resize_active_var_set();
if (m_nla_settings.run_grobner()) {
find_nl_cluster();
run_pdd_grobner();
run_grobner();
}
}
if (done()) {
@ -1396,13 +1396,32 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
}
void core::run_pdd_grobner() {
void core::run_grobner() {
lp_settings().stats().m_grobner_calls++;
configure_grobner();
m_pdd_grobner.saturate();
bool conflict = false;
for (auto eq : m_pdd_grobner.equations()) {
if (check_pdd_eq(eq)) {
conflict = true;
break;
}
}
if (conflict) {
IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
}
else {
IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
}
}
void core::configure_grobner() {
m_pdd_grobner.reset();
try {
set_level2var_for_pdd_grobner();
set_level2var_for_grobner();
for (unsigned i : m_rows) {
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
add_row_to_grobner(m_lar_solver.A_r().m_rows[i]);
}
}
catch (...) {
@ -1422,8 +1441,6 @@ void core::run_pdd_grobner() {
}
#endif
// configure grobner
// TBD: move this code somewhere self-contained, and tune it.
double tree_size = 100;
unsigned gr_eq_size = 0;
for (auto* e : m_pdd_grobner.equations()) {
@ -1434,27 +1451,13 @@ void core::run_pdd_grobner() {
struct dd::solver::config cfg;
cfg.m_expr_size_limit = (unsigned)tree_size;
cfg.m_max_steps = gr_eq_size;
cfg.m_eqs_threshold = m_nla_settings.grobner_eqs_growth() * ceil(log(gr_eq_size + 1)) * gr_eq_size;;
cfg.m_max_simplified = m_nla_settings.grobner_max_simplified();
m_pdd_grobner.set(cfg);
m_pdd_grobner.set_thresholds();
m_pdd_grobner.set_thresholds(m_nla_settings.grobner_eqs_growth(), m_nla_settings.grobner_expr_size_growth(),
m_nla_settings.grobner_expr_degree_growth());
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
m_pdd_grobner.saturate();
bool conflict = false;
for (auto eq : m_pdd_grobner.equations()) {
if (check_pdd_eq(eq)) {
conflict = true;
break;
}
}
if (conflict) {
IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
}
else {
IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
}
}
std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
@ -1568,7 +1571,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
return r;
}
void core::add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row) {
void core::add_row_to_grobner(const vector<lp::row_cell<rational>> & row) {
u_dependency *dep = nullptr;
dd::pdd sum = m_pdd_manager.mk_val(rational(0));
for (const auto &p : row) {
@ -1639,7 +1642,7 @@ void core::set_active_vars_weights(nex_creator& nc) {
}
}
void core::set_level2var_for_pdd_grobner() {
void core::set_level2var_for_grobner() {
unsigned n = m_lar_solver.column_count();
unsigned_vector sorted_vars(n), weighted_vars(n);
for (unsigned j = 0; j < n; j++) {

7
src/math/lp/nla_core.h
View file

@ -399,7 +399,7 @@ public:
return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); },
out);
}
void run_pdd_grobner();
void run_grobner();
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
@ -407,11 +407,12 @@ public:
void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&);
unsigned get_var_weight(lpvar) const;
void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
void add_row_to_grobner(const vector<lp::row_cell<rational>> & row);
bool check_pdd_eq(const dd::solver::equation*);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
void set_level2var_for_pdd_grobner();
void set_level2var_for_grobner();
void configure_grobner();
}; // end of core
struct pp_mon {

5
src/math/lp/nla_params.pyg
View file

@ -8,7 +8,10 @@ def_module_params('nla',
('horner_frequency', UINT, 4, 'horner\'s call frequency'),
('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
('grobner', BOOL, True, 'run grobner\'s basis heuristic'),
('grobner_eqs_growth', UINT, 10, 'grobner\'s maximum number of equalities'),
('grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
('grobner_expr_size_growth', UINT, 10, 'grobner\'s maximum expr size growth'),
('grobner_expr_degree_growth', UINT, 10, 'grobner\'s maximum expr degree growth'),
('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')
))

18
src/math/lp/nla_settings.h
View file

@ -33,6 +33,10 @@ class nla_settings {
unsigned m_grobner_row_length_limit;
bool m_grobner_subs_fixed;
unsigned m_grobner_eqs_growth;
unsigned m_grobner_tree_size_growth;
unsigned m_grobner_expr_size_growth;
unsigned m_grobner_expr_degree_growth;
unsigned m_grobner_max_simplified;
public:
nla_settings() : m_run_order(true),
m_run_tangents(true),
@ -69,5 +73,19 @@ public:
unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; }
bool grobner_subs_fixed() const { return m_grobner_subs_fixed; }
bool& grobner_subs_fixed() { return m_grobner_subs_fixed; }
unsigned grobner_tree_size_growth() const { return m_grobner_tree_size_growth; }
unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; }
unsigned grobner_expr_size_growth() const { return m_grobner_expr_size_growth; }
unsigned & grobner_expr_size_growth() { return m_grobner_expr_size_growth; }
unsigned grobner_expr_degree_growth() const { return m_grobner_expr_degree_growth; }
unsigned & grobner_expr_degree_growth() { return m_grobner_expr_degree_growth; }
unsigned grobner_max_simplified() const { return m_grobner_max_simplified; }
unsigned & grobner_max_simplified() { return m_grobner_max_simplified; }
};
}

3
src/smt/theory_lra.cpp
View file

@ -457,6 +457,9 @@ class theory_lra::imp {
m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner();
m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = nla.grobner_subs_fixed();
m_nla->get_core()->m_nla_settings.grobner_eqs_growth() = nla.grobner_eqs_growth();
m_nla->get_core()->m_nla_settings.grobner_expr_size_growth() = nla.grobner_expr_size_growth();
m_nla->get_core()->m_nla_settings.grobner_expr_degree_growth() = nla.grobner_expr_degree_growth();
m_nla->get_core()->m_nla_settings.grobner_max_simplified() = nla.grobner_max_simplified();
}
}