Z3: Can't read multiline output

[loewenheim]

Using the ask function on Z3Session, we can pass commands such as check-sat and get-model to the z3 solver. The problem is that we can't read back the result of get-model, as z3 outputs it over multiple lines and the ask command only reads single-line responses, yielding an incomplete S-expression. There are 2 potential ways to fix this:

1. Change ask to read more than one line.
2. Somehow tell z3 to output stuff in one long line.

is either of the two doable?

[gebner]

I don't think you can tell z3 to write everything on a single line.

Unfortunately the parsing library we use for the s-expression parser does not allow us to resume parsing, see sirthias/parboiled2#26. I don't know how easy it is to check whether we hit the end-of-input in the parser (as opposed to a syntax error). But then we could just read lines as long as the parser says incomplete (and rerun the parser every time on the whole input).

[gebner]

BTW, the s-expression parser is pretty small. We could easily switch to another parsing library if that simplifies anything, as long as the performance remains reasonable.

[loewenheim]

Tbh I was thinking along the lines of changing ask to read from input until it hits an empty line or something similarly crude.

[gebner]

I'm not sure that would work. Z3 doesn't output empty lines after every response.