Fixing translation of polymorphic constants to Z3

[ibnyusuf]

#300 fixed the translation of polymorphic terms with arity > 0. However, we treat constants differently and they were not being translated correctly. This PR should ensure that they are now translated correctly to Z3.

[MichaelRawson]

The code seems fine, but I don't understand the fix.

fixed the translation of polymorphic terms with arity > 0

Shouldn't polymorphic terms be of arity > 0 by definition? They need a sort variable to be polymorphic.

From #453

If I understand correctly, #300 was a fix for theory instantiation where we know that we are only passing ground things to Z3. Hence, we can safely treat function symbols as indexed families.

When it comes to AVATAR, we pass non-ground things as well and this is where the issue arises.

AVATAR should only pass ground things to Z3. If not (and apparently it doesn't), we need some logic to do the grounding to something reasonable. To start with I'd suggest a new uninterpreted sort and a new uninterpreted constant of that sort, although it's possible that we could do better. Then, the logic in #300 should produce a family of functions for each polymorphic function on-demand.

What am I missing?

[ibnyusuf]

Please ignore the comment about non-ground and AVATAR. That was just a silly misunderstanding. I believe we only pass ground things to Z3 in AVATAR.

Indeed, polymorphic terms do have arity > 0. In an old version of this code, we treated something as a constant if numTermArgs > 0. However, that was fixed in master. I carried out my "fix" for the same issue on a branch that didn't contain this fix and then ported it onto master without noticing the different condition.

I have now investigated the root cause of #300 more deeply and it is being cause by unification with abstraction code creating constraints between sorts incorrectly. As the whole UWA mechanism is set to change, I don't propose a fix now, but will leave the bug report open so that it can be revited once the new UWA implementation goes in. I'm closing this PR now.

[MichaelRawson]

OK, thanks anyway @ibnyusuf - sounds like we got somewhere. :-)