mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

patch real columns when they are factors

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-31 16:50:02 -07:00
parent 35c59e3ca0
commit 086149f3f8
2 changed files with 35 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1332,8 +1332,10 @@ bool core::elists_are_consistent(bool check_in_model) const {
bool core::var_is_used_in_a_correct_monic(lpvar j) const { bool core::var_is_used_in_a_correct_monic(lpvar j) const {
for (const monic & m : emons().get_use_list(j)) { for (const monic & m : emons().get_use_list(j)) {
if (!m_to_refine.contains(m.var())) if (!m_to_refine.contains(m.var())) {
TRACE("nla_solver", tout << "j" << j << " is used in a correct monic \n";);
return true; return true;
}
} }
return false; return false;
} }
@ -1356,29 +1358,44 @@ void core::update_to_refine_of_var(lpvar j) {
} }
bool core::try_to_patch(lpvar k, const rational& v) {
return m_lar_solver.try_to_patch(k, v,
[this](lpvar u) { return var_is_used_in_a_correct_monic(u);},
[this](lpvar u) { update_to_refine_of_var(u); });
}
void core::patch_real_var(lpvar j) {
SASSERT(!var_is_int(j)); // looking for any real var to patch
rational v = mul_val(emons()[j]); void core::patch_monomial_with_real_var(lpvar j) {
if (val(j) == v) const monic& m = emons()[j];
rational v = mul_val(m);
if (val(j) == v || val(j).is_zero() || v.is_zero()) // correct or a lemma will catch it
return; return;
if (var_is_used_in_a_correct_monic(j)) if (!var_is_int(j) &&
return; !var_is_used_in_a_correct_monic(j)
if(m_lar_solver.try_to_patch(j, v, && try_to_patch(j, v)) {
[this](lpvar k) { return var_is_used_in_a_correct_monic(k);},
[this](lpvar k) { update_to_refine_of_var(k); }))
m_to_refine.erase(j); m_to_refine.erase(j);
} else {
rational r = val(j) / v;
for (lpvar k: m.vars()) {
if (var_is_int(k)) continue;
if (var_is_used_in_a_correct_monic(k))
continue;
if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
m_to_refine.erase(j);
}
}
}
} }
void core::patch_real_vars() { void core::patch_monomials_with_real_vars() {
auto to_refine = m_to_refine.index(); auto to_refine = m_to_refine.index();
// the rest of the function might change m_to_refine, so have to copy // the rest of the function might change m_to_refine, so have to copy
for (lpvar j : to_refine) { for (lpvar j : to_refine) {
if (var_is_int(j)) patch_monomial_with_real_var(j);
continue;
patch_real_var(j);
} }
SASSERT(m_lar_solver.ax_is_correct()); SASSERT(m_lar_solver.ax_is_correct());
} }
@ -1394,7 +1411,7 @@ lbool core::check(vector<lemma>& l_vec) {
} }
init_to_refine(); init_to_refine();
patch_real_vars(); patch_monomials_with_real_vars();
if (m_to_refine.is_empty()) { if (m_to_refine.is_empty()) {
return l_true; return l_true;
} }

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

@ -415,10 +415,11 @@ public:
bool influences_nl_var(lpvar) const; bool influences_nl_var(lpvar) const;
bool is_nl_var(lpvar) const; bool is_nl_var(lpvar) const;
bool is_used_in_monic(lpvar) const; bool is_used_in_monic(lpvar) const;
void patch_real_vars(); void patch_monomials_with_real_vars();
void patch_real_var(lpvar); void patch_monomial_with_real_var(lpvar);
bool var_is_used_in_a_correct_monic(lpvar) const; bool var_is_used_in_a_correct_monic(lpvar) const;
void update_to_refine_of_var(lpvar j); void update_to_refine_of_var(lpvar j);
bool try_to_patch(lpvar, const rational&);
}; // end of core }; // end of core
struct pp_mon { struct pp_mon {