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

return the minimal dependencies for the case of a fixed to zero var in pdd_expr()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-11 17:46:29 -08:00
parent 379a1927e6
commit e17214c1c2
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1564,6 +1564,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
if (!is_monic_var(j))
return c * m_pdd_manager.mk_var(j);
u_dependency* zero_dep = dep;
// j is a monic var
dd::pdd r = m_pdd_manager.mk_val(c);
const monic& m = emons()[j];
@ -1571,7 +1572,9 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
if (m_nla_settings.grobner_subs_fixed() && var_is_fixed(k)) {
r *= m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep));
} else if (m_nla_settings.grobner_subs_fixed() == 2 && var_is_fixed_to_zero(k)) {
return m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep));
r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, zero_dep));
dep = zero_dep;
return r;
} else {
r *= m_pdd_manager.mk_var(k);
}