mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Add support for prem_gcd in square_free

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-12 19:49:50 -08:00
parent 551d0b7de0
commit 2b5883454c
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/realclosure/realclosure.cpp
View file

@ -3475,12 +3475,17 @@ namespace realclosure {
value_ref_buffer p_prime(*this); value_ref_buffer p_prime(*this);
value_ref_buffer g(*this); value_ref_buffer g(*this);
derivative(sz, p, p_prime); derivative(sz, p, p_prime);
gcd(sz, p, p_prime.size(), p_prime.c_ptr(), g); if (m_use_prem)
prem_gcd(sz, p, p_prime.size(), p_prime.c_ptr(), g);
else
gcd(sz, p, p_prime.size(), p_prime.c_ptr(), g);
if (g.size() <= 1) { if (g.size() <= 1) {
r.append(sz, p); r.append(sz, p);
} }
else { else {
div(sz, p, g.size(), g.c_ptr(), r); div(sz, p, g.size(), g.c_ptr(), r);
if (m_use_prem)
normalize_int_coeffs(r);
} }
} }
} }