mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

work on Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-07 17:17:18 -07:00
parent 0c126031b0
commit 86357de6fe
2 changed files with 27 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -172,32 +172,20 @@ nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * &
void nla_grobner::add_row(unsigned i) { void nla_grobner::add_row(unsigned i) {
const auto& row = c().m_lar_solver.A_r().m_rows[i]; const auto& row = c().m_lar_solver.A_r().m_rows[i];
TRACE("non_linear", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout);); TRACE("nla_grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout););
nex * row_nex = nullptr; nex_sum * ns = m_nex_creator.mk_sum();
/* v_dependency * dep = nullptr; create_sum_from_row(row, m_nex_creator, *ns);
m_tmp_var_set.reset(); TRACE("nla_grobner", tout << "ns = " << *ns << "\n";);
for (const auto & p : row) { ci_dependency * dep = nullptr;
rational coeff = p.coeff(); m_tmp_var_set.clear();
lpvar j = p.var(); assert_eq_0(ns, dep);
// TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";);
nex * new_m = mk_monomial(coeff, j, dep, m_tmp_var_set);
TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
if (new_m)
monomials.push_back(new_m);
}
assert_eq_0(monomials, dep);*/
}
void nla_grobner::add_monomial_def(lpvar) {
NOT_IMPLEMENTED_YET();
} }
void nla_grobner::init() { void nla_grobner::init() {
find_nl_cluster(); find_nl_cluster();
for (unsigned i : m_rows) { for (unsigned i : m_rows) {
add_row(i); add_row(i);
} }
for (lpvar j : m_active_vars) {
add_monomial_def(j);
}
} }
bool nla_grobner::is_trivial(equation* eq) const { bool nla_grobner::is_trivial(equation* eq) const {
@ -419,9 +407,23 @@ void nla_grobner::display(std::ostream & out) const {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
void nla_grobner::assert_eq_0(ptr_buffer<monomial> &, v_dependency * dep) { void nla_grobner::assert_eq_0(const nex* e, ci_dependency * dep) {
NOT_IMPLEMENTED_YET(); if (e == nullptr)
return;
equation * eq = new equation();
init_equation(eq, dep);
m_to_process.insert(eq);
} }
void nla_grobner::init_equation(equation* e, ci_dependency * dep) {
NOT_IMPLEMENTED_YET();
/* eq->m_scope_lvl = get_scope_level();
unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx;
eq->m_dep = d;
eq->m_lc = true;
m_equations_to_delete.push_back(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);*/
}
} // end of nla namespace } // end of nla namespace

5
src/math/lp/nla_grobner.h
View file

@ -131,8 +131,7 @@ private:
bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight); bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
bool internalize_gb_eq(equation*); bool internalize_gb_eq(equation*);
void add_row(unsigned); void add_row(unsigned);
void add_monomial_def(lpvar); void assert_eq_0(const nex*, ci_dependency * dep);
void assert_eq_0(ptr_buffer<monomial> &, v_dependency * dep);
void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&); void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&);
nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&); nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&);
@ -143,6 +142,8 @@ private:
return rational(1); return rational(1);
} }
void init_equation(equation* eq, ci_dependency* d);
// bool less_than_on_vars(lpvar a, lpvar b) const { // bool less_than_on_vars(lpvar a, lpvar b) const {
// const auto &aw = m_nex_creatorm_active_vars_weights[a]; // const auto &aw = m_nex_creatorm_active_vars_weights[a];
// const auto &ab = m_active_vars_weights[b]; // const auto &ab = m_active_vars_weights[b];