iagoabal / haskell-z3

Haskell bindings to Microsoft's Z3 API (unofficial).

Haskell bindings for Microsoft's Z3 (unofficial)

These are Haskell bindings for the Z3 theorem prover. We don't provide any high-level interface (e.g. in the form of a Haskell eDSL) here, these bindings are targeted to those who want to build verification tools on top of Z3 in Haskell.

Changelog here.

Examples here.

Do you want to contribute?

State of maintenance

The library is currently "maintained", meaning that I try to be responsive to new issues and pull requests. Unfortunately I do not have time to investigate issues or to do major work myself. I do try to help those who want to contribute.

If someone demonstrates willingness to maintain the library more actively in the long run, then I will be very happy to give the required permissions to become a co-maintainer. In the meantime I will do my best to keep it alive.

Supported versions and version policy

Z3 releases come out often and sometimes introduce backwards incompatible changes. In order to avoid churn and #ifdef-ery, we only support recent releases of the latest Z3 minor version. We use semantic versioning to reflect which versions are supported:

<z3-version>.<bindings-version>[.<patch-level>]

The <z3-version> indicates which version of Z3 is supported, it is computed as x*100+y for Z3 x.y. For example, versions 408.y.z of these bindings are meant to support versions 4.8.* of Z3. This version policy is in line with Haskell's PVP. If you are using an older solver version you can check compatibility with these bindings below:

Z3-4.8.* compatibility

Bindings version / Z3 version	4.8.12	4.8.11	4.8.10	4.8.9	4.8.7	4.8.6	4.8.5	4.8.4	4.8.3	4.8.1
408.3	✔	✔	✔	✔	❌	❌	❌	❌	❌	❌
408.2	✔	✔	✔	✔	✔	✔	✔	❌	❌	❌
408.1	✔	✔	✔	✔	✔	✔	✔	✔	✔	✔
408.0	❌	❌	❌	❌	❌	❌	❌	✔	✔	✔

Installation

Preferably use the z3 package.

• Install a Z3 4.x release. (Support for Z3 3.x is provided by the 0.3.2 version of these bindings.)

• Just type cabal install z3 if you used the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include).

  • Otherwise use the --extra-lib-dirs and --extra-include-dirs Cabal flags when installing.

Example

Most people use the Z3.Monad interface. Here is an example script that solves the 4-queen puzzle:

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

import Z3.Monad

script :: Z3 (Maybe [Integer])
script = do
  q1 <- mkFreshIntVar "q1"
  q2 <- mkFreshIntVar "q2"
  q3 <- mkFreshIntVar "q3"
  q4 <- mkFreshIntVar "q4"
  _1 <- mkInteger 1
  _4 <- mkInteger 4
  -- the ith-queen is in the ith-row.
  -- qi is the column of the ith-queen
  assert =<< mkAnd =<< T.sequence
    [ mkLe _1 q1, mkLe q1 _4  -- 1 <= q1 <= 4
    , mkLe _1 q2, mkLe q2 _4
    , mkLe _1 q3, mkLe q3 _4
    , mkLe _1 q4, mkLe q4 _4
    ]
  -- different columns
  assert =<< mkDistinct [q1,q2,q3,q4]
  -- avoid diagonal attacks
  assert =<< mkNot =<< mkOr =<< T.sequence
    [ diagonal 1 q1 q2  -- diagonal line of attack between q1 and q2
    , diagonal 2 q1 q3
    , diagonal 3 q1 q4
    , diagonal 1 q2 q3
    , diagonal 2 q2 q4
    , diagonal 1 q3 q4
    ]
  -- check and get solution
  fmap snd $ withModel $ \m ->
    catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]
  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 d)

In order to run this SMT script:

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

Garbage Collection

This library automatically garbage collects all C objects created through its API.

Concurrency

Since version 408.3, this library implements thread-safety over the C API, i.e. API calls are serialized by locking on their Context argument. To safely compile for multi-threaded code please upgrade to >= 408.3.

Operations and objects in different Contexts can safely be accessed concurrently and are not synchronized by this library. Therefore, if you want to achieve real concurrency, you must use a different Context in each thread. You can use the *_translate_* functions from Z3's API to copy objects between different Contexts.

haskell-z3's Issues

"Unexpected code was reached." when parsing

I'm using haskell-z3 v408.2 and z3 v4.8.15. When I try to run the example on using parsing (see below) I get the following error:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 414
UNEXPECTED CODE WAS REACHED.
Z3 4.8.15.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

The example in the readme runs fine though.

---

import Z3.Monad

main :: IO ()
main = evalZ3 script >>= print

-- Toy example SMTLIB string
smtStr1 :: String
smtStr1 = "(declare-const x Int)\n(assert (< x 5))"

smtStr2 :: String
smtStr2 = "(declare-const x Int)\n(assert (> x 5))"

script :: Z3 Result
script = do
  l <- parseSMTLib2String smtStr1 [] [] [] []
  r <- parseSMTLib2String smtStr2 [] [] [] []
  eq <- mkEq l r
  assert l
  assert r
  assert eq
  check

Derive a proper test suite from the existing examples

Reference URL's in haddock documentation seem to be broken.

solverCheckAndGetModel segfaults on timeout

solverCheckAndGetModel segfaults on timeout. Might we worth only calling getModel when sat:

                  Unsat -> return Nothing
                  _     -> Just <$> solverGetModel ctx solver

Problem installing on OSX

After successfully building z3 and installing it with homebrew, I tried installing your package with cabal

cabal install z3 --extra-lib-dirs=/usr/local/lib --extra-include-dirs=/usr/local/include

which gives the following error:

