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

fix #1303

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-12 07:39:27 -07:00
parent c093e6d4b9
commit da2b876acb
2 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3536,10 +3536,11 @@ namespace polynomial {
iccp(p, max_var(p), i, c, pp); iccp(p, max_var(p), i, c, pp);
} }
void pp(polynomial const * p, var x, polynomial_ref & pp) { polynomial_ref pp(polynomial const * p, var x) {
scoped_numeral i(m_manager); scoped_numeral i(m_manager);
polynomial_ref c(pm()); polynomial_ref c(pm()), result(pm());
iccp(p, x, i, c, pp); iccp(p, x, i, c, result);
return result;
} }
bool is_primitive(polynomial const * p, var x) { bool is_primitive(polynomial const * p, var x) {
@ -3598,7 +3599,7 @@ namespace polynomial {
if (is_zero(rem)) { if (is_zero(rem)) {
TRACE("polynomial", tout << "rem is zero...\npp_v: " << pp_v << "\n";); TRACE("polynomial", tout << "rem is zero...\npp_v: " << pp_v << "\n";);
flip_sign_if_lm_neg(pp_v); flip_sign_if_lm_neg(pp_v);
pp(pp_v, x, r); r = pp(pp_v, x);
r = mul(d_a, d_r, r); r = mul(d_a, d_r, r);
return; return;
} }
@ -3849,7 +3850,7 @@ namespace polynomial {
TRACE("mgcd", tout << "new combined:\n" << C_star << "\n";); TRACE("mgcd", tout << "new combined:\n" << C_star << "\n";);
} }
} }
pp(C_star, x, candidate); candidate = pp(C_star, x);
TRACE("mgcd", tout << "candidate:\n" << candidate << "\n";); TRACE("mgcd", tout << "candidate:\n" << candidate << "\n";);
scoped_numeral lc_candidate(m()); scoped_numeral lc_candidate(m());
lc_candidate = univ_coeff(candidate, degree(candidate, x)); lc_candidate = univ_coeff(candidate, degree(candidate, x));
@ -6619,8 +6620,8 @@ namespace polynomial {
polynomial_ref cf1(pm()); m_wrapper.content(f1, x, cf1); polynomial_ref cf1(pm()); m_wrapper.content(f1, x, cf1);
polynomial_ref cf2(pm()); m_wrapper.content(f2, x, cf2); polynomial_ref cf2(pm()); m_wrapper.content(f2, x, cf2);
tout << "content(f1): " << cf1 << "\ncontent(f2): " << cf2 << "\n";); tout << "content(f1): " << cf1 << "\ncontent(f2): " << cf2 << "\n";);
pp(f1, x, f1); f1 = pp(f1, x);
pp(f2, x, f2); f2 = pp(f2, x);
TRACE("factor", tout << "f1: " << f1 << "\nf2: " << f2 << "\n";); TRACE("factor", tout << "f1: " << f1 << "\nf2: " << f2 << "\n";);
DEBUG_CODE({ DEBUG_CODE({
polynomial_ref f1f2(pm()); polynomial_ref f1f2(pm());
@ -7150,7 +7151,7 @@ namespace polynomial {
} }
void manager::primitive(polynomial const * p, var x, polynomial_ref & pp) { void manager::primitive(polynomial const * p, var x, polynomial_ref & pp) {
m_imp->pp(p, x, pp); pp = m_imp->pp(p, x);
} }
void manager::icpp(polynomial const * p, var x, numeral & i, polynomial_ref & c, polynomial_ref & pp) { void manager::icpp(polynomial const * p, var x, numeral & i, polynomial_ref & c, polynomial_ref & pp) {

2
src/test/nlsat.cpp
View file

@ -698,10 +698,8 @@ static void tst10() {
void tst_nlsat() { void tst_nlsat() {
tst10(); tst10();
std::cout << "------------------\n"; std::cout << "------------------\n";
exit(0);
tst9(); tst9();
std::cout << "------------------\n"; std::cout << "------------------\n";
exit(0);
tst8(); tst8();
std::cout << "------------------\n"; std::cout << "------------------\n";
tst7(); tst7();