mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

expose comparisons with polynomials, incremental way to extract variables

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-30 16:59:50 -07:00
parent bc577b93ae
commit 39dc8861ee
2 changed files with 94 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
src/math/polynomial/polynomial.cpp
View file

@ -190,6 +190,10 @@ namespace polynomial {
}
};
bool operator==(monomial const& other) const {
return eq_proc()(this, &other);
}
static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz * sizeof(power); }
monomial(unsigned id, unsigned sz, power const * pws, unsigned h):
@ -3221,9 +3225,16 @@ namespace polynomial {
};
bool_vector m_found_vars;
void vars(polynomial const * p, var_vector & xs) {
xs.reset();
void begin_vars_incremental() {
m_found_vars.reserve(num_vars(), false);
}
void end_vars_incremental(var_vector& xs) {
// reset m_found_vars
unsigned sz = xs.size();
for (unsigned i = 0; i < sz; i++)
m_found_vars[xs[i]] = false;
}
void vars(polynomial const * p, var_vector & xs) {
unsigned sz = p->size();
for (unsigned i = 0; i < sz; i++) {
monomial * m = p->m(i);
@ -3236,10 +3247,6 @@ namespace polynomial {
}
}
}
// reset m_found_vars
sz = xs.size();
for (unsigned i = 0; i < sz; i++)
m_found_vars[xs[i]] = false;
}
typedef sbuffer<power, 32> power_buffer;
@ -6045,6 +6052,47 @@ namespace polynomial {
}
return true;
}
bool ge(polynomial const* p, polynomial const* q) {
unsigned sz1 = p->size();
unsigned sz2 = q->size();
unsigned i = 0, j = 0;
while (i < sz1 || j < sz2) {
auto * m1 = i < sz1 ? p->m(i) : q->m(j);
auto & a1 = i < sz1 ? p->a(i) : q->a(j);
auto * m2 = j < sz2 ? q->m(j) : p->m(i);
auto & a2 = j < sz2 ? q->a(j) : p->a(i);
if (i < sz1 && j == sz2 && m1->is_unit()) {
if (!m_manager.is_pos(a1))
return false;
++i;
continue;
}
if (i == sz1 && j < sz2 && m2->is_unit()) {
if (!m_manager.is_neg(a2))
return false;
++j;
continue;
}
if (i == sz1 || j == sz2)
break;
if (!(*m1 == *m2)) {
if (m_manager.is_pos(a1) && m1->is_square()) {
++i;
continue;
}
return false;
}
if (!m_manager.ge(a1, a2))
return false;
++i, ++j;
}
return i == sz1 && j == sz2;
}
// Functor used to compute the maximal degree of each variable in a polynomial p.
class var_max_degree {
@ -7228,13 +7276,33 @@ namespace polynomial {
return m_imp->is_nonneg(p);
}
bool manager::ge(polynomial const* p, polynomial const* q) {
return m_imp->ge(p, q);
}
void manager::rename(unsigned sz, var const * xs) {
return m_imp->rename(sz, xs);
}
void manager::vars(polynomial const * p, var_vector & xs) {
xs.reset();
m_imp->begin_vars_incremental();
m_imp->vars(p, xs);
m_imp->end_vars_incremental(xs);
}
void manager::vars_incremental(polynomial const * p, var_vector & xs) {
m_imp->vars(p, xs);
}
void manager::begin_vars_incremental() {
m_imp->begin_vars_incremental();
}
void manager::end_vars_incremental(var_vector & xs) {
m_imp->end_vars_incremental(xs);
}
polynomial * manager::substitute(polynomial const * p, var2mpq const & x2v) {
return m_imp->substitute(p, x2v);
@ -7293,17 +7361,20 @@ namespace polynomial {
return m_imp->eval(p, x2v, r);
}
void manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const {
std::ostream& manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const {
m->display(out, proc, user_star);
return out;
}
void manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const {
std::ostream& manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const {
SASSERT(m_imp->consistent_coeffs(p));
p->display(out, m_imp->m_manager, proc, use_star);
return out;
}
void manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const {
std::ostream& manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const {
p->display_smt2(out, m_imp->m_manager, proc);
return out;
}
};

19
src/math/polynomial/polynomial.h
View file

@ -921,6 +921,13 @@ namespace polynomial {
*/
bool is_nonneg(polynomial const * p);
/**
\brief Return true if p is always greater or equal to q.
This is an incomplete check
*/
bool ge(polynomial const* p, polynomial const* q);
/**
\brief Make sure the monomials in p are sorted using lexicographical order.
Remark: the maximal monomial is at position 0.
@ -931,6 +938,9 @@ namespace polynomial {
\brief Collect variables that occur in p into xs
*/
void vars(polynomial const * p, var_vector & xs);
void vars_incremental(polynomial const * p, var_vector & xs);
void begin_vars_incremental();
void end_vars_incremental(var_vector & xs);
/**
\brief Evaluate polynomial p using the assignment [x_1 -> v_1, ..., x_n -> v_n].
@ -1019,15 +1029,14 @@ namespace polynomial {
*/
void exact_pseudo_division_mod_d(polynomial const * p, polynomial const * q, var x, var2degree const & x2d, polynomial_ref & Q, polynomial_ref & R);
void display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const;
std::ostream& display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const;
void display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
std::ostream& display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
void display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const;
std::ostream& display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const;
friend std::ostream & operator<<(std::ostream & out, polynomial_ref const & p) {
p.m().display(out, p);
return out;
return p.m().display(out, p);
}
};