adding free points from CindyScript does not invoke the prover #895
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 invokingaddElementNoProof
instead ofaddElement
, but this still had quadratic runtime as the conjectures comparing the new element to all other elements are created in theaddElementNoProof
code.This pull request changes the behaviour of
addElementNoProof
to match its name – conjectures are only created when the prover is invoked, and also usesaddElementNoProof
for thecreatepoint(…)
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.