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

more fixes in patching of monomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-02 14:47:06 -07:00
parent 2d01c64d2c
commit 55329ea935
3 changed files with 33 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lar_solver.cpp
View file

@ -2398,7 +2398,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
VERIFY(remove_from_basis(j)); VERIFY(remove_from_basis(j));
} }
impq ival(val); impq ival(val);
if (!inside_bounds(j, ival)) if (!inside_bounds(j, ival) || blocker(j))
return false; return false;
impq delta = get_column_value(j) - ival; impq delta = get_column_value(j) - ival;
@ -2414,6 +2414,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
} }
set_column_value(j, ival); set_column_value(j, ival);
report_change(j);
for (const auto &c : A_r().column(j)) { for (const auto &c : A_r().column(j)) {
unsigned row_index = c.var(); unsigned row_index = c.var();
const mpq & a = c.coeff(); const mpq & a = c.coeff();

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

@ -1379,6 +1379,21 @@ bool in_power(const svector<lpvar>& vs, unsigned l) {
return (l != 0 && vs[l - 1] == k) || (l + 1 < vs.size() && k == vs[l + 1]); return (l != 0 && vs[l - 1] == k) || (l + 1 < vs.size() && k == vs[l + 1]);
} }
bool core::to_refine_is_correct() const {
for (unsigned j = 0; j < m_lar_solver.number_of_vars(); j++) {
if (!emons().is_monic_var(j)) continue;
bool valid = check_monic(emons()[j]);
if (valid != m_to_refine.contains(j)) {
TRACE("nla_solver", tout << "inconstency in m_to_refine : ";
print_monic(emons()[j], tout) << "\n";
if (valid) tout << "should NOT be there\n";
else tout << "should be there\n";);
return false;
}
}
return true;
}
// looking for any real var to patch // looking for any real var to patch
void core::patch_monomial_with_real_var(lpvar j) { void core::patch_monomial_with_real_var(lpvar j) {
const monic& m = emons()[j]; const monic& m = emons()[j];
@ -1393,11 +1408,23 @@ void core::patch_monomial_with_real_var(lpvar j) {
return; return;
if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) { if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) {
// SASSERT(mul_val(m) == var_val(m)); SASSERT(to_refine_is_correct());
m_to_refine.erase(j);
return; return;
} }
// handle perfect squares
if (m.vars().size() == 2 && m.vars()[0] == m.vars()[1]) {
rational root;
if (v.is_perfect_square(root)) {
lpvar k = m.vars()[0];
if (!var_is_int(k) &&
!var_is_used_in_a_correct_monic(k) &&
(try_to_patch(k, root, m) || try_to_patch(k, -root, m))
) {
}
}
return;
}
// We have v != abc. Let us suppose we patch b. Then b should // We have v != abc. Let us suppose we patch b. Then b should
// be equal to v/ac = v/(abc/b) = b(v/abc) // be equal to v/ac = v/(abc/b) = b(v/abc)
rational r = val(j) / v; rational r = val(j) / v;

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

@ -420,6 +420,7 @@ public:
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&, const monic&); bool try_to_patch(lpvar, const rational&, const monic&);
bool to_refine_is_correct() const;
}; // end of core }; // end of core
struct pp_mon { struct pp_mon {