Currently in SMT-LIB2, logic names (e.g. AUFLIRA) are (somewhat) formed from concatenating the names of theories (e.g. UF, A, LIRA).
As far as I've seen, all logics officially mentioned on the SMT-LIB website and specification adhere to a somewhat strict order or the theory names when concatenating them: for instance, the UFLIA logics exists but I've never seen the LIAUF logic.
Correspondingly, Dolmen currently expects a certain order for the theory names when parsing a logic, the code used for that can be found here, with some comments there. Among other things, in that order BF comes before FP, however, some users have raised an issue where they have problems that use the logic QF_FPBV (cf Gbury/dolmen#227 )
While it's not a problem for Dolmen to accept such a logic, I cas wondering what is the official stance w.r.t. logics names and theory orders within them ? Since it's a problem that will disappear in SMT-LIB3, I understand it's not a big (or pressing) issue, but it would be nice to have an official position on that question (even if it's : accept any logic name that is used and looks reasonable).
Currently in SMT-LIB2, logic names (e.g.
AUFLIRA) are (somewhat) formed from concatenating the names of theories (e.g.UF,A,LIRA).As far as I've seen, all logics officially mentioned on the SMT-LIB website and specification adhere to a somewhat strict order or the theory names when concatenating them: for instance, the
UFLIAlogics exists but I've never seen theLIAUFlogic.Correspondingly, Dolmen currently expects a certain order for the theory names when parsing a logic, the code used for that can be found here, with some comments there. Among other things, in that order
BFcomes beforeFP, however, some users have raised an issue where they have problems that use the logicQF_FPBV(cf Gbury/dolmen#227 )While it's not a problem for Dolmen to accept such a logic, I cas wondering what is the official stance w.r.t. logics names and theory orders within them ? Since it's a problem that will disappear in SMT-LIB3, I understand it's not a big (or pressing) issue, but it would be nice to have an official position on that question (even if it's : accept any logic name that is used and looks reasonable).