mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

limit the row length in horner's scheme

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-23 11:01:17 -07:00
parent b075d3923e
commit bf79d93d51
4 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/horner.cpp
View file

@ -40,6 +40,10 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
template <typename T> template <typename T>
bool horner::row_is_interesting(const T& row) const { bool horner::row_is_interesting(const T& row) const {
TRACE("nla_solver_details", m_core->print_term(row, tout);); TRACE("nla_solver_details", m_core->print_term(row, tout););
if (row.size() > m_core->m_settings.horner_row_length_limit()) {
TRACE("nla_solver_details", tout << "disregard\n";);
return false;
}
SASSERT(row_has_monomial_to_refine(row)); SASSERT(row_has_monomial_to_refine(row));
m_row_var_set.clear(); m_row_var_set.clear();
for (const auto& p : row) { for (const auto& p : row) {

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

@ -4,6 +4,8 @@ def_module_params('nla',
('order', BOOL, True, 'run order lemmas'), ('order', BOOL, True, 'run order lemmas'),
('tangents', BOOL, True, 'run tangent lemmas'), ('tangents', BOOL, True, 'run tangent lemmas'),
('horner', BOOL, True, 'run horner\'s heuristic'), ('horner', BOOL, True, 'run horner\'s heuristic'),
('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')
)) ))

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

@ -26,11 +26,14 @@ class nla_settings {
bool m_run_horner; bool m_run_horner;
// how often to call the horner heuristic // how often to call the horner heuristic
unsigned m_horner_frequency; unsigned m_horner_frequency;
unsigned m_horner_row_length_limit;
public: public:
nla_settings() : m_run_order(true), nla_settings() : m_run_order(true),
m_run_tangents(true), m_run_tangents(true),
m_run_horner(true), m_run_horner(true),
m_horner_frequency(4) {} m_horner_frequency(4),
m_horner_row_length_limit(10)
{}
bool run_order() const { return m_run_order; } bool run_order() const { return m_run_order; }
bool& run_order() { return m_run_order; } bool& run_order() { return m_run_order; }
@ -42,6 +45,8 @@ public:
bool& run_horner() { return m_run_horner; } bool& run_horner() { return m_run_horner; }
unsigned horner_frequency() const { return m_horner_frequency; } unsigned horner_frequency() const { return m_horner_frequency; }
unsigned& horner_frequency() { return m_horner_frequency; } unsigned& horner_frequency() { return m_horner_frequency; }
unsigned horner_row_length_limit() const { return m_horner_row_length_limit; }
unsigned& horner_row_length_limit() { return m_horner_row_length_limit; }
}; };
} }

2
src/smt/theory_lra.cpp
View file

@ -451,6 +451,8 @@ class theory_lra::imp {
m_nla->get_core()->m_settings.run_order() = nla.order(); m_nla->get_core()->m_settings.run_order() = nla.order();
m_nla->get_core()->m_settings.run_tangents() = nla.tangents(); m_nla->get_core()->m_settings.run_tangents() = nla.tangents();
m_nla->get_core()->m_settings.run_horner() = nla.horner(); m_nla->get_core()->m_settings.run_horner() = nla.horner();
m_nla->get_core()->m_settings.horner_frequency() = nla.horner_frequency();
m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit();
} }
} }