C.hsc:107:16: error: use of undeclared identifier 'Z3_PRINT_SMTLIB_COMPLIANT'; did you mean 'Z3_PRINT_SMTLIB2_COMPLIANT'? hsc_const (Z3_PRINT_SMTLIB_COMPLIANT); ^~~~~~~~~~~~~~~~~~~~~~~~~ Z3_PRINT_SMTLIB2_COMPLIANT /Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/template-hsc.h:38:10: note: expanded from macro 'hsc_const' if ((x) < 0) \ ^ /usr/local/include/z3_api.h:1339:5: note: 'Z3_PRINT_SMTLIB2_COMPLIANT' declared here Z3_PRINT_SMTLIB2_COMPLIANT ^ C.hsc:107:16: error: use of undeclared identifier 'Z3_PRINT_SMTLIB_COMPLIANT'; did you mean 'Z3_PRINT_SMTLIB2_COMPLIANT'? hsc_const (Z3_PRINT_SMTLIB_COMPLIANT); ^~~~~~~~~~~~~~~~~~~~~~~~~ Z3_PRINT_SMTLIB2_COMPLIANT /Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/template-hsc.h:39:41: note: expanded from macro 'hsc_const' hsc_printf ("%lld", (long long)(x)); \ ^ /usr/local/include/z3_api.h:1339:5: note: 'Z3_PRINT_SMTLIB2_COMPLIANT' declared here Z3_PRINT_SMTLIB2_COMPLIANT ^ C.hsc:107:16: error: use of undeclared identifier 'Z3_PRINT_SMTLIB_COMPLIANT'; did you mean 'Z3_PRINT_SMTLIB2_COMPLIANT'? hsc_const (Z3_PRINT_SMTLIB_COMPLIANT); ^~~~~~~~~~~~~~~~~~~~~~~~~ Z3_PRINT_SMTLIB2_COMPLIANT /Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/template-hsc.h:41:50: note: expanded from macro 'hsc_const' hsc_printf ("%llu", (unsigned long long)(x)); ^ /usr/local/include/z3_api.h:1339:5: note: 'Z3_PRINT_SMTLIB2_COMPLIANT' declared here Z3_PRINT_SMTLIB2_COMPLIANT ^ 3 errors generated. compiling dist/build/Z3/Base/C_hsc_make.c failed (exit code 1) command was: /usr/bin/gcc -c dist/build/Z3/Base/C_hsc_make.c -o dist/build/Z3/Base/C_hsc_make.o -m64 -fno-stack-protector -m64 -fno-stack-protector -m64 -D__GLASGOW_HASKELL__=802 -Ddarwin_BUILD_OS=1 -Dx86_64_BUILD_ARCH=1 -Ddarwin_HOST_OS=1 -Dx86_64_HOST_ARCH=1 -I/usr/local/include -Idist/build/autogen -Idist/build/global-autogen -include dist/build/autogen/cabal_macros.h -I/Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/base-4.10.0.0/include -I/Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/integer-gmp-1.0.1.0/include -I/Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/include -I/Library/Frameworks/GHC.framework/Versions/8.2.1-x86_64/usr/lib/ghc-8.2.1/include/ cabal: Leaving directory '/var/folders/m6/9d63gywn353_cj0j7bzkkwc80000gn/T/cabal-tmp-88691/z3-4.1.2' cabal: Error: some packages failed to install: z3-4.1.2-IrMNUxENpOpAgxQjUOQ13q failed during the building phase. The exception was: ExitFailure 1

Failure to compile with z3 4.8.5

Using z3 4.8.5, we get the compilation failure:

ld: warning: directory not found for option '-L/nix/store/jf934f80x9m0smswv4352l6mvlra1d8n-gcc-wrapper-7.4.0/lib'
Undefined symbols for architecture x86_64:
 "_Z3_get_error_msg_ex", referenced from:
     _c1b9Y_info in libHSalacrity-0.1.0.0-ttwAml4Vgy2aT7WCYfDT6.a(Compiler.o)
     _c1b9J_info in libHSalacrity-0.1.0.0-ttwAml4Vgy2aT7WCYfDT6.a(Compiler.o)
     _c18Gj_info in libHSz3-408.0-1WFnpTfCBrCIgiQLAlveou.a(Base.o)
     _c18Ig_info in libHSz3-408.0-1WFnpTfCBrCIgiQLAlveou.a(Base.o)
     _c18Ng_info in libHSz3-408.0-1WFnpTfCBrCIgiQLAlveou.a(Base.o)
     _c18Q9_info in libHSz3-408.0-1WFnpTfCBrCIgiQLAlveou.a(Base.o)
     _c1ap4_info in libHSz3-408.0-1WFnpTfCBrCIgiQLAlveou.a(Base.o)
     ...                    
ld: symbol(s) not found for architecture x86_64
clang-7: error: linker command failed with exit code 1 (use -v to see invocation)
`cc' failed in phase `Linker'. (Exit code: 1)

(The above is the error using clang on a mac, but a similar error happens using gcc on linux.)

MonadZ3 for ReaderT

I currently have

instance MonadZ3 m => MonadZ3 (ReaderT r m) where
  getSolver = ReaderT $ const getSolver
  getContext = ReaderT $ const getContext

in my code base which is a pretty straightforward implementation. But:

1. It's an orphan instance.
2. It can probably be useful for somebody else if they wish to carry additional context around MonadZ3.

I probably wouldn't have considered wasting time discussing this and just opened a PR with these three lines straight ahead, but I noticed 3ec14bc, so I thought it's worth double-checking if it's a desirable direction, and, if so, if it's the best way to implement this change.

So, what are your thoughts on this?

Empty model with Z3 >=4.8

Haskell-Z3 408.0 returns an empty model, even when deciding that a query is satisfiable, when used with Z3 >= 4.8. The problem does not occur with Z3 4.4.

Steps to reproduce

Compile and run the following program:

module Main where
import Control.Monad.IO.Class
import Z3.Monad

main :: IO ()
main = evalZ3 $ do
  a <- mkFreshBoolVar "a"
  b <- mkFreshBoolVar "b"
  assert =<< mkAnd [a, b]
  (result, model) <- withModel modelToString
  liftIO $ do
    print result
    maybe (putStrLn "no model") putStr model

Expected result

The program prints:

Sat
b!1 -> true
a!0 -> true

This is what happens when Z3 4.8 is replaced with 4.4.

Actual result

The program prints:

Sat

Additional details

The problem is not just with modelToString, as calling numConsts on the model returns 0 (and calling getConsts causes a Z3 error: index out of bounds to be thrown).

Crash on parseSMTLib2String

I'm seeing the following using haskell-z3 version 408.0 and z3 version 4.8.4 on a 64-bit Pop!_OS (Ubuntu-based) install, OS version 19.04.

Parsing a simple SMTLib2 string and displaying the AST crashes with what looks like a memory management error:

$ ghci
GHCi, version 8.4.4: http://www.haskell.org/ghc/  :? for help
Prelude> import Z3.Monad
Prelude Z3.Monad> ast <- evalZ3 $ parseSMTLib2String "(assert true)" [] [] [] []
Prelude Z3.Monad> s <- evalZ3 $ astToString ast
double free or corruption (out)
Aborted (core dumped)

