From beb4c0f27b2f6cadb54f2cbe5d6b1dec45b150cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Dec 2019 12:34:30 -0800 Subject: [PATCH] added notes Signed-off-by: Nikolaj Bjorner --- src/math/grobner/pdd_grobner.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index aee58abf8..3adc5555e 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -104,8 +104,8 @@ namespace dd { Given two definition polynomials d1, d2, it must be the case that level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing. Then starting from the lowest level examine pdd nodes. - The the current node be called p, check if the pdd node is used in an equation - w - r = 0, in which case, w inherits the labels from r. + Let the current node be called p, check if the pdd node p is used in an equation + w - r = 0. In which case, w inherits the labels from r. Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p). Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2];