iagoabal / haskell-z3 Goto Github PK
View Code? Open in Web Editor NEWHaskell bindings to Microsoft's Z3 API (unofficial).
License: Other
Haskell bindings to Microsoft's Z3 API (unofficial).
License: Other
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?
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
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?
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?
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!
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
solverCheckAndGetModel segfaults on timeout. Might we worth only calling getModel when sat:
Unsat -> return Nothing
_ -> Just <$> solverGetModel ctx solver
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,
mk
.Z3
monad, so even if it's just building an AST, there must be <$>
and <*>
. sequence
s are spilled everywhere without clear motivation.mk
'd. This is an unnecessary burden.Int
in evalInt m
? The type seems to be deducible from the context.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.)
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
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.)
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
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 reset
ting the solver state instead? Most importantly, how can I measure this?
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.
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
The program prints:
Sat
b!1 -> true
a!0 -> true
This is what happens when Z3 4.8 is replaced with 4.4.
The program prints:
Sat
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).
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:
cabal install ...
or cabal v2-install ...
results in Cannot build .. z3 because none of the components are available to build:
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)
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)
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?
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
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.
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
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.
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:
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.
Accept Int
or Integral int
and handle under- and overflows by
fromIntegral
.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.
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 |
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
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:
Initialize a Solver
and Context
at the beginning of main
.
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.
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.
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:
assert
and isSat
calls, the rate of segfaults goes down to about 25%.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!
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:
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?
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
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
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.