I inspected this in gdb and saw the following backtrace:

#0  __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1  0x00007ffff67f9535 in __GI_abort () at abort.c:79
#2  0x00007ffff6860726 in __libc_message (action=action@entry=do_abort, fmt=fmt@entry=0x7ffff6986952 "%s\n") at ../sysdeps/posix/libc_fatal.c:181
#3  0x00007ffff686759a in malloc_printerr (str=str@entry=0x7ffff6984ab3 "free(): invalid size") at malloc.c:5352
#4  0x00007ffff68693dc in _int_free (av=<optimized out>, p=0x7fffffff94a0, have_lock=<optimized out>) at malloc.c:4185
#5  0x00007ffff6b909c7 in shared_occs::operator()(expr*, shared_occs_mark&) [clone .cold.69] () from /lib/libz3.so
#6  0x00007ffff78493ac in shared_occs::operator()(expr*) () from /lib/libz3.so
#7  0x00007ffff7878eff in smt2_printer::process(expr*, obj_ref<app, ast_manager>&) () from /lib/libz3.so
#8  0x00007ffff787a825 in smt2_printer::operator()(expr*, unsigned int, char const*, obj_ref<app, ast_manager>&, sbuffer<symbol, 16u>&) () from /lib/libz3.so
#9  0x00007ffff7873ced in ast_smt2_pp(std::ostream&, expr*, smt2_pp_environment&, params_ref const&, unsigned int, unsigned int, char const*) () from /lib/libz3.so
#10 0x00007ffff7873ed7 in operator<<(std::ostream&, mk_ismt2_pp const&) () from /lib/libz3.so
#11 0x00007ffff6c19093 in Z3_ast_to_string () from /lib/libz3.so
#12 0x00000000005c1263 in ?? ()
#13 0x0000000000000000 in ?? ()

I was unable to reproduce this on an up-to-date MacOS install with z3 version 4.8.0 (so an earlier point release.)

Because of the "double free" in the error message, I originally thought this might be a finalizer race or similar, with a certain GC ordering triggering some bad sequence of free()s. Seeing "invalid size" in the backtrace and the MacOS non-repro makes me wonder if it could be something more platform-specific, though?

I'm stuck on what to investigate next to understand why this is happening. Any thoughts?

Question about the monadic semantic

Hi, I have a question regarding the semantics of the monadic interface of this package. Here's an example from the examples folder, which I slightly modified adding a slightly different version (grep "take two"):

import Z3.Monad
import Control.Monad.Trans (liftIO)
import Control.Monad

run :: IO ()
run = evalZ3 datatypeScript

mkCellDatatype :: Z3 Sort
mkCellDatatype = do
  -- Create a cell data type of the form:
  -- data Cell = Nil | Cons {car :: Cell, cdr :: Cell}

  -- Nil constructor
  nil      <- mkStringSymbol "Nil"
  isNil    <- mkStringSymbol "is_Nil"
  nilConst <- mkConstructor nil isNil []

  -- Cons constructor
  car    <- mkStringSymbol "car"
  cdr    <- mkStringSymbol "cdr"
  cons   <- mkStringSymbol "Cons"
  isCons <- mkStringSymbol "is_Cons"
  -- In the following, car and cdr are the field names. The second argument,
  -- their sort, is Nothing, since this is a recursive sort. The third argument is
  -- 0, since the type is not mutually recursive.
  consConst <- mkConstructor cons isCons [(car,Nothing,0),(cdr,Nothing,0)]

  -- Cell datatype
  cell <- mkStringSymbol "Cell"
  mkDatatype cell [nilConst, consConst]

cons_ :: Z3 AST -> Z3 AST -> Z3 AST
cons_ a b = do
  cell <- mkCellDatatype
  ~[_, consConst] <- getDatatypeSortConstructors cell
  a' <- a
  b' <- b
  mkApp consConst [a', b']
  
nil_ :: Z3 AST
nil_ = do
  cell <- mkCellDatatype
  ~[nilConst, _] <- getDatatypeSortConstructors cell
  mkApp nilConst []

eq_ :: Z3 AST -> Z3 AST -> Z3 AST
eq_ a b = do
  a' <- a
  b' <- b
  mkEq a' b'

not_ :: Z3 AST -> Z3 AST
not_ a = a >>= mkNot

assert_ :: Z3 AST -> Z3 ()
assert_ = (>>= assert)

implies_ :: Z3 AST -> Z3 AST -> Z3 AST
implies_ a b = join (mkImplies <$> a <*> b)

and_ :: [Z3 AST] -> Z3 AST
and_ a = sequence a >>= mkAnd

datatypeScript :: Z3 ()
datatypeScript = do
  cell <- mkCellDatatype
  ~[nilConst, consConst] <- getDatatypeSortConstructors cell

  liftIO $ putStrLn "prove (cons (x,u) = cons(y,v) => x = y && u = v) //Expect Unsat"
  ~[u,v,x,y] <- mapM (flip mkFreshConst cell) ["u","v","x","y"]
  t1 <- mkApp consConst [x,u]
  t2 <- mkApp consConst [y,v]
  p1 <- mkEq t1 t2
  p2 <- mkEq x y
  p3 <- mkEq u v
  p4 <- mkAnd [p2, p3]
  p5 <- mkImplies p1 p4
  push
  mkNot p5 >>= assert
  check >>= liftIO . print
  pop 1

  liftIO $ putStrLn "TAKE TWO: prove (cons (x,u) = cons(y,v) => x = y && u = v) //Expect Unsat"
  push
  assert_ . not_ $ implies_ (eq_ (cons_ (pure x) (pure u)) (cons_ (pure y) (pure v)))
                            (and_ [eq_  (pure x) (pure y), eq_ (pure u) (pure v)])
  check >>= liftIO . print
  pop 1

What is the difference between the two versions? I mean, in particular, what happens in the underlying monad if I call multiple times

mkDatatype cell [nilConst, consConst]

Is it semantically equal but adds cruft in the solver?

Things to know when updating bindings

Hi,
as the bindings lack a number of features that are now in the Z3 C API, I'd like to try my hand at bringing it up to speed. Do you have any suggestion on gotchas, possible mistakes to be avoided, and suggested workflows, @IagoAbal? Is there there something in that API that shouldn't be bound, or can I just start from the beginning and work my way down?

Runtime incompatibility with z3 >= 4.8 (undefined symbol: Z3_get_parser_error)

