support (grounded) polymorphic functions for Z3

[MichaelRawson]

This allows Vampire's Z3 translation to reason about fully-applied polymorphic functions by encoding them into a family of monomorphic functions. For example, if we have f: !>[A: $tType]: A > A and we create the terms f($int, 1) and f($real, 2.0) then Z3 cannot deal with f natively, but it is quite capable of reasoning about f$int(1) and f$real(2.0) where f$int: $int > $int and f$real: $real > $real.

Mostly I think the changes to achieve this are natural. There are two non-obvious points:

• Introduce a new BottomUpChildIter type, SortlessTermList: when building up such terms for Z3, we don't want to include sort terms in arguments as we'd get e.g. f$int($int, 1). This seems like the cleanest way of doing it.
• The Z3 interface has a type called FuncOrPredId, which is what it sounds like. I add a (nullable) Term * to this structure, which is merely a Vampire term including the sort arguments that we need to distinguish e.g. f$int from f$real, such as f($int, 1). We can supply this term when we need to construct such a term! I admit this is a bit weird, but it avoids an allocation and changes the least code.

Z3 seems quite happy with ad-hoc polymorphism, so I don't actually bother changing the name of the function. It will then have two separate functions called f with different types. Everyone OK with this?

This now proves the problem @ibnyusuf provided called prob_07476_368335__18231272_1.p relatively easily with only -sas z3. Naturally we should test thoroughly to make sure we're not accidentally unsound/out-of-spec.

[joe-hauns]

Looks all nice and tidy! Just one minor comment/question concerning operator==.

[ibnyusuf]

If forSorts is always set, it should be possible to remove this check since in the case where numTypeArguments() == 0 the for loop below will never be entered.

[ibnyusuf]

Another option, would be to always set forSorts in both the mono and the poly case. This would lead to some minor code simplifications below.

[MichaelRawson]

Sadly there are some places where we don't (?) have access to a concrete term. I guess in principle we could create a "dummy" term or review all of these places if you are very keen?

[ibnyusuf]

Sorry, I don't follow what you mean by "concrete term". We are passing a term into the constructor, can we not just use that?

[MichaelRawson]

The term is defaulted to nullptr in the first constructor (i.e. not this one) because at the various call sites we may have access to a symbol, but not a term using that symbol. So forSorts might be null later regardless of what we do here - but you're right, for this particular bit of code we can just use the term.

[ibnyusuf]

If we always set forSorts this check becomes redundant

[ibnyusuf]

I have tested this PR on a random sample of 98 TF1 problems coming from Petar's Sledgehammer benchmark set and there were no issues.

[MichaelRawson]

OK, so there was a bug. The problem was that if you had a 'phantom' type variable (I think I am using this word correctly, @ibnyusuf ?) we could end up having merging symbols that should be distinct in Z3.

For example, consider the propositional problem

p | q
~p | q
p | ~q
~p | ~q

Unsatisfiable, right? Now let's sprinkle some types all over it:

p: !>[A: $tType]: $o
q: $o
a: $tType

p(a) | q
~p(a) | q
p(a) | ~q
~p(a) | ~q

A little weird, but still unsat. But now if we introduce another type:

p: !>[A: $tType]: $o
q: $o
a: $tType
b: $tType

p(a) | q
~p(a) | q
p(a) | ~q
~p(b) | ~q

this should be satisfiable because the last clause doesn't forbid p(a), q, (and normal Vampire is OK with this) but -sas z3 says unsatisfiable because it doesn't distinguish between two p functions with the same type after substitution.

I've fixed this for now by adding a tag for each instantiated type variable to the Z3 name. I'm not sure this is the best solution, but I'm reasonably confident it's correct. Z3 does deal with compound symbol names correctly, e.g. p(f(a)).

[quickbeam123]

Well discovered, @MichaelRawson ! (Already running new performance check.)

As a side note: Since you are now adding these tags, isn't the comment

// Z3 seems OK with having overloaded functions

superfluous / incorrect?

[MichaelRawson]

isn't the comment superfluous / incorrect?

Correct! Removed.