mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

adding more aggressive patching in nl

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-27 17:46:37 -07:00
parent 6a5579341d
commit c58bd3105b
6 changed files with 55 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -265,8 +265,8 @@ class lar_solver : public column_namer {
void collect_rounded_rows_to_fix();
void register_normalized_term(const lar_term&, lpvar);
void deregister_normalized_term(const lar_term&);
bool inside_bounds(lpvar, const impq&) const;
public:
bool inside_bounds(lpvar, const impq&) const;
inline void set_column_value(unsigned j, const impq& v) {
m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
}
@ -306,6 +306,9 @@ public:
bool column_corresponds_to_term(unsigned) const;
inline unsigned row_count() const { return A_r().row_count(); }
bool var_is_registered(var_index vj) const;
void clear_inf_set() {
m_mpq_lar_core_solver.m_r_solver.inf_set().clear();
}
inline void remove_column_from_inf_set(unsigned j) {
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
}
@ -367,7 +370,7 @@ public:
}
impq ival(val);
if (!inside_bounds(j, ival) || blocker(j))
if (!blocker(j, ival))
return false;
impq delta = get_column_value(j) - ival;
@ -378,7 +381,7 @@ public:
impq rj_new_val = a * delta + get_column_value(rj);
// if (column_is_int(rj) && !rj_new_val.is_int())
// return false;
if (blocker(rj))
if (blocker(rj, rj_new_val))
return false;
}

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

@ -1288,10 +1288,10 @@ bool core::has_real(const monic& m) const {
return false;
}
bool core::patch_blocker(lpvar u, const monic& m) const {
bool core::patch_blocker(lpvar u, const monic& m, const lp::impq& ival) const {
SASSERT(m_to_refine.contains(m.var()));
if (m_cautious_patching && !m_lar_solver.inside_bounds(u, ival))
return false;
if (var_breaks_correct_monic(u)) {
TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
return true;
@ -1307,7 +1307,8 @@ bool core::patch_blocker(lpvar u, const monic& m) const {
bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
auto call_before_change = [this](lpvar u) { m_changes_of_patch.insert_if_not_there(u, val(u)); };
auto blocker = [this, k, m](lpvar u) { return u != k && patch_blocker(u, m); };
auto blocker = [this, k, m](lpvar u, const lp::impq& v)
{ return u != k && patch_blocker(u, m, v); };
auto change_report = [this](lpvar u) { update_to_refine_of_var(u); };
return m_lar_solver.try_to_patch(k, v, blocker, call_before_change, change_report);
}
@ -1390,6 +1391,7 @@ void core::restore_patched_values() {
void core::patch_monomials() {
m_changes_of_patch.reset();
m_cautious_patching = true;
auto to_refine = m_to_refine.index();
// the rest of the function might change m_to_refine, so have to copy
unsigned sz = to_refine.size();
@ -1400,19 +1402,37 @@ void core::patch_monomials() {
if (m_to_refine.size() == 0)
break;
}
if (m_to_refine.size()) {
restore_patched_values();
if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching()) {
return;
}
m_cautious_patching = false; //
NOT_IMPLEMENTED_YET(); // have to repeat the patching
m_lar_solver.push();
constrain_nl_in_tableau();
if (solve_tableau() && integrality_holds()) {
m_lar_solver.pop(1);
} else {
m_lar_solver.pop();
restore_patched_values();
m_lar_solver.clear_inf_set();
}
NOT_IMPLEMENTED_YET();
/*
If the tableau is not feasible we need to fix all non-linear
vars that do not satisfy var_breaks_correct_monic()
and find a feasible solution, fix the integral values too.
*/
TRACE("nla_solver", tout << "sz = " << m_to_refine.size() << "\n";);
SASSERT(m_lar_solver.ax_is_correct());
}
void core::constrain_nl_in_tableau() {
NOT_IMPLEMENTED_YET();
}
bool core::solve_tableau() {
NOT_IMPLEMENTED_YET();
}
bool core::integrality_holds() {
NOT_IMPLEMENTED_YET();
}
lbool core::check(vector<lemma>& l_vec) {
lp_settings().stats().m_nla_calls++;
TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
@ -1433,7 +1453,7 @@ lbool core::check(vector<lemma>& l_vec) {
set_use_nra_model(false);
if (l_vec.empty() && !done() && m_nla_settings.propagate_bounds())
if (l_vec.empty() && !done())
m_monomial_bounds();
if (l_vec.empty() && !done() && need_run_horner())

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

@ -175,7 +175,9 @@ public:
reslimit& m_reslim;
bool m_use_nra_model;
nra::solver m_nra;
private:
bool m_cautious_patching;
public:
void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j);
@ -472,7 +474,7 @@ public:
void update_to_refine_of_var(lpvar j);
bool try_to_patch(lpvar, const rational&, const monic&);
bool to_refine_is_correct() const;
bool patch_blocker(lpvar u, const monic& m) const;
bool patch_blocker(lpvar u, const monic& m, const lp::impq&) const;
bool has_big_num(const monic&) const;
bool var_is_big(lpvar) const;
bool has_real(const factorization&) const;
@ -482,6 +484,9 @@ public:
void collect_statistics(::statistics&);
private:
void restore_patched_values();
void constrain_nl_in_tableau();
bool solve_tableau();
bool integrality_holds();
}; // end of core
struct pp_mon {

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

@ -30,8 +30,8 @@ class nla_settings {
unsigned m_grobner_quota;
unsigned m_grobner_frequency;
bool m_run_nra;
// propagate bounds
bool m_bp;
// expensive patching
bool m_expensive_patching;
public:
nla_settings() : m_run_order(true),
m_run_tangents(true),
@ -45,10 +45,8 @@ public:
m_grobner_quota(0),
m_grobner_frequency(4),
m_run_nra(false),
m_bp(false)
m_expensive_patching(false)
{}
bool propagate_bounds() const { return m_bp; }
bool& propagate_bounds() { return m_bp; }
unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;}
unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;}
bool run_order() const { return m_run_order; }
@ -57,6 +55,9 @@ public:
bool run_tangents() const { return m_run_tangents; }
bool& run_tangents() { return m_run_tangents; }
bool expensive_patching() const { return m_expensive_patching; }
bool& expensive_patching() { return m_expensive_patching; }
bool run_horner() const { return m_run_horner; }
bool& run_horner() { return m_run_horner; }

2
src/smt/params/smt_params_helper.pyg
View file

@ -48,7 +48,7 @@ def_module_params(module_name='smt',
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),
('arith.nl.order', BOOL, True, 'run order lemmas'),
('arith.nl.bp', BOOL, True, 'propagate bounds on monomials'),
('arith.nl.expp', BOOL, False, 'expensive patching'),
('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),

2
src/smt/theory_lra.cpp
View file

@ -413,7 +413,7 @@ class theory_lra::imp {
m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().propagate_bounds() = prms.arith_nl_bp();
m_nla->settings().expensive_patching() = prms.arith_nl_expp();
}
}