z3 4.7.1 is the last version to contain the symbol Z3_get_parser_error. This causes runtime failures in haskell-z3 with newer versions of z3.

Please note that the upstream API docs have not been regenerated since 4.8 was released, so the github hosted docs still claim to contain it, while the source (or indeed a fresh regeneration of the docs) do not. I don't know why it was removed, but it appears to have been done intentionally:

Z3Prover/z3@1eb8cca#diff-d6c80d51fca9ba3afd43693f09f35c1dL5288

Publish new version with new combinators (mkPower missing)

Documentation here: https://z3prover.github.io/api/html/group__capi.html#ga8414506c805caa171f0c1fe29f9f9612

error dyld Library not loaded: libz3.dylib

Hi,

I'm running macos mojave 10.14.6 and using stack to manage my haskell projects.

I'm having issues importing z3. I've configured my stack.yaml for my project as follows:

extra-deps:
- z3-408.2@sha256:1f8b6ccbcc6d06a6701900a09fcfcbaf86ed8a8495615710bef4da5cdb073a3f,4226
extra-include-dirs: [/Users/haliq/usr/include]
extra-lib-dirs: [/Users/haliq/usr/lib]

I've installed release z3-4.8.9 to the location specified above as follows

python scripts/mk_make.py --prefix=$HOME/usr --python --pypkgdir=$HOME/usr/lib/python-2.7/site-packages
cd build; make
make install

The libz3.dylib exists in the lib directory and various header files in include

But when i run stack build

Its trying to access libz3.dylib from a different location than the one specified in stack.yaml

z3    > configure
z3    > Configuring z3-408.2...
z3    > build
z3    > Preprocessing library for z3-408.2..
z3    > running .stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/C_hsc_make failed (exit code -6)
z3    > rsp file was: ".stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/hsc2hscall97343-3.rsp"
z3    > output file:".stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/C.hs"
z3    > command was: .stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/C_hsc_make  >.stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/C.hs
z3    > error: dyld: Library not loaded: libz3.dylib
z3    >   Referenced from: /private/var/folders/f6/128r_qx57953hch5znq5npq00000gn/T/stack-cab3f28c34c9f1db/z3-408.2/.stack-work/dist/x86_64-osx/Cabal-3.0.1.0/build/Z3/Base/C_hsc_make
z3    >   Reason: image not found
z3    >

Note the line Referenced from: ... is a different directory

Question about a fixpoint example

Hi, I'm trying to translate this example in z3's documentation using the api provided by this package. The closest thing I can get is:

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, DefaultSignatures          #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric, FlexibleContexts            #-}
{-# LANGUAGE FlexibleInstances, FunctionalDependencies, GADTs           #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeFamilyDependencies     #-}
{-# LANGUAGE TypeOperators, UndecidableInstances                        #-}

import Z3.Monad
import Control.Monad.Trans (liftIO)
import Control.Monad

run :: IO ()
run = evalZ3 fixpointComputation

fixpointComputation :: Z3 ()
fixpointComputation = do
  intSort <- mkIntSort
  edge <- join $ mkFuncDecl <$> (mkStringSymbol "edge") <*> pure [intSort, intSort] <*> mkBoolSort
  path <- join $ mkFuncDecl <$> (mkStringSymbol "path") <*> pure [intSort, intSort] <*> mkBoolSort
  a <- join $ mkVar <$> mkStringSymbol "a" <*> (pure intSort)
  b <- join $ mkVar <$> mkStringSymbol "b" <*> (pure intSort)
  c <- join $ mkVar <$> mkStringSymbol "c" <*> (pure intSort)
  fpAddRule (implies_ (mkApp edge [a,b]) (mkApp path [a,b])) (mkStringSymbol "ruleSymbol1")
  fpAddRule (implies_ (and_ [mkApp edge [a,b], mkApp edge [b,c]]) (mkApp path [a,c])) (mkStringSymbol "ruleSymbol2")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 1, ic 2]) (mkStringSymbol "base1")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 1, ic 3]) (mkStringSymbol "base2")
  fpAddRule (join $ mkApp <$> pure edge <*> sequence [ic 2, ic 4]) (mkStringSymbol "base3")
  q3 <- join $ mkFuncDecl <$> (mkStringSymbol "q3") <*> pure [intSort] <*> mkBoolSort
  one <- ic 1
  fpAddRule (implies_ (mkApp path [one,b]) (mkApp q3 [b])) (mkStringSymbol "q3rule")
  liftIO . putStrLn $ "AN ERROR IS ABOUT TO HAPPEN:"
  res <- fixedpointQueryRelations [q3]
  liftIO . putStrLn $ "The solution:"
  liftIO . print $ res
  astRes <- fixedpointGetAnswer
  astResString <- astToString astRes
  liftIO . print $ astResString

--------------------------------------------------------------------------------
-- Utilities
--------------------------------------------------------------------------------

(===) :: Z3 AST -> Z3 AST -> Z3 AST
(===) a b = join (mkEq <$> a <*> b)

not_ :: Z3 AST -> Z3 AST
not_ a = join (mkNot <$> a)

assert_ :: Z3 AST -> Z3 ()
assert_ a = join (assert <$> a)

implies_ :: Z3 AST -> Z3 AST -> Z3 AST
implies_ a b = join (mkImplies <$> a <*> b)

and_ :: [Z3 AST] -> Z3 AST
and_ a = sequence a >>= mkAnd

fpAddRule :: Z3 AST -> Z3 Symbol -> Z3 ()
fpAddRule a b = join $ fixedpointAddRule <$> a <*> b

fpRegisterRelation :: Z3 FuncDecl -> Z3 ()
fpRegisterRelation a = join $ fixedpointRegisterRelation <$> a

ic :: Int -> Z3 AST
ic n = join $ mkConst <$> mkIntSymbol n <*> mkIntSort

Unfortunately, if I try to run the run function, I get, after the warning I inserted:

AN ERROR IS ABOUT TO HAPPEN:
*** Exception: Z3 error: Illegal head. The head predicate needs to be uninterpreted and registered (as recursive) (path a b)

Could you show me how to get the output of the example problem?

