It should not be too hard to add support for theory and logic definitions. Two options: 1) add callbacks for "fake" commands: `(theory ..)` and `(logic ..)` 2) modify the Pomelo parser to be multimodal. ~~This can be done by accepting a first token `Mode(m)` that sets the mode.~~ (EDIT: not needed) https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
It should not be too hard to add support for theory and logic definitions.
Two options:
(theory ..)and(logic ..)This can be done by accepting a first token(EDIT: not needed)Mode(m)that sets the mode.https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf