Properly parse qualified identifiers

[ajreynol]

This refactors the smt2 parser so that it properly parses qualified identifiers (the generic form of function application heads in smt2). This required refactoring of the termNonVariable grammar in Smt2.g.

Specifically:

• This PR merges the cases of termNonVariable of (1) a type-ascripted term with head as, (2) function variables applied to argument list (3) indexed functions applied to argument list, and (4) array constants, which can be seen as (as const (Array T1 T2)) applied to an argument.
  These are now all cases of a qualified identifier (qualIdentifier) applied to argument list, which follows terms in section 3.6 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf.
• Merges indexed function names and symbols into a identifier, following the definition of identifier in section 3.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf.
• A few checks had to be rearranged to preserve the old behavior, including moving the hack for unary minus in sygus version 1.0.

This fixes #2832.

[mpreiner]

LGTM, one minor suggestion.

[4tXJ7f]

I didn't have time to look at this in detail yet. One high-level comment that I have: We have decided to move logic out of the parser files as much as possible (to make it easier to move away from ANTLR3) but this PR adds quite a bit of logic in the parser file itself. Is there any chance that we could move this code to the parser class?

[ajreynol]

I agree we should move code to the parser files. This PR actually doesn't add much code, it just rearranges it. Perhaps we should do this on a followup PR?

[mpreiner]

Yes, I think it's a good idea to move the logic to the parser files in a follow-up PR.

[ajreynol]

Ready to merge?

[mpreiner]

I think we should still wait to get a second review for that. @4tXJ7f do you have any time soon to do a quick review?

[4tXJ7f]

I'll try to do it tomorrow evening (Thursday).