NOTE for the reasons outlined in [#9] you shouldn't use the last z3 (z3-4.7.1 is ok)

Question: understanding the timing of `evalZ3`

Hi,
in a current project of mine, I am using z3 to solve a lot of small problems, via evalZ3 smallProblem. The typical time for one of these problems, brutally measured using :set +s in ghci, is around 0.3s.

Now, I'd like to understand where these 0.3s are spent: are they mainly spent in the z3 solution, or in the z3 process initialization, so that I would benefit from invoking the solver only once and resetting the solver state instead? Most importantly, how can I measure this?

Inconsistent integer argument handling

Motivated by #66 which used Integer int for all integer arguments, I looked into the matter. Our current types for integer API arguments are inconsistent and even allow some invalid Z3 API calls (admittedly edge cases though). In the C world it is common to use unsigned integers when appropriate and so does the Z3 C API. In the Haskell world it seems much less common and Int is everywhere. So we have a choice:

1. Use unsigned integer types ( Word, Word64 ) for unsigned int and unsigned long arguments. This means that API users have to do fromIntegral and think about under- and overflows themselves if they are using Int in their application.

2. Accept Int or Integral int and handle under- and overflows by

   1. Silently wrapping them around by just using fromIntegral.
   2. Adding runtime boundary checks and error-ing out if arguments fall outside of the target type range.

Our current choice is (2.i) in 95% of the cases and either (1) or (2.ii) in the rest.

Since this library is most useful in verification and similar fields where correctness is crucial, I think (2.i) is not good enough. Moving from (2) to (1) is a massive breaking change, so I propose we do (2.ii) using Integral int such that all types stay backwards compatible. Technically this is also a breaking change since we add new runtime errors, but these are proper edge cases where users most likely already get Z3 errors or crashes anyway, e.g. Z3.algebraicRoot ctx _ (-1) results in Z3 error: Overflow encountered when expanding vector. I think it would be much more helpful to error out in the HS API already. The cost is of course the runtime checks.

@IagoAbal I would like to hear your opinion before working on anything here.

---

Status quo

Cases of integer arguments into Z3 API functions

HS API type	C API type	Example	Range consistency
Integral int	CInt	mkIntSymbol	custom runtime error if outside range
Word64	CULLong	mkFiniteDomainSort	type system
Integral int	CUInt	mkBvSort	with function specific range check, but not full type range check
Int	CUInt	algebraicRoot	without range check
Word	CUInt	paramsSetUInt	type system
Int	CInt	mkReal	type system
Int64	CLLong	mkInt64	type system
Word64	CULLong	mkUnsignedInt64	type system

Installer deletes header files

I'm trying to install the z3 package on Windows 10 64 bit, Haskell Platform 8.4.3, with the following command (in Windows Powershell):

cabal install z3 --extra-lib-dirs=/z3-4.7.1-x64-win/bin --extra-include-dirs=/z3-4.7.1-x64-win/include

To my great surprise, the header files that were in the Z3 include directory before I ran this command, were no longer there afterwards! Something is going horribly wrong.
Output:

PS C:\mverifast\mverifast\mverifastgui> cabal install z3 --extra-lib-dirs=/z3-4.7.1-x64-win/bin --extra-include-dirs=/z3-4.7.1-x64-win/include
Resolving dependencies...
Configuring z3-4.3.1...
Failed to install z3-4.3.1
Build log ( C:\Users\bartj\AppData\Roaming\cabal\logs\ghc-8.4.3\z3-4.3.1-6btBgYDddap75zYSt6wHBl.log ):
Configuring z3-4.3.1...
cabal.exe: Missing dependency on a foreign library:
* Missing (or bad) header file: z3.h
This problem can usually be solved by installing the system package that
provides this library (you may need the "-dev" version). If the library is
already installed but in a non-standard location then you can use the flags
--extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
library file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
If the header file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.

cabal: Leaving directory 'C:\Users\bartj\AppData\Local\Temp\cabal-tmp-6032\z3-4.3.1'
cabal.exe: Error: some packages failed to install:
z3-4.3.1-6btBgYDddap75zYSt6wHBl failed during the configure step. The
exception was:
ExitFailure 1

Nondeterministic segfaults from z3

Apologies in advance for a vague issue report!

I am encountering frequent but nondeterministic segfaults from z3 using these bindings. After several hours of debugging, I haven't been able to figure out what's causing them. I suspect the issue is that I'm violating some assumption/invariant of the bindings, but I'm not sure. In some of the core dumps (included below) it looks like it might be some kind of double-delete error.

I'm using these bindings as part of a programming language interpreter. Here's a high-level view of what I'm doing:

1. Initialize a Solver and Context at the beginning of main.

2. Create symbolic boolean values for all relevant variables up front (using mkStringSymbol and mkBoolVar), and cache these in the relevant AST nodes for easy use later.

3. Add the solver and context from step 1 to a Reader context used in an evaluation monad used to evaluate my language. I've instantiated MonadZ3 for this monad, trivially returning the solver and context, so I can call functions like local, assert, and checkAssumptions from within this monad.

4. During evaluation, I use z3 in an incremental style, recursively creating assertions and checking satisfiability inside local calls. I use the cached symbolic values in the AST to construct more complex assertions using mkAnd, mkOr, etc.

Here are some oddities:

• Everything works about 30% of the time, the other 70% I get a segfault.
• If I insert short thread delays before assert and isSat calls, the rate of segfaults goes down to about 25%.
• The particular call that triggers the segfault is unpredictable.

When I don't include the thread delay, almost all of the core dumps look like this:

#0  0x00007f4a3f7715ca in ast_manager::delete_node(ast*) () from /lib64/libz3.so
#1  0x00007f4a3eb03e98 in Z3_dec_ref () from /lib64/libz3.so
#2  0x000000000049bdf5 in ?? ()
#3  0x0000000000000000 in ?? ()

When I do include the thread delay, the core dumps are more interesting. Here's one example:

#0  0x00007fe858f8305e in small_object_allocator::allocate(unsigned long) () from /lib64/libz3.so
#1  0x00007fe858bd8629 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) () from /lib64/libz3.so
#2  0x00007fe858bd9009 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) () from /lib64/libz3.so
#3  0x00007fe858b50426 in ?? () from /lib64/libz3.so
#4  0x00007fe858b5368b in ?? () from /lib64/libz3.so
#5  0x00007fe8585cfbe8 in asserted_formulas::assert_expr(expr*, app*) () from /lib64/libz3.so
#6  0x00007fe85872d07d in smt::context::assert_expr(expr*, app*) () from /lib64/libz3.so
#7  0x00007fe8589bfc4f in solver::assert_expr(expr*) () from /lib64/libz3.so
#8  0x00007fe8589bfc4f in solver::assert_expr(expr*) () from /lib64/libz3.so
#9  0x00007fe857f29b48 in Z3_solver_assert () from /lib64/libz3.so
#10 0x0000000000283309 in ResourcezmDSLzm0zi0zi0zmKprRwTLDuStJtRi6Xwqbkx_DSLziEvaluation_zdwzdsinVCtx_info ()
#11 0x0000000000000000 in ?? ()

Here's another with the thread delay:

#0  0x00007f2714392e35 in raise () from /lib64/libc.so.6
#1  0x00007f271437d895 in abort () from /lib64/libc.so.6
#2  0x00007f27143d623f in __libc_message () from /lib64/libc.so.6
#3  0x00007f27143dd7bc in malloc_printerr () from /lib64/libc.so.6
#4  0x00007f27143def1c in _int_free () from /lib64/libc.so.6
#5  0x00007f2715bf7d64 in memory::deallocate(void*) () from /lib64/libz3.so
#6  0x00007f27158497e3 in ast_manager::delete_node(ast*) () from /lib64/libz3.so
#7  0x00007f2714bdbe98 in Z3_dec_ref () from /lib64/libz3.so
#8  0x000000000049c0cd in ?? ()
#9  0x0000000000000000 in ?? ()

Thank you very much in advance for any insight you can provide!

Error running examples on Ubuntu 18.04

I have Z3 installed, version 4.4.0, have created a haskell project in which I have added z3 dependency on my .cabal file:

build-depends: z3 >= 4.3

If I try to add code from the examples to one of my project files, such as: (from ParserInterface.hs)

import Z3.Monad

run :: IO ()
run = evalZ3 script >>= print

-- Toy example SMTLIB string
smtStr1 :: String
smtStr1 = "(declare-const x Int)\n(assert (< x 5))"

smtStr2 :: String
smtStr2 = "(declare-const x Int)\n(assert (> x 5))"


script :: Z3 Result
script = do
  l <- parseSMTLib2String smtStr1 [] [] [] []
  r <- parseSMTLib2String smtStr2 [] [] [] []
  eq <- mkEq l r
  assert l
  assert r
  assert eq
  check

then cabal install fails with this linking errors:

nicolas@nico-M4700:~/MateFun$ cabal install
Warning: cannot determine version of /usr/local/bin/hpc :
""
Resolving dependencies...
Notice: installing into a sandbox located at
/home/nicolas/MateFun/.cabal-sandbox
Configuring MateFun-0.6.1...
Building MateFun-0.6.1...
Failed to install MateFun-0.6.1
Build log ( /home/nicolas/MateFun/.cabal-sandbox/logs/MateFun-0.6.1.log ):
cabal: Entering directory '.'
Configuring MateFun-0.6.1...
Building MateFun-0.6.1...
Preprocessing executable 'MateFun' for MateFun-0.6.1...
Linking dist/dist-sandbox-92f89273/build/MateFun/MateFun ...
/home/nicolas/MateFun/.cabal-sandbox/lib/x86_64-linux-ghc-8.0.1/z3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo/libHSz3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo.a(Base.o):(.text+0x180d0): undefined reference to `Z3_get_parser_error'
/home/nicolas/MateFun/.cabal-sandbox/lib/x86_64-linux-ghc-8.0.1/z3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo/libHSz3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo.a(C.o):(.text+0xdbdc): undefined reference to `Z3_add_func_interp'
/home/nicolas/MateFun/.cabal-sandbox/lib/x86_64-linux-ghc-8.0.1/z3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo/libHSz3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo.a(C.o):(.text+0xdd5f): undefined reference to `Z3_add_const_interp'
/home/nicolas/MateFun/.cabal-sandbox/lib/x86_64-linux-ghc-8.0.1/z3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo/libHSz3-4.3.1-ASx9PyKYlPsKRW7mw0pEEo.a(C.o):(.text+0x13610): undefined reference to `Z3_get_parser_error'
collect2: error: ld returned 1 exit status
`gcc' failed in phase `Linker'. (Exit code: 1)
cabal: Leaving directory '.'
cabal: Error: some packages failed to install:
MateFun-0.6.1 failed during the building phase. The exception was:
ExitFailure 1

Set up CI to check that the bindings work against new Z3 releases

Reference URL's in haddock documentation seem to be broken

It seems that microsoft has changed the url containing the Z3 documentation, breaking the links in the Haskell Z3 module documentation. For example:
https://hackage.haskell.org/package/z3-408.2/docs/Z3-Monad.html#v:mkTrue

Points to:

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7
Which leads to a general landing page.

Unable to install on M1/M2 Mac

I'm running into issues installing Haskell z3 on my m2 MacBook. I've ran the following commands:

brew install z3
cabal install z3 --lib

This results in the following error message:

Resolving dependencies...
Build profile: -w ghc-9.2.8 -O1
In order, the following will be built (use -v for more details):
 - z3-408.2 (lib) (requires build)
Starting     z3-408.2 (lib)

Failed to build z3-408.2. The failure occurred during the configure step.
Build log ( /Users/nna/.cabal/logs/ghc-9.2.8/z3-408.2-14ff341a.log ):
Configuring library for z3-408.2..
cabal-3.6.2.0: Missing dependency on a foreign library:
* Missing (or bad) header file: z3.h
* Missing (or bad) C library: z3
This problem can usually be solved by installing the system package that
provides this library (you may need the "-dev" version). If the library is
already installed but in a non-standard location then you can use the flags
--extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
library file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
If the header file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.

cabal: Failed to build z3-408.2. See the build log above for details.

Since I'm on M2 Mac, it seems like homebrew will install z3 in a different location:

% brew info z3          
==> z3: stable 4.12.2 (bottled), HEAD
High-performance theorem prover
https://github.com/Z3Prover/z3
/opt/homebrew/Cellar/z3/4.12.2 (118 files, 30.6MB) *
  Poured from bottle using the formulae.brew.sh API on 2023-09-05 at 12:33:32
From: https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/z/z3.rb
License: MIT
==> Dependencies
Build: cmake ✘, [email protected] ✘
==> Options
--HEAD
	Install HEAD version
==> Analytics
install: 16,081 (30 days), 42,436 (90 days), 92,273 (365 days)
install-on-request: 343 (30 days), 1,161 (90 days), 3,556 (365 days)
build-error: 403 (30 days)

From the error message from Haskell z3, I would suspect that then the following should work, but it does not:

cabal install z3 --lib --extra-lib-dirs=/opt/homebrew/Cellar/z3/4.12.2/lib --extra-include-dirs=/opt/homebrew/Cellar/z3/4.12.2/include

Any help would be greatly appreciated!

MonadFail and GHC 8.6+

It looks like the z3 library doesn’t play nicely with the MonadFail desugaring changes starting in GHC 8.6. I’ll submit a pull request shortly.

Cannot build with Z3 4.8.5

Preprocessing library for z3-408.0..
Building library for z3-408.0..
[1 of 4] Compiling Z3.Base.C        ( dist/build/Z3/Base/C.hs, dist/build/Z3/Base/C.o )
[2 of 4] Compiling Z3.Base          ( src/Z3/Base.hs, dist/build/Z3/Base.o )
[3 of 4] Compiling Z3.Opts          ( src/Z3/Opts.hs, dist/build/Z3/Opts.o )
[4 of 4] Compiling Z3.Monad         ( src/Z3/Monad.hs, dist/build/Z3/Monad.o )
[1 of 4] Compiling Z3.Base.C        ( dist/build/Z3/Base/C.hs, dist/build/Z3/Base/C.p_o )
[2 of 4] Compiling Z3.Base          ( src/Z3/Base.hs, dist/build/Z3/Base.p_o )
[3 of 4] Compiling Z3.Opts          ( src/Z3/Opts.hs, dist/build/Z3/Opts.p_o )
[4 of 4] Compiling Z3.Monad         ( src/Z3/Monad.hs, dist/build/Z3/Monad.p_o )
Preprocessing test suite 'spec' for z3-408.0..
Building test suite 'spec' for z3-408.0..
[1 of 2] Compiling Z3.Base.Spec     ( test/Z3/Base/Spec.hs, dist/build/spec/spec-tmp/Z3/Base/Spec.o )
[2 of 2] Compiling Main             ( test/Spec.hs, dist/build/spec/spec-tmp/Main.o )
Linking dist/build/spec/spec ...
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: dist/build/spec/spec-tmp/Z3/Base/Spec.o: in function `c8YP_info':
(.text.s8Ln_info+0x278): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o):(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkIntSort_info+0x9c): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c191G_info':
(.text.s10Eu_info+0x240): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c195Q_info':
(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkTrue_info+0x14d): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o): in function `c197F_info':
(.text.zz3zm408zi0zm7xF7S34UzzMR9jLZZteoIWY7_ZZ3ziBase_zdwmkFalse_info+0x14d): undefined reference to `Z3_get_error_msg_ex'
/nix/store/3pyyiahac08rz0vszvpjvnk1pkggqqr2-binutils-2.31.1/bin/ld: /build/z3-408.0/dist/build/libHSz3-408.0-7xF7S34UzMR9jLZteoIWY7.a(Base.o):(.text.s10LJ_info+0x280): more undefined references to `Z3_get_error_msg_ex' follow

Z3 removed Z3_fixpoint_push/pop

Z3Prover/z3@40e329f

I'm not sure what the fix is, but Z3 4.8.5 removed these api fxns which can cause problems with the haskell bindings now

Possibility of an interface with better ergonomics?

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.)

