Possibility of an interface with better ergonomics?

[ksqsf]

The current interface IMHO is pretty primitive. The readme includes a 4queen example, but that is unnecessarily tedious, frustrating, and straight terrifying.

I believe you have more experience with z3 than me, but I made some simplifications to the 4queen example. It's still very tedious.

import Control.Applicative
import Control.Monad ( join )
import Data.Maybe
import qualified Data.Traversable as T

import Z3.Monad

run :: IO ()
run = evalZ3 script >>= \mbSol ->
        case mbSol of
             Nothing  -> error "No solution found."
             Just sol -> putStr "Solution: " >> print sol

script :: Z3 (Maybe [Integer])
script = do
  q <- traverse mkFreshIntVar ["q1", "q2", "q3", "q4"]
  [_1, _4] <- traverse mkInteger [1, 4]
  assert =<< mkAnd =<< sequence (   [ mkLe _1 qi | qi <- q ]
                                 ++ [ mkLe qi _4 | qi <- q ])
  assert =<< mkDistinct q
  assert =<< mkNot =<< mkOr =<< T.sequence [diagonal (j-i) (q!!i) (q!!j) | i<-[0..3], j<-[i+1..3]]
  fmap snd $ withModel $ \m ->
    catMaybes <$> mapM (evalInt m) q
  where mkAbs x = do
          _0 <- mkInteger 0
          join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
        diagonal d c c' =
          join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInteger (fromIntegral d))

Specifically,

1. Every call is prefixed with mk.
2. Every call is inside the Z3 monad, so even if it's just building an AST, there must be <$> and <*>. sequences are spilled everywhere without clear motivation.
3. Literals must be mk'd. This is an unnecessary burden.
4. Do we really need Int in evalInt m? The type seems to be deducible from the context.
5. mkLe mkSub ... They all seem unintuitive and ugly.

As I personally want to use Haskell for my next z3-related project, I'm concerned with the productivity implication. I used to use z3py. Simple tasks are really simple, intuitive, and even good-looking. But complex tasks are ugly (e.g. folding over a list of expressions). Haskell-z3 seems to be on the opposite extreme, where complex tasks are made fairly easy (e.g. assert =<< mkAnd =<< T.sequence [ mkLe _1 qi | qi <- q ] ) but simple tasks are less than ideal (e.g. mkInteger 0 >>= \_0 -> join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x versus z3py's straightforward If(0 <= x, x, -x)).

I believe Haskell-z3 can have the best of the both worlds. But before I set out to start coding, I decide to create an issue first to gather opinions: Is a better interface really needed? What could the design be? What are the previous attempts (if any) and how they turned out to be? After a design is sketched out, I'm willing to implement it. If it's not really important or it's a dead-end, I'll save some time. :)

