mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

port grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-15 17:16:30 -07:00
parent 0f948d7a07
commit e987479e8a
4 changed files with 24 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nex_creator.cpp
View file

@ -189,6 +189,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
} }
bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const { bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
TRACE("nla_cn_details", tout << "a = " << *a << " , b = " << *b << "\n";);
SASSERT(is_simplified(a) && is_simplified(b)); SASSERT(is_simplified(a) && is_simplified(b));
unsigned a_deg = a->get_degree(); unsigned a_deg = a->get_degree();
unsigned b_deg = b->get_degree(); unsigned b_deg = b->get_degree();

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

@ -157,7 +157,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) { template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
c().prepare_active_var_set();
SASSERT(row.size() > 1); SASSERT(row.size() > 1);
sum.children().clear(); sum.children().clear();
for (const auto &p : row) { for (const auto &p : row) {
@ -167,8 +167,7 @@ template <typename T> void common::create_sum_from_row(const T& row, nex_creator
sum.add_child(nexvar(p.coeff(), p.var(), cn)); sum.add_child(nexvar(p.coeff(), p.var(), cn));
} }
} }
set_active_vars_weights(); }
}
void common::set_active_vars_weights() { void common::set_active_vars_weights() {
m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count()); m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());

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

@ -183,11 +183,20 @@ void nla_grobner::add_row(unsigned i) {
assert_eq_0(ns, dep); assert_eq_0(ns, dep);
} }
void nla_grobner::simplify_equations_to_process() {
for (equation *eq : m_to_process) {
eq->exp() = m_nex_creator.simplify(eq->exp());
}
}
void nla_grobner::init() { void nla_grobner::init() {
find_nl_cluster(); find_nl_cluster();
c().prepare_active_var_set();
for (unsigned i : m_rows) { for (unsigned i : m_rows) {
add_row(i); add_row(i);
} }
set_active_vars_weights();
simplify_equations_to_process();
} }
bool nla_grobner::is_trivial(equation* eq) const { bool nla_grobner::is_trivial(equation* eq) const {
@ -325,7 +334,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
m_equations_to_unfreeze.push_back(target); m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target); to_remove.push_back(target);
if (m_changed_leading_term) { if (m_changed_leading_term) {
m_to_process.insert(new_target); insert_to_process(new_target);
to_remove.push_back(target); to_remove.push_back(target);
} }
else { else {
@ -335,7 +344,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
} }
else { else {
if (m_changed_leading_term) { if (m_changed_leading_term) {
m_to_process.insert(target); insert_to_process(target);
to_remove.push_back(target); to_remove.push_back(target);
} }
} }
@ -383,7 +392,7 @@ void nla_grobner::simplify_to_process(equation* eq) {
to_delete.push_back(target); to_delete.push_back(target);
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
m_to_process.insert(eq); insert_to_process(eq);
for (equation* eq : to_remove) for (equation* eq : to_remove)
m_to_process.erase(eq); m_to_process.erase(eq);
for (equation* eq : to_delete) for (equation* eq : to_delete)
@ -612,16 +621,16 @@ void nla_grobner::display(std::ostream & out) const {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
void nla_grobner::assert_eq_0(const nex* e, ci_dependency * dep) { void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
TRACE("nla_grobner", tout << "e = " << *e << "\n";); TRACE("nla_grobner", tout << "e = " << *e << "\n";);
if (e == nullptr) if (e == nullptr)
return; return;
equation * eq = new equation(); equation * eq = new equation();
init_equation(eq, e, dep); init_equation(eq, e, dep);
m_to_process.insert(eq); insert_to_process(eq);
} }
void nla_grobner::init_equation(equation* eq, const nex*e, ci_dependency * dep) { void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
unsigned bidx = m_equations_to_delete.size(); unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx; eq->m_bidx = bidx;
eq->m_dep = dep; eq->m_dep = dep;

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

@ -41,7 +41,7 @@ class nla_grobner : common {
class equation { class equation {
unsigned m_bidx:31; //!< position at m_equations_to_delete unsigned m_bidx:31; //!< position at m_equations_to_delete
unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. unsigned m_lc:1; //!< true if equation if a linear combination of the input equations.
const nex * m_exp; //!< sorted monomials nex * m_exp; // simplified expressionted monomials
ci_dependency * m_dep; //!< justification for the equality ci_dependency * m_dep; //!< justification for the equality
friend class nla_grobner; friend class nla_grobner;
equation() {} equation() {}
@ -49,6 +49,7 @@ class nla_grobner : common {
unsigned get_num_monomials() const { return m_exp->size(); } unsigned get_num_monomials() const { return m_exp->size(); }
nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET(); nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET();
return nullptr; } return nullptr; }
nex* & exp() { return m_exp; }
ci_dependency * get_dependency() const { return m_dep; } ci_dependency * get_dependency() const { return m_dep; }
unsigned hash() const { return m_bidx; } unsigned hash() const { return m_bidx; }
bool is_linear_combination() const { return m_lc; } bool is_linear_combination() const { return m_lc; }
@ -116,13 +117,13 @@ bool simplify_processed_with_eq(equation*);
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 assert_eq_0(const nex*, ci_dependency * dep); void assert_eq_0(nex*, ci_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*&);
void init_equation(equation* eq, const nex*, ci_dependency* d); void init_equation(equation* eq, nex*, ci_dependency* d);
equation * simplify(equation const * source, equation * target); equation * simplify(equation const * source, equation * target);
// 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];
@ -141,6 +142,7 @@ bool simplify_processed_with_eq(equation*);
// } // }
std::ostream& display_dependency(std::ostream& out, ci_dependency*); std::ostream& display_dependency(std::ostream& out, ci_dependency*);
void insert_to_process(equation *eq) { m_to_process.insert(eq); }
void simplify_equations_to_process();
}; // end of grobner }; // end of grobner
} }