Installation on Windows 10

I'm having trouble building a Cabal project with the z3 bindings.

The following is the minimum (faulty) example:

Using a project initialized by cabal init:

test/
- Main.hs
- Setup.hs
- CHANGELOG.md
- test.cabal

With modified test.cabal:

cabal-version:         3.0
name:                  z3-test
version:               0.1.0.0
extra-source-files:    CHANGELOG.md
executable test
  main-is:             Main.hs
  build-depends:       base                    >=4.14 && <4.15
                       , z3                    ^>=408.2
  default-language:    Haskell2010
  extra-libraries:     C:\z3-4.8.5-x64-win\bin 
  extra-lib-dirs:      C:\z3-4.8.5-x64-win\include

Z3 binaries are located at C:\z3-4.8.5-x64-win. and installed: cabal v1-install z3 --extra-lib-dirs=C:/z3-4.8.5-x64-win/bin --extra-include-dirs=C:/z3-4.8.5-x64-win/include

All the requested packages are already installed:
z3-408.2
Use --reinstall if you want to reinstall anyway.

now building the project using:

cabal v1-build

Results in the error:

Preprocessing executable 'test' for z3-test-0.1.0.0..
Building executable 'test' for z3-test-0.1.0.0..
Linking dist\build\test\test.exe ...
C://ProgramData//chocolatey//lib//ghc//tools//ghc-8.10.2//mingw//bin/ld.exe: cannot find -lC:\z3-4.8.5-x64-win\bin
collect2.exe: error: ld returned 1 exit status
`gcc.exe' failed in phase `Linker'. (Exit code: 1)

