Entry stack behaviour

[georgefst]

We've been trying to convert a tool from using the sbv library to what4, which seems like a better fit for our work. Our one remaining issue involves manipulation of the entry stack. For example, from my experience with sbv, and my understanding of smtlib, I would have expected:

pushEntryStack w
assume w p
popEntryStack w

to always be a no-op. But it appears that the assumption of p remains on returning to the previous context.

So what is going on here, and how then would we use what4 to check satisfiabilty of a single predicate, within the current context, without infecting the global state?

[robdockins]

Sorry, the way the APIs are layered here can be a little confusing! The entry stack is really an internal bookeeping data structure that's used to keep track of what definitions are in scope, and not necessarily what logical conditions have been asserted.

To do that, you'll want to use the push, pop or inNewFrame operations from What4.Protocol.Online.

In that case your sequence will look something like:

do push proc
   assume (solverConn proc) p
   res <- check proc "check"
   pop proc

Or, you can have the whole sequence bundled up with the checkSatisfiable or checkSatisfaibleWithModel operations.

[georgefst]

Aha, thanks! I should have known there'd be a nicer API somewhere... I'm still finding my way around the what4 haddocks - there's a lot to take in!

I assume there's no real harm in the String argument to checkSatisfiable etc. being ""? Digging in to the source, it appears to just be used for logging.

[robdockins]

Yes, that string is just used for logging. If you don't find it useful, it's fine to leave it empty.