diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 3ac44d974..0fd9606bb 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -9,6 +9,9 @@ Abstract: Poly DD package + It is a mild variant of ZDDs. + In PDDs arithmetic is either standard or using mod 2 (over GF2). + Non-leaf nodes are of the form x*hi + lo where - maxdegree(x, lo) = 0, diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index a0fa7edd4..9edc4aac9 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -425,7 +425,7 @@ namespace dd { // they watch the top most variable in poly i = 0; for (auto const& w : m_watch) { - for (equation const* e : w) { + for (equation* e : w) { VERIFY(!e->poly().is_val()); VERIFY(e->poly().var() == i); VERIFY(!e->is_processed());