mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

added notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-23 12:34:30 -08:00
parent 77868f3d96
commit beb4c0f27b
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -104,8 +104,8 @@ namespace dd {
Given two definition polynomials d1, d2, it must be the case that 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. 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. 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 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. 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). 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]; Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2];