mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

cleaner code in add row to gb

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-02 12:21:41 -08:00
parent ca9ed38ff5
commit 8596fb2ae6
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1536,14 +1536,17 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
}
}
const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
unsigned lc, uc;
m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
return m_lar_solver.column_lower_bound(j).x;
}
dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
if (var_is_fixed(j)) {
unsigned lc, uc;
m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
return m_pdd_manager.mk_val(c * m_lar_solver.column_lower_bound(j).x);
return m_pdd_manager.mk_val(c * val_of_fixed_var_with_deps(j, dep));
}
if (!is_monic_var(j))
@ -1554,11 +1557,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
const monic& m = emons()[j];
for (lpvar k : m.vars()) {
if (var_is_fixed(k)) {
unsigned lc, uc;
r *= m_pdd_manager.mk_val(m_lar_solver.column_lower_bound(k).x);
m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
r *= m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep));
} else {
r *= m_pdd_manager.mk_var(k);
}

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

@ -409,6 +409,7 @@ public:
unsigned get_var_weight(lpvar) const;
void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
bool check_pdd_eq(const dd::grobner::equation*);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
void set_level2var_for_pdd_grobner();
}; // end of core