QEPCAD Timeout

[anirjoshi]

Steps To Reproduce

1. My machine is Mac M2 with the OS Ventura 13.4
2. I already have installed sage with version 10.3 [I believe the same issue exists with 10.4 as well] The following program times-out:

var('x')
var('a')
var('y')
var('b')
var('r')

qf = qepcad_formula
F0 = (0 > 0 + 1*x*x*a*a + 1*y*y*b*b + -1*a*a*b*b)
F1 = (0 > 0 + 1*x*x + 1*y*y + -20*x + -20*y + -1*r*r + 200)
F2 = qf.and_(F0,F1)
F3 = qf.and_(F2)
var("tmp")
eliminate_trick = qepcad(qf.exists(tmp,qf.and_(tmp==0,F3)),memcells='1000000000 +L5000')
print(eliminate_trick)

Quantification out of the tmp variable should be pretty easy since this only appears in the constraint tmp==0.

Expected Behavior

A formula without the tmp variable.

Actual Behavior

Just keeps running for a long time.

Additional Information

No response

Environment

• OS: Mac M2 with the OS Ventura 13.4
• Sage Version: 10.3

Checklist

• [X] I have searched the existing issues for a bug report that matches the one I want to file, without success.
• [X] I have read the documentation and troubleshoot guide

[maxale]

I this issue is irrelevant to Sage, it should be reported to Qepcad developers.

[anirjoshi]

@maxale , Thank you for the quick response. Since I used Sage software, therefore I thought this is the correct place to report the issue. It would be great if you/someone can point me to the Qepcad developers?

[maxale]

@anirjoshi: No, it's not a right place as Sage is not responsible for issues in other packages, which it uses as blackboxes. For Qepcad issues, please check its homepage: https://www.usna.edu/CS/qepcadweb/B/QEPCAD.html

[dimpase]

I don't understand the computation

sage: qf.exists(tmp,qf.and_(tmp==0,F3))
(E tmp)[tmp = 0 /\ [[0 > -a^2 b^2 + a^2 x^2 + b^2 y^2 /\ 0 > -r^2 + x^2 + y^2 - 20 x - 20 y + 200]]]
sage: qepcad(qf.exists(tmp,qf.and_(tmp==0,F3)),memcells='1000000000 +L5000')
finish  &

The last line is the output I get on my Linux machine. What is it supposed to do?

[dimpase]

@anirjoshi: No, it's not a right place as Sage is not responsible for issues in other packages, which it uses as blackboxes. For Qepcad issues, please check its homepage: https://www.usna.edu/CS/qepcadweb/B/QEPCAD.html

Probably a better place to report QEPCAD issues is https://github.com/chriswestbrown/qepcad

Although they seem to be putting all the work into a successor project, https://github.com/chriswestbrown/tarski

[dimpase]

Anyhow, running

sage: eliminate_trick = qepcad(qf.exists(tmp,qf.and_(tmp==0,F3)),memcells='1000000000 +L5000')
....: print(eliminate_trick)

just prints an empty line on my Linux laptop.

[anirjoshi]

@dimpase Thank you for the pointer to the appropriate QEPCAD repo.

The output is supposed to simply be the formula in the square brackets after tmp==0. That is, the output is supposed to be [0 > -a^2 b^2 + a^2 x^2 + b^2 y^2 /\ 0 > -r^2 + x^2 + y^2 - 20 x - 20 y + 200]. This is so because there is no tmp variable in this formula. So tmp==0 is the only place where tmp variable occurs. Just taking a conjunction of tmp==0 with another formula where tmp does not occur, and then existentially quantifying out tmp variable should return the other formula, which is [0 > -a^2 b^2 + a^2 x^2 + b^2 y^2 /\ 0 > -r^2 + x^2 + y^2 - 20 x - 20 y + 200] in this case.

[dimpase]

Does this work on small examples?