Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

createpoint is slow #894

Closed
kortenkamp opened this issue Nov 2, 2022 · 0 comments · Fixed by #895
Closed

createpoint is slow #894

kortenkamp opened this issue Nov 2, 2022 · 0 comments · Fixed by #895
Assignees
@kortenkamp

Comments

@kortenkamp
Copy link
Member

An old oral comment of @montaga about https://cinderella.de/files/ml215/stellenwerttafel.html was that moving a point from the "Einer" to the "Tausendstel" is very slow. The root cause of this is that 999 elements are being created. However, adding elements seems to be $O(n)$ instead of $O(1)$ for points, which leads to quadratic runtime in the number of elements being added.

It is important to check whether the prover is needed at all when adding an element. It is not if adding a free point from a script. In Cindy Classic it is necessary to use the prover on all elements that have been added by the user, so we have to take care to use the right semantics when we will create "Cindy in Cindy", but that is not the case yet.
@kortenkamp kortenkamp self-assigned this Nov 2, 2022
@kortenkamp kortenkamp mentioned this issue Nov 2, 2022
Merged
kortenkamp added a commit that referenced this issue Nov 2, 2022
@kortenkamp
Merge pull request #895 from CindyJS/kortenkamp/fastInsertElements
412441a 
adding free points from CindyScript does not invoke the prover

When adding elements using the createpoint(…) function, the prover does not need to be invoked. However, it was, leading to a quadratic runtime when adding n points. I tried to fix this by invoking addElementNoProof instead of addElement, but this still had quadratic runtime as the conjectures comparing the new element to all other elements are created in the addElementNoProof code.

This pull request changes the behaviour of addElementNoProof to match its name – conjectures are only created when the prover is invoked, and also uses addElementNoProof for the createpoint(…) function.

An example illustrating the now instant creation of 999 elements has been added as well, the Stellenwerttafel. Add a point in the first column and then drag it to the rightmost column to create 999 elements. This took about 5-15 seconds, depending on the computer/tablet you used, and is now immediate.

This closes #894.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kortenkamp kortenkamp

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

adding free points from CindyScript does not invoke the prover CindyJS/CindyJS
1 participant
@kortenkamp