Mourning for sbvExists/sbvForall

[arrowd]

Hi @LeventErkok

It is great to see new developments for SBV. Skolemization and DataKinds expression are certainly awesome feature, but I'm really disappointed to see sbvExists and sbvForall gone (even without deprecation period!)

Without sbvExists and co. how do I rewrite this

v <- if cond
    then sbvExists "foo"
    else literal bar

or this

vars <- mapM sbvExists $ genericTake numInputs ["InputLoc" ++ show i | i <- [1..]]

?

sbvExists and co. seem simpler and less verbose for me in some cases, so it is really unfortunate that you removed them.

[LeventErkok]

First one can be written as:

v <- if cond
        then free "foo"
        else literal bar

or, if you want:

v <- free "foo"
when cond $ constrain (v .== literal bar)

Second one is similar, simply use free:

vars  <- mapM free $ genericTake numInputs ["InputLoc" ++ show I | I <- [1..]]

Any reason why these won't work for you? It seems to me that all your uses of sbvExists can simply be replaced by free and it should work just fine. (I can imagine complications if you are mixing quantifiers, but that's why the old system was really bad anyhow. The new mechanism handles alternating quantifiers much better.)

[arrowd]

Yes, I though about free, but I looked into its implementation and found it to be a bit different from the sbvExists one. I'm not sure what what's exactly different between them, but if you say it will work then fine.

Another question is what to use in place of sbvForall? In my case I have both sbvExists and sbvForall in the same Symbolic action.

[LeventErkok]

free means existential in a sat call, and universal in prove call. This is the most common use case. If you want to alternate/nest quantifiers, then you use the new mechanism:

\(Exists @"x" x) (Forall @"y" y) (Exists @"z" z) -> ... code using x y z, which might have other quantifiers

For modeling purposes, you probably want to skolemize your formula, since SBV will only display the values of existentials at the outermost level. You can do this manually, or use the new skolemize function, which will do it for you.

Long story short, everything the old SBV did regarding quantifiers, the new implementation can handle too, and in a much more disciplined and cleaner way.

I find it is always better to talk in terms of concrete examples; so if you have an actual concrete example you're having trouble with, feel free to share and I'll take a look. (i.e., one that worked in the old system but you're having hard time coding in the new.)

[LeventErkok]

I should also note that we have ExistsN/ForallN abstractions as well, which allows for creation multiple of such variables if that's what you're trying to do. See:

• https://hackage.haskell.org/package/sbv-10.1/docs/Data-SBV.html#v:ForallN
• https://hackage.haskell.org/package/sbv-10.1/docs/Data-SBV.html#v:ExistsN
• https://hackage.haskell.org/package/sbv-10.1/docs/Data-SBV.html#v:ExistsUnique

Some extra comments are at: https://hackage.haskell.org/package/sbv-10.1/docs/Data-SBV.html#g:44

[LeventErkok]

@arrowd Is there any action item for SBV on this? Let's close the issue if not.

[arrowd]

I was planning to try to port my project to the new API this weekend, but we can probably close this issue and reopen it if I get into trouble with it.

[LeventErkok]

@arrowd Yes; feel fee to open a new issue if you run into trouble. Cheers..

[rsoeldner]

I'm trying to migrate some bigger code base and tried re-introducing sbvForall and sbvExits via the old implementation:

sbvForall :: SBVI.SymVal a => String -> Symbolic (SBVI.SBV a)
sbvForall = SBV.mkSymVal (SBVI.NonQueryVar (Just SBVI.ALL)) . Just

sbvExists :: SBVI.SymVal a => String -> Symbolic (SBVI.SBV a)
sbvExists = SBV.mkSymVal (SBVI.NonQueryVar (Just SBVI.EX)) . Just

Doing so breaks a few tests. I couldn't see any obvious reasons so-far. @LeventErkok is this, in general, a (short-term) option?

[LeventErkok]

@rsoeldner The implementation of quantifiers is completely redone; so your definitions of sbvForall and sbvExists will no longer work. You'll have to either stick to the old version of SBV, or adapt your code for the new system.