-
Notifications
You must be signed in to change notification settings - Fork 102
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.
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
Prover functions for small arith. #2608
base: main
Are you sure you want to change the base?
Conversation
int_to_limbs(quotient) + int_to_limbs(remainder) | ||
} | ||
} | ||
); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have reviewed the mathematics behind all the computation and after a first look, it seems to makes sense (it is even clearer than before). What I don't quite understand is the use of the query function. I understand that the results are assigned in y3 + x1, but when is it “called” for that to happen? Is it related to the div operation defined above, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the runtime solver, (all) query functions are executed when there is no more progress, I think. It works because eval
silently fails if the value is not there yet. If all eval
calls succeed, then the computed value is assigned to the target columns.
Co-authored-by: Georg Wiese <[email protected]>
…-labs/powdr into use_queue_for_identity_queue
…to enable_permutations
…to enable_permutations
No description provided.