[question] how to see the formula that gets sent to the solver?

[jwaldmann]

I want to show liquid Haskell as an application of constraint programming. You are using QF_UFLRA?

Is there an easy way to see the actual formula that gets sent to the backend solver? (and the answer). I guess I could put a fake z3 executable in my PATH that does some extra printing but I was hoping there is something more direct.

[ranjitjhala]

Hi @jwaldmann -- yes, there is an easy way:

• if you run LH on some source file path/to/file.hs
• then LH generates the SMT queries in path/to/.liquid/file.hs.smt2

So you can see the generated SMT queries in the latter file.

I should say though, that the latter is not terribly readable, owing to the various intermediate layers of abstractions introduced by GHC, the liquid type checking and the SMT translation!

If you like you may be interested in this stripped down version of LH

https://github.com/ranjitjhala/sprite-lang

which uses many of the same ideas, but where you can look at the constraints more easily, both as

1. The "Horn Constraints" generated by refinement type checking, and
2. The "SMTLIB" queries generated to solve the horn constraints (1).

[jwaldmann]

interesting! yes I only need small examples, readability is good. I can build and run "sprite".

[facundominguez]

@jwaldmann, is this issue good to close?

[jwaldmann]

Yeah it's fine. I just copy here a code snippet buried in another issue https://github.com/ucsd-progsys/liquidhaskell/issues/2261#issuecomment-1915945047 that shows how to call the constraint solver directly:

cat tests/neg/.liquid/Fail.hs.smt2 |sed -e 's/Str/String/g' -e 's/strLen/str.len/g' | z3 /dev/stdin 
unsat
sat