SMT-LIB: print symbols with |

[hansjoergschurr]

This is a feature request.
It would be nice if dolmen could print extended symbols with the | quotes in error messages.
For example:

File "foo.smt2", line 1056, character 64-96:
Error The term: (q(10) * 203.0) has type real but was expected to be of type
      int

Here q(10) is a symbol that must be written as |q(10)| in the input. While here this only leads to a second of confusion, in other cases it might lead to actual problems. For example, if the symbols is |(q 10)|, which would also be a valid SMT-LIB term.

[Gbury]

Indeed, I'll try and see if there is an easily reasonable way to do that.

[Gbury]

So, this issue will be fixed, but it will take a bit of time. Basically my roadmap currently is: finish higher-order for Dolmen (soon !), then get on with writing the export API (i.e. the capability to print terms in a given language), and once that's done, error messages will use that API to print terms in the input language syntax (and respect conventions for escaping, etc..), which will solve this problem.

[hansjoergschurr]

Sounds like a good plan