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

have the TermList default constructor zero-initialise #541

Merged
merged 3 commits into from Apr 8, 2024

Conversation

MichaelRawson
Copy link
Contributor

Somewhat trivial, but in discussion with @quickbeam123 have TermList zero-initialise its content. In (almost?) all cases this should be immediately overwritten, but it means that when there is a bug, we will get a hard null-dereference crash rather than...something else.

@joe-hauns
Copy link
Contributor

Could we indstead of zero-initializing it initializing it in such a way that Term::isEmpty returns true?

@easychair
Copy link
Contributor

easychair commented Mar 28, 2024 via email

@MichaelRawson
Copy link
Contributor Author

@joe-hauns - I had the same idea, but it seemed to me that an empty TermList should be a zero-initialised TermList. This doesn't work for some reason and crashes a lot - so I should figure out why, if two people want this.

@easychair - this is a good point. In principle it should not break term sharing, because we should never insert a Term containing an empty TermList into term sharing. But it would be smart to have some checks for this.

Either way - on hold for now until I look into it more, probably next week at this point.

@easychair
Copy link
Contributor

easychair commented Mar 28, 2024 via email

@MichaelRawson
Copy link
Contributor Author

Could we indstead of zero-initializing it initializing it in such a way that Term::isEmpty returns true?

Done. :-) I've also added an assertion to TermSharing to make sure we don't inadvertently break that.

I did briefly try to have two categories of "empty" TermLists: the current one and a zero TermList, but Vampire uses both "invalid TermList" and "off the end of an argument list" somewhat blurrily so that wasn't workable.

@MichaelRawson
Copy link
Contributor Author

See #384 - we no longer have "very special" variables, so SPEC_UPPER_BOUND is pointless. Also remove this here as I'm passing. Checking whether something is a special variable should now be very slightly faster.

@quickbeam123
Copy link
Collaborator

It's probably the SPEC_UPPER_BOUND test gone, which have us 3 ott problems and 5 discount10 TPTP problems solved extra with this, under -i 10000.

@quickbeam123 quickbeam123 merged commit 5a168f8 into master Apr 8, 2024
1 check passed
@quickbeam123 quickbeam123 deleted the michael-term-default branch April 8, 2024 15:35
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.

None yet

4 participants