Last `set-logic` "wins" about dolmen HOT 6 CLOSED

All done (in #80 for the reset behavior, and) in #82, which adds a warning. On your example, dolmen now prints:

File "/home/guigui/tmp/tmp.smt2", line 2, character 0-18:
Warning Logic was already set at line 1, character 0-22

from dolmen.

Indeed, multiple set-logic should at the very least warn, if not error; I'll correct that asap.

from dolmen.

A quick remark: Section 4.2.1 of the SMT-LIB standard hints that multiple set-logic commands are allowed and that indeed the last one is the one that is used.
There is one weird effect though: "The effect of the command is to add globally (and permanently) a declaration of
each sort and function symbol in the logic." hence in the second case here the bitvector functions should still be around?

from dolmen.

Oh... I'll have to read it, but it seems particularly annoying to implement, particularly when considering that a logic is not simply a set of theories, but also extensions and restrictions. Would the restrictions be cumulative ?

from dolmen.

This is not how I understood it, but I just quickly looked this up

from dolmen.

Okay, so there are basically two parts of the language specification that relates to set-logic:

page 55:

current signature: the signature determined by the logic specified with the most recent set-logic command and by the set of sort symbols and rank associations (for function symbols) in the current context.

page 60:

(set-logic l) tells the solver what logic, in the sense of Section 5.5, is being used. The argument l can be the name of a logic in the SMT-LIB catalog or of some other solver-specific logic. The effect of the command is to add globally (and permanently) a declaration of each sort and function symbol in the logic. The argument l can also be the predefined symbol ALL. With this argument, the solver sets the logic to the most general logic it supports.(35) Note that while the reaction to (set-logic ALL) is the same for every compliant solver, the chosen logic is solverspecific. We refer to the logic set by the most recent set-logic command as the current logic.

From what I understand, this means that the last set-logic should be used to determine the logic to use when typing an assertion. The part about adding symbols globally is, to my understanding, more about what happens with respect to the (reset-assertions) command as described:

(reset-assertions) removes from the assertion stack all assertion levels beyond the first one. In addition, it removes all assertions from the first assertion level. Declarations and definitions resulting from the set-logic command are unaffected (because they are global)

So, I think that dolmen's behavior is currently not wrong, however a few things could be made better:

• a warning when using multiple set-logic in the same file, or more precisely when a set-logic command overwrites a previous one (so set-logic commands separated by a reset should be okay (which reminds me that I don't think dolmen correctly handles the reset command, which i'll try to fix)).
• should that warning be fatal in strict mode ?
• are there realistic cases where one would want to use and/or need multiple logics in a single file (without any reset) ?

from dolmen.