Code tree search structs refactor + lazily expanded flat terms

mezpusz commented 5 months ago

Two main changes in this pull request:

CodeTree::SearchStruct is refactored avoiding duplication of subclasses. Raw array containing value-target pairs is replaced with STL containers for better and easier handling.
Added new tag FUN_UNEXPANDED to FlatTerm in which case only the tag, term pointer and number of subentries is filled out first. A call on FlatTerm::Entry::expand fills out the same entries for the arguments. The point is that we expand tha flat term lazily which in some cases would be a bottleneck when the FlatTerm is not even used.

Additionally, added some basic printing for code trees.

MichaelRawson commented 5 months ago

Thanks for the fixes/improvements, @mezpusz! I'm happy apart from the GET_CONTAINING_OBJECT macro when you want to take a look, @quickbeam123.

quickbeam123 commented 5 months ago

No new assertion violations and slightly improves performance. I think it's ready to go!

MichaelRawson commented 5 months ago

OK! I'll wait to see how/if @mezpusz wants to fix GET_CONTAINING_OBJECT and then we can merge, I think.

vprover / vampire