(IMHO, the whole situation is like embedding the Z3 language into Haskell, and we automatically get several existing designs: Free monads, GADTs, and tagless final. But I'd like to add that Template Haskell should also be considered, as it allows us to write something like [z3| if 0 <= x then x else -x |] instead of mkInteger 0 >>= \_0 -> join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x. This however still needs duplicating AST definitions, which is very undesirable.)

[maurobringolf]

Hi and thanks for starting this discussion again!

About 5 months ago I asked the same thing, e.g. building an improved interface layer over the current one. There has been an attempt at this in the past:

https://hackage.haskell.org/package/z3-0.3.2/docs/Z3-Lang-Prelude.html

As far as I understood it was abandoned because library users preferred to build their own abstractions which directly match their needs. But @IagoAbal told me that he is still open to it. I have not started working on this yet, but would love to. What I was missing so far was my own use case because I am currently not using the library in any projects. If you bring this, I am happy to help with building a higher-layer interface.

My perspective on your specific points:

1. Every call is prefixed with mk

The current API is a minimal wrapper around the C API, so the function names should just be camelCased versions of the original C API functions [1]. In my opinion, having consistent naming with the Z3 documentation is worth more than these prefixes hurt. In a higher layer interface we could definitely choose new names.

2. Every call is inside the Z3 monad, so even if it's just building an AST, there must be <$> and <*>. sequences are spilled everywhere without clear motivation.

I think this is because there isn't much of a Haskell AST, a Haskell AST node is just a wrapped ForeignPtr to the C AST node. So before being able to use a new node, the monadic action of calling the constructor needs to be performed. I think we should avoid re-defining and building a separate Haskell AST. But maybe we could play some tricks behind the scenes in order to make something like this possible (correct me if this is not what you described/wanted):

xPlusy <- mkAdd [mkFreshIntVar "x", mkFreshIntVar "y"]
-- as opposed to
x <- mkFreshIntVar "x"
y <- mkFreshIntVar "y"
xPlusy <- mkAdd [x,y]

3. Literals must be mk'd. This is an unnecessary burden.

Definitely! It would be very nice if we could automatically lift Haskell Bool and Int literals at least. But I think this is a job for a higher layer and this low-level API does not need it.

4. Do we really need Int in evalInt m? The type seems to be deducible from the context.

Since it is all ForeignPtrs from the Haskell perspective, there is no sort information on the Haskell level, e.g. the AST is untyped. So eval just computes a ForeignPtr -> ForeignPtr function and then additional information is required to interpret the resulting node. Deducing Int from the context would require a typed AST I believe.

5. mkLe mkSub ... They all seem unintuitive and ugly.

Same as point 1.

---

So I think there are two key ideas here worth discussing/pursuing:

1. Typed AST: The static option would be to differentiate AST types to be sorted directly in the Haskell type system (BoolAST, IntAST, ArrayAST s1 s2 etc), i.e. turn sort-errors directly into Haskell compiler errors. I think the type systems should be compatible such that this is possible in a natural way. But maybe there are API functions which then no longer typecheck on the Haskell level, not sure. Maximum safety, minimum flexibility. A second option could be dynamic where we store the sort as additional field with the AST node and check sorts at runtime. This would most likely give better error messages, but it is not 100% clear to me if that provides additional value since Z3 also sort-checks. It would still allow us to drop the Int from evalInt and the like.
2. Embedded SMT-language: Provide a translation mechanism from a Haskell subset to SMT AST via Template Haskell. This would resemble the Python API where plain Python expressions can represent SMT terms. Since the Z3 API is so vast, this is probably best started for a particular use case and then we could try to extend it.

Apart from these I think the current API has its place and should stay as a minimal transparent C wrapper.

[ksqsf]

Thanks for your detailed reply!

I agree that the low-level API should be kept, and the 'simpler' interface should be a separate module (or even a package).

But maybe we could play some tricks behind the scenes in order to make something like this possible (correct me if this is not what you described/wanted) [...]

I'm not sure how to do this, but this example looks really neat! If it's achievable, I believe most of my complaints are instantly gone.

Typed AST

It seems that the previous Z3.Lang is exactly this. I'm still not sure why it's abandoned. My guess is that a separate AST type doesn't always satisfy people's needs, so the interoperability with the low-level API is important. If so, a complete wrapper (like z3py) and/or convert functions from/to raw z3 types should be enough.

My plan is to first experiment with the previous Z3.Lang and see how it can be extended in the next few days.

Template Haskell

I think it can be used to generate Z3 monad-compatible code, so interoperability is better than typed AST. But on a second thought, syntax like [z3|if x<0 then -x else x] doesn't add more value than If (x<0) (-x) x, and we have to implement a type checker to infer the types of literals. (This is my gut feeling, so maybe I'm wrong here.)

[maurobringolf]

My plan is to first experiment with the previous Z3.Lang and see how it can be extended

Sounds good, feel free to ping me or report any problems/requests here. I will think about potential designs as well and hopefully then we can draft something.

[IagoAbal]

I think it's interesting to have a deep DSL. Generate an intermediate AST, perform some checks on it, then pass it down to the lower-level Z3 library. That should help making a better higher-level API, although errors would still be caught at runtime. I personally don't have time to get into that kind of project, but I am happy to participate in discussions and review code.

But I don't find a shallow DSL powered by Haskell's type hackery to be very interesting, and it's a lot harder and more work than one initially thinks. That is why we abandoned Z3.Lang. If you want to play with SMT and write stuff by hand... then yes a shallow DSL is very nice. But if you're writing a tool that uses Z3 as a verification backend, and then you generate different SMT problems depending on what you get as input... then that shallow DSL is not that useful and, in fact, it may actually be rather cumbersome to work with.

[ElijahVlasov]

Hey guys! What's the current state of this issue?

[ksqsf]

Hi! I wasn't aware of SBV when I opened this issue. I was frustrated then, because I thought Haskell deserved something better than a low level wrapper. It took me some time to discover (maybe rediscover?) SBV. SBV seems pretty complete and capable, and fulfills my current needs.

I certainly see the necessity of a low-level Z3 library (the current haskell-z3), but I'm not sure I want to work on a / another Z3-specific high-level wrapper now. So, feel free to close this issue! :)