search

tweag / smtlib-backends

A Haskell library providing low-level functions for SMTLIB-based interaction with SMT solvers.
https://hackage.haskell.org/package/smtlib-backends
MIT License
17 stars 1 forks source link

Document edge cases of the SMTLIB API #51

Closed qaristote closed 1 year ago

qaristote commented 1 year ago

I think we should document the edge cases of the SMTLIB API somewhere.

For instance, what happens if we send an empty command to the solver ? Does it fail ? Does it just return an empty line ? Does the behavior differ depending on the backend ? (here the answer seems to be that for both backend the solver returns an empty line). Another behavior that's non-trivial is when sending a command that doesn't produce an output. For the Z3 backend the behavior is clear, but for the Process backend we don't get any response, not even an empty line.

These kinds of questions may come back frequently when adding new features and it'd probably be more efficient to have our own resource then having to go through the SMTLIB documentation (if it's even specified here) or just trying things out again in a REPL.

Perhaps the best place for this would be in the test-suites, since the behavior may depend on the backend, with some checks and a lot of comments.

facundominguez commented 1 year ago

We get the most freedom for future decisions by declaring the behavior as undefined. If no client relies on the behavior in these situations, no client will be broken when we settle for one direction or another.

qaristote commented 1 year ago

I guess one of the points of the library is to hide these possibly undefined behaviors: we ask ourselves these questions so the users don't have to. For instance flushing an empty queue relies on the behavior of the backends when processing empty commands. The user will assume that nothing happens, but we have to keep in mind that there's something to think about there.

facundominguez commented 1 year ago

For instance flushing an empty queue relies on the behavior of the backends when processing empty commands.

In that case there was a need that drove the definition. But why would a user want to try the cases considered here?

  1. evaluating command solver ""
  2. evaluating command "(push)" when :print-success false is set.

For the API, I argue that we need to wait rather than trying to guess what the behavior should be.

But it would be fine to have internal comments in the implementation of the backends or the testsuites, if all we care about is reminding to maintainers how the backends behave currently.

qaristote commented 1 year ago

Yeah my point wasn't that we should document it for the users, only for the maintainers.