From feff6a2addcb67437065d4a42255d941b1cd65c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Dec 2019 11:49:50 -0800 Subject: [PATCH] fix build, add ZDD reference Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.h | 3 +++ src/math/grobner/pdd_grobner.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) 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());