mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix in nla_ordered_lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-12-08 15:40:51 -08:00
parent 621e99284b
commit 4d7062d2a1
2 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -783,7 +783,7 @@ namespace lp {
update_x_and_inf_costs_for_columns_with_changed_bounds();
m_mpq_lar_core_solver.solve();
set_status(m_mpq_lar_core_solver.m_r_solver.get_status());
lp_assert((((lp_settings::ddd++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold());
lp_assert(((m_settings.stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold());
}

15
src/math/lp/nla_order_lemmas.cpp
View file

@ -199,20 +199,21 @@ bool order::order_lemma_on_ac_and_bc(const monic& rm_ac,
}
// Here ab is a binary factorization of m.
// Here m = ab, that is ab is binary factorization of m.
// We try to find a monic n = cd, such that |b| = |d|
// and get a lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation
// and get lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation
void order::order_lemma_on_factorization(const monic& m, const factorization& ab) {
bool sign = m.rsign();
for (factor f: ab)
sign ^= _().canonize_sign(f);
bool sign = false;
for (factor f: ab)
sign ^= f.sign();
const rational rsign = sign_to_rat(sign);
const rational fv = val(var(ab[0])) * val(var(ab[1]));
const rational mv = rsign * var_val(m);
TRACE("nla_solver",
tout << "ab.size()=" << ab.size() << "\n";
tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";);
TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
tout << "we should have mv =" << mv << " = " << fv << " = fv\n";
tout << "m = "; _().print_monic_with_vars(m, tout); tout << "\nab ="; _().print_factorization(ab, tout););
if (mv != fv && !c().has_real(m)) {
bool gt = mv > fv;
for (unsigned j = 0, k = 1; j < 2; j++, k--) {