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

move some grobner settings to pdd_solver.m_config

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-10 11:06:01 -08:00
parent bb6511b425
commit 00e1049ff2
6 changed files with 35 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -70,17 +70,18 @@ namespace dd {
} }
void solver::set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth) { void solver::adjust_cfg() {
auto & cfg = m_config;
IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream())); IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
m_config.m_eqs_threshold = static_cast<unsigned>(eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size()); cfg.m_eqs_threshold = static_cast<unsigned>(cfg.m_eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size());
m_config.m_expr_size_limit = 0; cfg.m_expr_size_limit = 0;
m_config.m_expr_degree_limit = 0; cfg.m_expr_degree_limit = 0;
for (equation* e: m_to_simplify) { 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()); cfg.m_expr_size_limit = std::max(cfg.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()); cfg.m_expr_degree_limit = std::max(cfg.m_expr_degree_limit, e->poly().degree());
} }
m_config.m_expr_size_limit *= expr_size_growth; cfg.m_expr_size_limit *= cfg.m_expr_size_growth;
m_config.m_expr_degree_limit *= expr_degree_growth;; cfg.m_expr_degree_limit *= cfg.m_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"; 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_size_limit to " << m_config.m_expr_size_limit << "\n";

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

@ -55,6 +55,10 @@ public:
unsigned m_max_simplified; unsigned m_max_simplified;
unsigned m_random_seed; unsigned m_random_seed;
bool m_enable_exlin; bool m_enable_exlin;
unsigned m_eqs_growth;
unsigned m_expr_size_growth;
unsigned m_expr_degree_growth;
unsigned m_number_of_conflicts_to_report;
config() : config() :
m_eqs_threshold(UINT_MAX), m_eqs_threshold(UINT_MAX),
m_expr_size_limit(UINT_MAX), m_expr_size_limit(UINT_MAX),
@ -62,7 +66,11 @@ public:
m_max_steps(UINT_MAX), m_max_steps(UINT_MAX),
m_max_simplified(UINT_MAX), m_max_simplified(UINT_MAX),
m_random_seed(0), m_random_seed(0),
m_enable_exlin(false) m_enable_exlin(false),
m_eqs_growth(10),
m_expr_size_growth(10),
m_expr_degree_growth(5),
m_number_of_conflicts_to_report(1)
{} {}
}; };
@ -121,6 +129,7 @@ public:
void set(print_dep_t& pd) { m_print_dep = pd; } void set(print_dep_t& pd) { m_print_dep = pd; }
void set(config const& c) { m_config = c; } void set(config const& c) { m_config = c; }
void adjust_cfg();
void reset(); void reset();
void add(pdd const& p) { add(p, nullptr); } void add(pdd const& p) { add(p, nullptr); }
@ -138,7 +147,7 @@ public:
std::ostream& display_statistics(std::ostream& out) const; std::ostream& display_statistics(std::ostream& out) const;
const stats& get_stats() const { return m_stats; } const stats& get_stats() const { return m_stats; }
stats& get_stats() { return m_stats; } stats& get_stats() { return m_stats; }
void set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth); unsigned number_of_conflicts_to_report() const { return m_config.m_number_of_conflicts_to_report; }
private: private:
bool step(); bool step();
@ -185,7 +194,6 @@ private:
scoped_process(solver& g, equation* e): g(g), e(e) {} scoped_process(solver& g, equation* e): g(g), e(e) {}
~scoped_process(); ~scoped_process();
}; };
void update_stats_max_degree_and_size(const equation& e); void update_stats_max_degree_and_size(const equation& e);
}; };

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

@ -1401,10 +1401,13 @@ void core::run_grobner() {
configure_grobner(); configure_grobner();
m_pdd_grobner.saturate(); m_pdd_grobner.saturate();
bool conflict = false; bool conflict = false;
unsigned n = m_pdd_grobner.number_of_conflicts_to_report();
SASSERT(n > 0);
for (auto eq : m_pdd_grobner.equations()) { for (auto eq : m_pdd_grobner.equations()) {
if (check_pdd_eq(eq)) { if (check_pdd_eq(eq)) {
conflict = true; conflict = true;
break; if (--n == 0)
break;
} }
} }
if (conflict) { if (conflict) {
@ -1452,11 +1455,12 @@ void core::configure_grobner() {
cfg.m_expr_size_limit = (unsigned)tree_size; cfg.m_expr_size_limit = (unsigned)tree_size;
cfg.m_max_steps = gr_eq_size; cfg.m_max_steps = gr_eq_size;
cfg.m_max_simplified = m_nla_settings.grobner_max_simplified(); cfg.m_max_simplified = m_nla_settings.grobner_max_simplified();
cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth();
cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth();
cfg.m_expr_degree_growth = m_nla_settings.grobner_expr_degree_growth();
cfg.m_number_of_conflicts_to_report = m_nla_settings.grobner_number_of_conflicts_to_report();
m_pdd_grobner.set(cfg); m_pdd_grobner.set(cfg);
m_pdd_grobner.set_thresholds(m_nla_settings.grobner_eqs_growth(), m_nla_settings.grobner_expr_size_growth(), m_pdd_grobner.adjust_cfg();
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_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
} }

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

@ -12,6 +12,7 @@ def_module_params('nla',
('grobner_expr_size_growth', UINT, 10, 'grobner\'s maximum expr size 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_expr_degree_growth', UINT, 10, 'grobner\'s maximum expr degree growth'),
('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants') ('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')
)) ))

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

@ -37,6 +37,7 @@ class nla_settings {
unsigned m_grobner_expr_size_growth; unsigned m_grobner_expr_size_growth;
unsigned m_grobner_expr_degree_growth; unsigned m_grobner_expr_degree_growth;
unsigned m_grobner_max_simplified; unsigned m_grobner_max_simplified;
unsigned m_grobner_number_of_conflicts_to_report;
public: public:
nla_settings() : m_run_order(true), nla_settings() : m_run_order(true),
m_run_tangents(true), m_run_tangents(true),
@ -86,6 +87,9 @@ public:
unsigned grobner_max_simplified() const { return m_grobner_max_simplified; } unsigned grobner_max_simplified() const { return m_grobner_max_simplified; }
unsigned & grobner_max_simplified() { return m_grobner_max_simplified; } unsigned & grobner_max_simplified() { return m_grobner_max_simplified; }
unsigned grobner_number_of_conflicts_to_report() const { return m_grobner_number_of_conflicts_to_report; }
unsigned & grobner_number_of_conflicts_to_report() { return m_grobner_number_of_conflicts_to_report; }
}; };
} }

1
src/smt/theory_lra.cpp
View file

@ -460,6 +460,7 @@ class theory_lra::imp {
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_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_expr_degree_growth() = nla.grobner_expr_degree_growth();
m_nla->get_core()->m_nla_settings.grobner_max_simplified() = nla.grobner_max_simplified(); m_nla->get_core()->m_nla_settings.grobner_max_simplified() = nla.grobner_max_simplified();
m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = nla.grobner_cnfl_to_report();
} }
} }