mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 05:09:02 +00:00
Code Activity

Update polynomial.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-15 09:38:17 -07:00
parent f4a87d4f61
commit 7efcda2674
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polynomial/polynomial.cpp
View file

@ -2334,7 +2334,8 @@ namespace polynomial {
// Buffer for multiplying large polynomials. // Buffer for multiplying large polynomials.
// It delays internalizing monomials, and uses sorted vectors instead of hash tables. // It delays internalizing monomials, and uses sorted vectors instead of hash tables.
// this implementation is 10x slower on results up to 10K monomials // this implementation is 10x slower on results up to 10K monomials
// it also has a bug as entries are not properly sorted. // it also has a bug as entries are not properly sorted and therefore
// the same monomial can appear several times.
// perf tuning and debugging is required if this is to be used. // perf tuning and debugging is required if this is to be used.
// it is possible this can be faster for very large polynomials by ensuring cache locality. // it is possible this can be faster for very large polynomials by ensuring cache locality.
// at this point there are several cache misses: such as m_powers are pointers inside of m_monomial. // at this point there are several cache misses: such as m_powers are pointers inside of m_monomial.