Result of cabal v1-build -v3 is

How can I build a project with the z3 bindings?

Note that:

• I can only use cabal
• Using cabal install ... or cabal v2-install ... results in Cannot build .. z3 because none of the components are available to build:

Support for parametric datatypes

I've been considering before using bindings to z3 for Liquid Haskell. The thing that deterred me at the time was that Liquid Haskell uses parametric types via SMTLIB2, but I couldn't find in the api of z3 how to define the parameters. That is necessary, for instance, to define a sort of lists data List a = Nil | Cons a (List a).

By checking the example of haskell-z3, I also see that datatypes aren't parametric either.

Is this a limitation of the z3 API?

segfault on evalBv

I tried a bunch of different ways to get the model of a particular node. This doesn't seem to work -- the library just hard crashes with a segfault. Do you happen to have a working example?

segfault = Z.evalZ3 $ do

    i32sort <- Z.mkBvSort 32
    let mkV name = do sym <- Z.mkStringSymbol name
                      Z.mkVar sym i32sort

    c <- Z.mkBitvector 32 35
    x <- mkV "x"
    y <- mkV "y"

    -- Perform some operations on the values
    p  <- Z.mkBvmul x y
    e  <- Z.mkEq c p

    Z3.assert e

    one <- Z.mkBitvector 32 1
    Z.assert =<< Z.mkBvuge x one
    Z.assert =<< Z.mkBvuge y one


    z3result <- Z.solverCheckAndGetModel
    case z3result of
      (Z.Sat, Just model) -> do
        strModel <- Z.modelToString model
        liftIO $ putStrLn $ "MODEL = " ++ strModel -- THIS IS OKAY
        mx <- Z.evalBv True model x                -- THIS SEGFAULTS
        liftIO $ putStrLn $ show mx
      (r, _) -> liftIO $ putStrLn $ "FAIL: " ++ show r

