search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

remove `splPrefix`, not necessary #572

Closed MichaelRawson closed 2 months ago

MichaelRawson commented 2 months ago

There's a static splPrefix floating around in Splitter, which is mirrored as splitPrefix in InferenceStore. It doesn't seem to do much and does not conform with the convention.

Just compute this thing on-demand and conform to the convention.

quickbeam123 commented 2 months ago

I like the initiative, but can't this lead to a name clash?

MichaelRawson commented 2 months ago

It's "namespaced" by putting _split on the end. So unless we have other names of the form spN_split, no.

quickbeam123 commented 2 months ago

Is there are chance these names could mix with any other term material? I am thinking of the evil user coming with a TPTP problem with a predicate sp5_split (perhaps by coincidence) in the signature.

MichaelRawson commented 2 months ago

You are quite right - I thought it was just "already broken" and this wouldn't fix it (but would be considerably shorter) but I think addFreshFunction does some linear search, which surprised me.

Let's close this and I'll keep this corner in mind when I get to look at some of my other gripes with Signature.