Implement UF/DT theory restrictions

[Gbury]

This is still WIP, but contains quite a few changes:

• the typechecker and typing loop are adapted to reject declarations that do not respect the restrictions imposed by the (lack of) UF/DT theories
• some additions to error reporting which is missing a few cases (still in progress)
• the representation of smtlib logic is a bit more structured now, restrictions are transformed into a set of features represented as field of a record
• the parsing of smtlib logic is made a bit more strict by taking into account:
  • the order in which theories can appear in a logic name
  • the fact the a theory can not be repeated in a logic name

This last point probably some review/comment by @bobot , who should be more knowledgeable about whether it is correct/reasonable; the idea was to not allow to parse logic such as LIABVQF_ANIRA, which the current code happily parses, even though it's not really a valid theory declaration (it's incoherent with respect to arithmetic for instance).

[bobot]

Are you sure of the A for array just after QF_? Do you have a source? Otherwise refusing LIANIRA is good.

[Gbury]

Well, I mostly looked at all the logics listed on http://smtlib.cs.uiowa.edu/logics.shtml , which contains QF_ABV , QF_AUFBV, QF_ALIA and QF_AUFLIA, so it seems that the array theory can indeed occur after a QF_, or did I miss something ?

[bobot]

This list of logic is not exhaustive. However the code of CVC4 give you reason. There are some hacks to accept some commutation, we accept more of them.

EDIT: clarify

[Gbury]

Ok, so this should be fine to merge ?

[Gbury]

I'll merge, but don't hesitate to open issues if there are more logics that should be supported.