Some additional SMTLib2.6 support

[robdockins]

It would be convenient for some use cases I have if boolector supported the get-info and reset-assertions commands from SMTLib2.6 (cf http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf)

$ boolector --version
3.2.1

$ boolector -i
(get-info :version)
boolector: <stdin>:1:2: unsupported command 'get-info'

$ boolector -i
(get-info :error-behavior)
boolector: <stdin>:1:2: unsupported command 'get-info'

$ boolector -i
(reset-assertions)
boolector: <stdin>:1:2: expected command at 'reset-assertions'

[aytey]

If you can provide an example (as per stp/stp#365), then I can also take a look at implementing it for Boolector as well.

However, things are currently in-flux for Boolector in favour of Aina/Mathias's new solver (Bitwuzla). I am not sure they're taking feature PRs against Boolector before Bitwuzla comes out (later this year).

[robdockins]

The following example uses reset-assertions, and is accepted by Z3 and CVC4, but not Boolector.

quickstart-alt.txt

[aytey]

I’m (genuinely) happy to take a look at this; I just need to wait on my second paragraph (the work is worthless for you if it is unlikely to get merged).

[robdockins]

No problem, this isn't urgent for me, I just wanted to be sure I got a test case in the ticket before I forgot.

[mpreiner]

I already looked into adding support for (reset-assertions) a while ago and it's not that easy to add because of Boolector's current architecture. @robdockins is there a specific reason why you use (reset-assertions) + global-declarations instead of push/pop?

[robdockins]

The most ordinary use case does use push/pop because that's what makes the most sense when you are working "locally" according to the control-flow of a program. However, sometimes you want to break focus on one area and transition to a different focus. The easiest way to do this is to reset the solver state and establish a new context by pushing fresh frames and asserting new path conditions. I could do that by manually popping all the currently pushed frames, and being careful never to assert anything at top level... but it's more bookeeping and would be a code path specific to solvers that don't support reset-assertions. I could instead (reset) and also just resend all the declarations, but boolector doesn't support that either. Finally, I can also just shut everything down and start a new solver instance, but that has associated process startup costs in addition to losing all context.

In short, there's other workarounds, but I prefer to use the most direct methods when possible, especially if those methods can be generic across as many solvers as possible. It helps to prevent subtle solver-specific bugs

[mpreiner]

We may be able to add support for the (reset) command, but no ETA (our focus is now on Bitwuzla). @robdockins would that help? Unfortunately, (reset-assertions) is out of the question.

[robdockins]

Currently, my workaround is to just (push) an extra frame at the beginning of an interaction and pretend that's the top-level. When I would otherwise do a (reset-assertions), I just pop all the frames and push a new one. It's a little more bookkeeping for me, but otherwise works fine. In fact, I might suggest you do basically that behind the scenes as a way to implement reset-assertions on your end.

At any rate, (reset) doesn't actually help me much, and I currently have a workaround, so I'm not in a hurry.

[mpreiner]

An initial push works, but doing this by default hurts performance. We could however add an option to enable this behavior, what do you think @robdockins .

[robdockins]

If such an option existed, I'd probably use it. When using the incremental mode, I'm usually deep inside a stack of frames anyway.

[mpreiner]

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.