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.

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

Change hashes in Induction so that iteration orders are deterministic #496

Merged
merged 1 commit into from
Oct 26, 2023

Conversation

mezpusz
Copy link
Contributor

@mezpusz mezpusz commented Oct 26, 2023

Tested with portfolio mode and Discount over UFDTLIA benchmarks (only structural induction, integer induction uses the same structures apart from the induction term set). Diff shows no change in the proofs over multiple runs, and there is no major diff compared to master.

@quickbeam123
Copy link
Collaborator

Could you please remind me why storing TermList instead of Term*should already liberate you from hashing on pointers? I think TermList hashes on content which boils down to the pointer+tag for wrapped Term*.

Other than that, could please rename TermHash to SharedTermHash?

@mezpusz
Copy link
Contributor Author

mezpusz commented Oct 26, 2023

My bad, I remembered that TermList is properly hashed (wrong) but did not check where content was coming from. I'll change it back and add the same hash function.

@mezpusz mezpusz force-pushed the make-induction-deterministic branch from 979e1aa to d0dc35d Compare October 26, 2023 16:54
@quickbeam123
Copy link
Collaborator

Cool!

@quickbeam123 quickbeam123 merged commit 050f606 into master Oct 26, 2023
1 check passed
@quickbeam123 quickbeam123 deleted the make-induction-deterministic branch October 26, 2023 17:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants