Refactoring signature

[mezpusz]

Shell::Signature is painful and error-prone to use, make it better. We could do the following things to make it better:

• Remove setType and pass OperatorType directly when creating a symbol. This removes the need for the weird fnType, predType, typeConType triplet. Currently being implemented in require-symbol-operatortype.
• Have a unified domain for all symbol types. This should be straightforward to do, we just have some edge cases where we have to enumerate functions/predicates/typecons, so we have to additionally maintain some structures storing these. The benefit of this is that a tremendous amount of branching can be removed from the code, having getSymbol instead of getFunction, getPredicate and getTypeCon, and of course, that debugging becomes much easier because symbols map one-to-one to unsigneds, so no more "not sure what this symbol is".
• Have some kind of nicer, builder interface for all the makeIntroduced, makeSkolem, etc. and maybe also for getting the functor itself, so the addFunction and immediate getFunction patterns could disappear. (suggested by @MichaelRawson)

[shalashaska117]

Can I solve this one?

[mezpusz]

Yes, feel free to do so, just note that I have an almost working first item on require-symbol-operatortype. The following still doesn't work:

./vampire --ignore_missing warn --decode fmb+10_1_si=on:fmbes=contour:fmbswr=3:random_seed=12345:fmbsr=1.29942:i=5000:nm=0:rtra=on_0 $TPTP/Problems/GRP/GRP655+1.p
...
Condition n < _size at location /Users/mezpusz/vampire/Lib/DArray.hpp:100 was violated, as:
n == 0
_size == 0

Probably the changes in FMB/SortInference.cpp are wrong.

[quickbeam123]

I would prefer if someone with a longer experience with the codebase orchestrates this. I asked Michael to look into this...

[MichaelRawson]

One way we could do this if you're keen @shalashaska117 is that I work out what the new interface should be and you help me adapt the existing code.

[mezpusz]

@MichaelRawson @quickbeam123 feel free to add more items, or elaborate on them, I just added what was on the top of my mind.

[shalashaska117]

One way we could do this if you're keen @shalashaska117 is that I work out what the new interface should be and you help me adapt the existing code.

For me it's ok, let me know what I have to do