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

fix arith errors add_row for nex grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-30 12:24:06 -08:00
parent c5187902ad
commit 361964f173
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_common.cpp
View file

@ -134,7 +134,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
} }
return cn.mk_scalar(c().m_lar_solver.column_lower_bound(j).x); return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x);
} }
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
@ -144,13 +144,13 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
nex_creator::mul_factory mf(cn); nex_creator::mul_factory mf(cn);
mf *= coeff; mf *= coeff;
for (lpvar k : m.vars()) { for (lpvar k : m.vars()) {
if (c().var_is_fixed(j)) { if (c().var_is_fixed(k)) {
if (dep_manager) { if (dep_manager) {
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
} }
mf *= c().m_lar_solver.column_lower_bound(j).x; mf *= c().m_lar_solver.column_lower_bound(k).x;
} else { } else {
c().insert_to_active_var_set(k); c().insert_to_active_var_set(k);
mf *= cn.mk_var(k); mf *= cn.mk_var(k);
@ -184,8 +184,8 @@ template <typename T> u_dependency* common::create_sum_from_row(const T& row,
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
if (uc + 1) if (uc + 1)
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc)); dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
sum += e;
} }
sum += e;
} }
return dep; return dep;
} }

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

@ -726,6 +726,10 @@ std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency*
#ifdef Z3DEBUG #ifdef Z3DEBUG
bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) { bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) {
if (ab->is_var()) {
return b->size() == 0 || (b->get_degree() == 1 && b->get_child_exp(0)->to_var().var() ==
ab->to_var().var());
}
nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul(); nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul();
nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b); nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b);
ab_clone.m_coeff = rational(1); ab_clone.m_coeff = rational(1);