feat: Echo command

[Stevendeo]

Adds the echo command to alt-ergo

[bclement-ocp]

Can you add a test that we do the right thing with escaped quote?

AFAICT, (echo "a""b") should print "a""b", not sure if Dolmen replaces the inner "" with a single " or not.

[Stevendeo]

AFAICT, (echo "a""b") should print "a""b", not sure if Dolmen replaces the inner "" with a single " or not.

It does not actually; isn't it a Dolmen issue?

[Stevendeo]

It does not* print "a""b", but "a"b"

[bclement-ocp]

AFAICT, (echo "a""b") should print "a""b", not sure if Dolmen replaces the inner "" with a single " or not.

It does not actually; isn't it a Dolmen issue?

It is not a Dolmen issue — the semantics of "a""b" is indeed the string a"b (e.g. it's length must be 3, not 4), it just so happens that echo specifically requires printing the string literal in escaped form, and so we need to re-escape it.

[Gbury]

See page 23 of the smtlib spec : https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

String literals. A (literal) is any sequence of characters from <printable_char> or
<white_space_char> delimited by the double quote character " (34dec). The character "
can itself occur within a string literal only if duplicated. In other words, after an initial "
that starts a literal, a lexer should treat the sequence "" as an escape sequence denoting
a single occurrence of " within the literal.