mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
fixing leading term computation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
57846e50fa
commit
301f9598a4
2 changed files with 85 additions and 28 deletions
|
|
@ -27,6 +27,7 @@ namespace dd {
|
|||
m_spare_entry = nullptr;
|
||||
m_max_num_nodes = 1 << 24; // up to 16M nodes
|
||||
m_mark_level = 0;
|
||||
m_dmark_level = 0;
|
||||
m_disable_gc = false;
|
||||
m_is_new_node = false;
|
||||
m_semantics = s;
|
||||
|
|
@ -398,15 +399,18 @@ namespace dd {
|
|||
|
||||
// true if leading monomial of p divides leading monomial of q
|
||||
bool pdd_manager::lm_divides(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)) {
|
||||
p = hi(p); q = hi(q);
|
||||
p = next_leading(p);
|
||||
q = next_leading(q);
|
||||
}
|
||||
else {
|
||||
q = hi(q);
|
||||
q = next_leading(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -415,6 +419,8 @@ namespace dd {
|
|||
// assume lm_divides(p, q)
|
||||
pdd_manager::PDD pdd_manager::lt_quotient(PDD p, PDD q) {
|
||||
SASSERT(lm_divides(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)) {
|
||||
|
|
@ -423,12 +429,15 @@ namespace dd {
|
|||
}
|
||||
}
|
||||
else if (level(p) == level(q)) {
|
||||
return lt_quotient(hi(p), hi(q));
|
||||
return lt_quotient(next_leading(p), next_leading(q));
|
||||
}
|
||||
push(lt_quotient(p, hi(q)));
|
||||
|
||||
SASSERT(!is_val(q));
|
||||
push(lt_quotient(p, next_leading(q)));
|
||||
PDD r = apply_rec(m_var2pdd[var(q)], read(1), pdd_mul_op);
|
||||
pop(1);
|
||||
return r;
|
||||
return r;
|
||||
|
||||
}
|
||||
|
||||
//
|
||||
|
|
@ -450,13 +459,13 @@ namespace dd {
|
|||
|
||||
bool pdd_manager::common_factors(pdd const& a, pdd const& b, unsigned_vector& p, unsigned_vector& q, rational& pc, rational& qc) {
|
||||
p.reset(); q.reset();
|
||||
PDD x = a.root, y = b.root;
|
||||
PDD x = first_leading(a.root), y = first_leading(b.root);
|
||||
bool has_common = false;
|
||||
while (true) {
|
||||
if (is_val(x) || is_val(y)) {
|
||||
if (!has_common) return false;
|
||||
while (!is_val(y)) q.push_back(var(y)), y = hi(y);
|
||||
while (!is_val(x)) p.push_back(var(x)), x = hi(x);
|
||||
while (!is_val(y)) q.push_back(var(y)), y = next_leading(y);
|
||||
while (!is_val(x)) p.push_back(var(x)), x = next_leading(x);
|
||||
pc = val(x);
|
||||
qc = val(y);
|
||||
if (m_semantics != mod2_e && pc.is_int() && qc.is_int()) {
|
||||
|
|
@ -468,24 +477,25 @@ namespace dd {
|
|||
}
|
||||
if (level(x) == level(y)) {
|
||||
has_common = true;
|
||||
x = hi(x);
|
||||
y = hi(y);
|
||||
x = next_leading(x);
|
||||
y = next_leading(y);
|
||||
}
|
||||
else if (level(x) > level(y)) {
|
||||
p.push_back(var(x));
|
||||
x = hi(x);
|
||||
x = next_leading(x);
|
||||
}
|
||||
else {
|
||||
q.push_back(var(y));
|
||||
y = hi(y);
|
||||
y = next_leading(y);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* Compare leading monomials.
|
||||
/*.
|
||||
* The pdd format makes lexicographic comparison easy: compare based on
|
||||
* the top variable and descend depending on whether hi(x) == hi(y)
|
||||
*
|
||||
* NB. this does not compare leading monomials.
|
||||
*/
|
||||
bool pdd_manager::lt(pdd const& a, pdd const& b) {
|
||||
PDD x = a.root;
|
||||
|
|
@ -517,14 +527,14 @@ namespace dd {
|
|||
Compare leading terms of pdds
|
||||
*/
|
||||
bool pdd_manager::different_leading_term(pdd const& a, pdd const& b) {
|
||||
PDD x = a.root;
|
||||
PDD y = b.root;
|
||||
PDD x = first_leading(a.root);
|
||||
PDD y = first_leading(b.root);
|
||||
while (true) {
|
||||
if (x == y) return false;
|
||||
if (is_val(x) || is_val(y)) return true;
|
||||
if (level(x) == level(y)) {
|
||||
x = hi(x);
|
||||
y = hi(y);
|
||||
x = next_leading(x);
|
||||
y = next_leading(y);
|
||||
}
|
||||
else {
|
||||
return true;
|
||||
|
|
@ -532,6 +542,28 @@ namespace dd {
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* The assumption is that var(p) is part of the leading monomial.
|
||||
* Then the next leading monomial that uses var(p) has to be under hi(p)
|
||||
* because lo(p) does not use var(p).
|
||||
*/
|
||||
pdd_manager::PDD pdd_manager::next_leading(PDD p) const {
|
||||
SASSERT(!is_val(p));
|
||||
return first_leading(hi(p));
|
||||
}
|
||||
|
||||
/**
|
||||
* The first node that contains a term from the leading monomial
|
||||
* is a node of highest degree and highest variable.
|
||||
* Thus, when the degree of hi(p) + 1 is not dominated by degree of lo(p).
|
||||
*/
|
||||
pdd_manager::PDD pdd_manager::first_leading(PDD p) const {
|
||||
while (!is_val(p) && degree(hi(p)) + 1 < degree(lo(p))) {
|
||||
p = lo(p);
|
||||
}
|
||||
return p;
|
||||
}
|
||||
|
||||
/*
|
||||
Determine whether p is a linear polynomials.
|
||||
A linear polynomial is of the form x*v1 + y*v2 + .. + vn,
|
||||
|
|
@ -764,29 +796,44 @@ namespace dd {
|
|||
return sz;
|
||||
}
|
||||
|
||||
unsigned pdd_manager::degree(pdd const& b) {
|
||||
init_mark();
|
||||
void pdd_manager::init_dmark() {
|
||||
m_dmark.resize(m_nodes.size());
|
||||
m_degree.reserve(m_nodes.size());
|
||||
m_todo.push_back(b.root);
|
||||
++m_dmark_level;
|
||||
if (m_dmark_level == 0) {
|
||||
m_dmark.fill(0);
|
||||
++m_dmark_level;
|
||||
}
|
||||
}
|
||||
|
||||
unsigned pdd_manager::degree(pdd const& b) const {
|
||||
return degree(b.root);
|
||||
}
|
||||
|
||||
unsigned pdd_manager::degree(PDD p) const {
|
||||
if (is_dmarked(p)) {
|
||||
return m_degree[p];
|
||||
}
|
||||
m_todo.push_back(p);
|
||||
while (!m_todo.empty()) {
|
||||
PDD r = m_todo.back();
|
||||
if (is_marked(r)) {
|
||||
if (is_dmarked(r)) {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
else if (is_val(r)) {
|
||||
m_degree[r] = 0;
|
||||
set_mark(r);
|
||||
set_dmark(r);
|
||||
}
|
||||
else if (!is_marked(lo(r)) || !is_marked(hi(r))) {
|
||||
else if (!is_dmarked(lo(r)) || !is_dmarked(hi(r))) {
|
||||
m_todo.push_back(lo(r));
|
||||
m_todo.push_back(hi(r));
|
||||
}
|
||||
else {
|
||||
m_degree[r] = std::max(m_degree[lo(r)], m_degree[hi(r)]+1);
|
||||
set_mark(r);
|
||||
set_dmark(r);
|
||||
}
|
||||
}
|
||||
return m_degree[b.root];
|
||||
return m_degree[p];
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -833,7 +880,6 @@ namespace dd {
|
|||
return m_free_vars;
|
||||
}
|
||||
|
||||
|
||||
void pdd_manager::alloc_free_nodes(unsigned n) {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
m_free_nodes.push_back(m_nodes.size());
|
||||
|
|
@ -842,6 +888,7 @@ namespace dd {
|
|||
}
|
||||
std::sort(m_free_nodes.begin(), m_free_nodes.end());
|
||||
m_free_nodes.reverse();
|
||||
init_dmark();
|
||||
}
|
||||
|
||||
bool pdd_manager::is_reachable(PDD p) {
|
||||
|
|
@ -883,6 +930,7 @@ namespace dd {
|
|||
}
|
||||
|
||||
void pdd_manager::gc() {
|
||||
init_dmark();
|
||||
m_free_nodes.reset();
|
||||
SASSERT(well_formed());
|
||||
IF_VERBOSE(13, verbose_stream() << "(pdd :gc " << m_nodes.size() << ")\n";);
|
||||
|
|
|
|||
|
|
@ -213,7 +213,14 @@ namespace dd {
|
|||
inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
|
||||
|
||||
unsigned dag_size(pdd const& p);
|
||||
unsigned degree(pdd const& p);
|
||||
|
||||
mutable svector<unsigned> m_dmark;
|
||||
mutable unsigned m_dmark_level;
|
||||
void init_dmark();
|
||||
void set_dmark(unsigned i) const { m_dmark[i] = m_dmark_level; }
|
||||
bool is_dmarked(unsigned i) const { return m_dmark[i] == m_dmark_level; }
|
||||
unsigned degree(pdd const& p) const;
|
||||
unsigned degree(PDD p) const;
|
||||
|
||||
bool var_is_leaf(PDD p, unsigned v);
|
||||
|
||||
|
|
@ -228,6 +235,8 @@ namespace dd {
|
|||
rational m_pc, m_qc;
|
||||
pdd spoly(pdd const& a, pdd const& b, unsigned_vector const& p, unsigned_vector const& q, rational const& pc, rational const& qc);
|
||||
bool common_factors(pdd const& a, pdd const& b, unsigned_vector& p, unsigned_vector& q, rational& pc, rational& qc);
|
||||
PDD first_leading(PDD p) const;
|
||||
PDD next_leading(PDD p) const;
|
||||
|
||||
monomials_t to_monomials(pdd const& p);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue