Skip to content

Commit 77cfa98

Browse files
sage: Normalize sign of polynomial factors in prover
The prover, when run on recent sage versions, failed to prove some of its goals due to a change in sage. This commit adapts our code accordingly. The prover passes again after this commit.
1 parent eae7586 commit 77cfa98

File tree

1 file changed

+34
-10
lines changed

1 file changed

+34
-10
lines changed

sage/group_prover.sage

+34-10
Original file line numberDiff line numberDiff line change
@@ -177,6 +177,30 @@ class constraints:
177177
def __repr__(self):
178178
return "%s" % self
179179

180+
def normalize_factor(p):
181+
"""Normalizes the sign of primitive polynomials (as returned by factor())
182+
183+
This function ensures that the polynomial has a positive leading coefficient.
184+
185+
This is necessary because recent sage versions (starting with v9.3 or v9.4,
186+
we don't know) are inconsistent about the placement of the minus sign in
187+
polynomial factorizations:
188+
```
189+
sage: R.<ax,bx,ay,by,Az,Bz,Ai,Bi> = PolynomialRing(QQ,8,order='invlex')
190+
sage: R((-2 * (bx - ax)) ^ 1).factor()
191+
(-2) * (bx - ax)
192+
sage: R((-2 * (bx - ax)) ^ 2).factor()
193+
(4) * (-bx + ax)^2
194+
sage: R((-2 * (bx - ax)) ^ 3).factor()
195+
(8) * (-bx + ax)^3
196+
```
197+
"""
198+
# Assert p is not 0 and that its non-zero coeffients are coprime.
199+
# (We could just work with the primitive part p/p.content() but we want to be
200+
# aware if factor() does not return a primitive part in future sage versions.)
201+
assert p.content() == 1
202+
# Ensure that the first non-zero coefficient is positive.
203+
return p if p.lc() > 0 else -p
180204

181205
def conflicts(R, con):
182206
"""Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
@@ -204,10 +228,10 @@ def get_nonzero_set(R, assume):
204228
nonzero = set()
205229
for nz in map(numerator, assume.nonzero):
206230
for (f,n) in nz.factor():
207-
nonzero.add(f)
231+
nonzero.add(normalize_factor(f))
208232
rnz = zero.reduce(nz)
209233
for (f,n) in rnz.factor():
210-
nonzero.add(f)
234+
nonzero.add(normalize_factor(f))
211235
return nonzero
212236

213237

@@ -222,27 +246,27 @@ def prove_nonzero(R, exprs, assume):
222246
return (False, [exprs[expr]])
223247
allexprs = reduce(lambda a,b: numerator(a)*numerator(b), exprs, 1)
224248
for (f, n) in allexprs.factor():
225-
if f not in nonzero:
249+
if normalize_factor(f) not in nonzero:
226250
ok = False
227251
if ok:
228252
return (True, None)
229253
ok = True
230254
for (f, n) in zero.reduce(allexprs).factor():
231-
if f not in nonzero:
255+
if normalize_factor(f) not in nonzero:
232256
ok = False
233257
if ok:
234258
return (True, None)
235259
ok = True
236260
for expr in exprs:
237261
for (f,n) in numerator(expr).factor():
238-
if f not in nonzero:
262+
if normalize_factor(f) not in nonzero:
239263
ok = False
240264
if ok:
241265
return (True, None)
242266
ok = True
243267
for expr in exprs:
244268
for (f,n) in zero.reduce(numerator(expr)).factor():
245-
if f not in nonzero:
269+
if normalize_factor(f) not in nonzero:
246270
expl.add(exprs[expr])
247271
if expl:
248272
return (False, list(expl))
@@ -279,17 +303,17 @@ def describe_extra(R, assume, assumeExtra):
279303
if base not in zero:
280304
add = []
281305
for (f, n) in numerator(base).factor():
282-
if f not in nonzero:
283-
add += ["%s" % f]
306+
if normalize_factor(f) not in nonzero:
307+
add += ["%s" % normalize_factor(f)]
284308
if add:
285309
ret.add((" * ".join(add)) + " = 0 [%s]" % assumeExtra.zero[base])
286310
# Iterate over the extra nonzero expressions
287311
for nz in assumeExtra.nonzero:
288312
nzr = zeroextra.reduce(numerator(nz))
289313
if nzr not in zeroextra:
290314
for (f,n) in nzr.factor():
291-
if zeroextra.reduce(f) not in nonzero:
292-
ret.add("%s != 0" % zeroextra.reduce(f))
315+
if normalize_factor(zeroextra.reduce(f)) not in nonzero:
316+
ret.add("%s != 0" % normalize_factor(zeroextra.reduce(f)))
293317
return ", ".join(x for x in ret)
294318

295319

0 commit comments

Comments
 (0)