mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Nikolaj fixes pdd_manager::reduce() to work with the changed order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-10 12:02:34 -08:00
parent 00e1049ff2
commit 7ad95aa5d2
5 changed files with 246 additions and 207 deletions
Download patch file Download diff file Expand all files Collapse all files

105
src/math/dd/dd_pdd.cpp
View file

@ -184,7 +184,8 @@ namespace dd {
case pdd_reduce_op:
if (is_zero(q)) return p;
if (is_val(p)) return p;
if (!is_val(q) && level(p) < level(q)) return p;
if (degree(p) < degree(q)) return p;
if (level(first_leading(q)) > level(p)) return p;
break;
case pdd_subst_val_op:
while (!is_val(q) && !is_val(p)) {
@ -310,18 +311,25 @@ namespace dd {
}
break;
case pdd_reduce_op:
if (level_p > level_q) {
if (level(first_leading(q)) < level_p) {
push(apply_rec(lo(p), q, op));
push(apply_rec(hi(p), q, op));
if (read(2) == lo(p) && read(1) == hi(p)) {
PDD plo = read(2), phi = read(1);
if (plo == lo(p) && phi == hi(p)) {
r = p;
}
else {
r = make_node(level_p, read(2), read(1));
else if (level(plo) < level_p && level(phi) <= level(p)) {
r = make_node(level_p, plo, phi);
}
else {
push(apply_rec(phi, m_var2pdd[var(p)], pdd_mul_op));
push(apply_rec(read(1), plo, pdd_add_op));
r = read(1);
npop = 4;
}
}
else {
SASSERT(level_p == level_q);
SASSERT(level(first_leading(q)) == level_p);
r = reduce_on_match(p, q);
npop = 0;
}
@ -384,11 +392,16 @@ namespace dd {
return r;
}
// q = lt(a)/lt(b), return a - b*q
//
// produce polynomial where a is reduced by b.
// all monomials in a that are divisible by lm(b)
// are replaced by (b - lt(b))/lm(b)
//
pdd_manager::PDD pdd_manager::reduce_on_match(PDD a, PDD b) {
SASSERT(level(a) == level(b) && !is_val(a) && !is_val(b));
SASSERT(level(first_leading(b)) == level(a));
SASSERT(!is_val(a) && !is_val(b));
push(a);
while (lm_divides(b, a)) {
while (lm_occurs(b, a)) {
push(lt_quotient(b, a));
push(apply_rec(read(1), b, pdd_mul_op));
push(apply_rec(a, read(1), pdd_add_op));
@ -400,47 +413,65 @@ namespace dd {
return a;
}
// true if leading monomial of p divides leading monomial of q
bool pdd_manager::lm_divides(PDD p, PDD q) const {
// true if leading monomial of p divides a monomial of q
bool pdd_manager::lm_occurs(PDD p, PDD q) const {
p = first_leading(p);
q = first_leading(q);
while (true) {
if (is_val(p)) return true;
if (is_val(q)) return false;
if (level(p) > level(q)) return false;
if (level(p) == level(q)) {
if (level(p) > level(q)) {
return false;
}
else if (level(p) == level(q)) {
p = next_leading(p);
q = next_leading(q);
q = hi(q);
}
else if (lm_occurs(p, hi(q))) {
return true;
}
else {
q = next_leading(q);
q = lo(q);
}
}
}
// return minus quotient -r, such that lt(q) = lt(p)*r
// assume lm_divides(p, q)
// return minus quotient -r, such that lt(p)*r
// is a monomial in q.
// assume lm_occurs(p, q)
pdd_manager::PDD pdd_manager::lt_quotient(PDD p, PDD q) {
SASSERT(lm_divides(p, q));
SASSERT(lm_occurs(p, q));
p = first_leading(p);
q = first_leading(q);
SASSERT(is_val(p) || !is_val(q));
if (is_val(p)) {
if (is_val(q)) {
SASSERT(!val(p).is_zero());
return imk_val(-val(q) / val(p));
while (!is_val(p)) {
SASSERT(level(p) <= level(q));
SASSERT(lm_occurs(p, q));
if (level(p) == level(q)) {
p = next_leading(p);
q = lm_occurs(p, hi(q)) ? hi(q) : lo(q);
}
else if (lm_occurs(p, hi(q))) {
return lt_quotient_hi(p, q);
}
else {
q = lo(q);
}
}
else if (level(p) == level(q)) {
return lt_quotient(next_leading(p), next_leading(q));
SASSERT(!is_zero(p));
if (is_val(q)) {
return imk_val(-val(q) / val(p));
}
else {
return lt_quotient_hi(p, q);
}
}
SASSERT(!is_val(q));
push(lt_quotient(p, next_leading(q)));
pdd_manager::PDD pdd_manager::lt_quotient_hi(PDD p, PDD q) {
SASSERT(lm_occurs(p, hi(q)));
push(lt_quotient(p, hi(q)));
PDD r = apply_rec(m_var2pdd[var(q)], read(1), pdd_mul_op);
pop(1);
return r;
}
//
@ -606,19 +637,6 @@ namespace dd {
return p;
}
/*
Determine whether p is a linear polynomials.
A linear polynomial is of the form x*v1 + y*v2 + .. + vn,
where v1, v2, .., vn are values.
*/
bool pdd_manager::is_linear(PDD p) {
while (true) {
if (is_val(p)) return true;
if (!is_val(hi(p))) return false;
p = lo(p);
}
}
bool pdd_manager::is_linear(pdd const& p) {
return is_linear(p.root);
}
@ -853,6 +871,9 @@ namespace dd {
}
unsigned pdd_manager::degree(PDD p) const {
if (p == zero_pdd || p == one_pdd) {
return 0;
}
if (is_dmarked(p)) {
return m_degree[p];
}

6
src/math/dd/dd_pdd.h
View file

@ -46,7 +46,6 @@ namespace dd {
public:
enum semantics { free_e, mod2_e, zero_one_vars_e };
private:
friend test;
friend pdd;
friend pdd_iterator;
@ -178,8 +177,9 @@ namespace dd {
PDD minus_rec(PDD p);
PDD reduce_on_match(PDD a, PDD b);
bool lm_divides(PDD p, PDD q) const;
bool lm_occurs(PDD p, PDD q) const;
PDD lt_quotient(PDD p, PDD q);
PDD lt_quotient_hi(PDD p, PDD q);
PDD imk_val(rational const& r);
void init_value(const_info& info, rational const& r);
@ -279,7 +279,7 @@ namespace dd {
pdd reduce(pdd const& a, pdd const& b);
pdd subst_val(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
bool is_linear(PDD p);
bool is_linear(PDD p) { return degree(p) == 1; }
bool is_linear(pdd const& p);
bool is_binary(PDD p);

4
src/math/grobner/pdd_solver.cpp
View file

@ -110,7 +110,7 @@ namespace dd {
void solver::scoped_process::done() {
pdd p = e->poly();
SASSERT(!p.is_val());
if (p.hi().is_val()) {
if (p.degree() == 1) {
g.push_equation(solved, e);
}
else {
@ -462,7 +462,7 @@ namespace dd {
VERIFY(e->idx() == i);
++i;
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val()) {
if (p.degree() == 1) {
unsigned v = p.var();
SASSERT(!head_vars.contains(v));
head_vars.insert(v);

1
src/math/grobner/pdd_solver.h
View file

@ -194,6 +194,7 @@ private:
scoped_process(solver& g, equation* e): g(g), e(e) {}
~scoped_process();
};
void update_stats_max_degree_and_size(const equation& e);
};