Queens4.hs dies with "Z3.Base.toBool: illegal `Z3_bool' value" on OS X

There is a bug on OS X where Z3 uses values other than 1 to represent True when evaluating various terms.

Assuming you have nix installed, the following script reproduces the error on OS X.
The script is based on the Queens4.hs example.

#! /usr/bin/env nix-shell
#! nix-shell -p "haskell.packages.ghc843.ghcWithPackages (pkgs: [pkgs.z3])" -i "cabal exec -- runghc"

module Main where

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

import Z3.Monad

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

script :: Z3 (Maybe [Integer])
script = do
  q1 <- mkFreshIntVar "q1"
  q2 <- mkFreshIntVar "q2"
  q3 <- mkFreshIntVar "q3"
  q4 <- mkFreshIntVar "q4"
  _1 <- mkInteger 1
  _4 <- mkInteger 4
  -- the ith-queen is in the ith-row.
  -- qi is the column of the ith-queen
  assert =<< mkAnd =<< T.sequence
    [ mkLe _1 q1, mkLe q1 _4  -- 1 <= q1 <= 4
    , mkLe _1 q2, mkLe q2 _4
    , mkLe _1 q3, mkLe q3 _4
    , mkLe _1 q4, mkLe q4 _4
    ]
  -- different columns
  assert =<< mkDistinct [q1,q2,q3,q4]
  -- avoid diagonal attacks
  assert =<< mkNot =<< mkOr =<< T.sequence
    [ diagonal 1 q1 q2  -- diagonal line of attack between q1 and q2
    , diagonal 2 q1 q3
    , diagonal 3 q1 q4
    , diagonal 1 q2 q3
    , diagonal 2 q2 q4
    , diagonal 1 q3 q4
    ]
  -- check and get solution
  fmap snd $ withModel $ \m ->
    catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]
  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 d)

Program hangs when running evalZ3 or evalZ3WithEnv more than once

The script below should reproduce the issue, my Z3 version is 4.8.13 - 64 bit on linux. Also let me know if I've made some obvious mistakes, as this is the first time I'm using this package I won't be surprised if that's the case :)

The symptom is that the first testModel prints fairly fast, but the second ones hangs forever (or just taking very long),
and my CPU usage went up to 100% on all cores. What's interesting is that if you swap the order of two testModel calls,
now that the first one completes but it hangs on the second call. So I'm not convinced that model checking itself takes that long or is that CPU-intense.

Also note that in my actual project, I have the following extra-deps:

- git: https://github.com/IagoAbal/haskell-z3.git
  commit: ba5c2907c06a7844a78cf1fb87dae60f9b6ee6df

which experiences the same problem - so issue is still present on current HEAD.

(I could give some more details about what this model does, but I think it's irrelevant to the issue.)

#!/usr/bin/env stack
{- stack
  script
  --resolver lts-16.31
  --package z3
-}

{-# LANGUAGE BlockArguments #-}

import Control.Monad
import Control.Monad.IO.Class
import Z3.Monad

main :: IO ()
main = do
  env <- liftIO (newEnv (Just QF_NIA) stdOpts)
  let testModel x = print =<< checkSat env params (x : replicate 13 1) (replicate 14 9)
      params =
        [ (1, 11, 14)
        , (1, 14, 6)
        , (1, 15, 6)
        , (1, 13, 13)
        , (26, -12, 8)
        , (1, 10, 8)
        , (26, -15, 7)
        , (1, 13, 10)
        , (1, 10, 8)
        , (26, -13, 12)
        , (26, -13, 10)
        , (26, -14, 8)
        , (26, -2, 8)
        , (26, -9, 7)
        ]
  testModel 2
  testModel 5

checkSat :: Z3Env -> [(Int, Int, Int)] -> [Int] -> [Int] -> IO Bool
checkSat env zs lowDs highDs = do
  r <-
    evalZ3WithEnv
      (script zs lowDs highDs)
      env
  pure r

script :: [(Int, Int, Int)] -> [Int] -> [Int] -> Z3 Bool
script zs lowDs highDs = do
  wVars <- mapM (\i -> mkFreshIntVar ("w_" <> show i)) [0 :: Int .. 13]
  forM_ (zip [0 :: Int ..] (zip lowDs highDs)) \(i, (dLo, dHi)) -> do
    -- lo <= w_i
    le0 <- (\lo -> mkLe lo (wVars !! i)) =<< mkInteger (toInteger dLo)
    le1 <- (\hi -> mkLe (wVars !! i) hi) =<< mkInteger (toInteger dHi)
    assert =<< mkAnd [le0, le1]

  zVars <- mapM (\i -> mkFreshIntVar ("z_" <> show i)) [0 :: Int .. 14]
  assert =<< mkEq (zVars !! 0) =<< mkInteger 0
  assert =<< mkEq (zVars !! 14) =<< mkInteger 0

  let mkMystery zVar wVar (a, b, c) = do
        lit0 <- mkInteger 0
        lit1 <- mkInteger 1
        x0 <- do
          op0 <- mkMod zVar =<< mkInteger 26
          op1 <- mkInteger (toInteger b)
          mkAdd [op0, op1]
        x1 <- do
          t <- mkNot =<< mkEq x0 wVar
          mkIte t lit1 lit0
        z1 <- do
          t0 <- do
            t00 <-
              -- z0 `div` a
              mkDiv zVar =<< mkInteger (toInteger a)

            t01 <- do
              -- 25 * x1 + 1
              lit25 <- mkInteger 25
              t010 <- mkMul [lit25, x1]
              mkAdd [t010, lit1]
            mkMul [t00, t01]
          t1 <- do
            -- (w + c) * x1
            t10 <- do
              tc <- mkInteger (toInteger c)
              mkAdd [wVar, tc]
            mkMul [t10, x1]
          mkAdd [t0, t1]
        pure z1
  forM_ (zip [0 :: Int ..] zs) $ \(i, (a, b, c)) -> do
    lhs <- mkMystery (zVars !! i) (wVars !! i) (a, b, c)
    assert =<< mkEq lhs (zVars !! (i + 1))
  r <- check

  pure $ r == Sat