[Haskell-cafe] Installing Z3 on OS X 10.8.4 ( Off topic )
mukesh tiwari
mukeshtiwari.iiitm at gmail.com
Mon Jul 1 12:12:43 CEST 2013
I also tried installing Yices[1] but still getting same error. I followed
the instructions but still the same error. Seems like I am missing some
crucial details about path but not able to resolve it.
Mukeshs-MacBook-Pro:SMT mukeshtiwari$ cd yices-2.1.0/
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE NOTICES README bin doc etc
examples include lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE NOTICES README bin doc etc
examples include lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cat README
Yices SMT Solver, Copyright SRI International, 2012
===================================================
This file is part of the Yices 2.0 binary distribution for MacOS X.
Yices is distributed free-of-charge for personal use under the terms
of the Yices license (see LICENSE).
Content
-------
This distribution includes three solvers
bin/yices (for the Yices 2 language)
bin/yices-smt (for SMT-LIB 1.2)
bin/yices-sat (sat solver, DIMACS format)
and the Yices libraries and header files
lib/libyices.2.0.0.dylib
include/yices.h
include/yices_types.h
include/yices_limits.h
include/yices_exit_codes.h
Examples and documentation are in the examples and doc directories.
The binaries and library were linked statically against GMP version 5.0.4,
copyright Free Software Foundation (see NOTICES).
Recommended Library Installation on MacOS X
-------------------------------------------
The library's install name is '/usr/local/lib/libyices.2.dylib' so
the following procedure should be used to install it.
1) copy libyices.2.0.0.dylib in /usr/local/lib (this requires
administrative privileges):
sudo cp libyices.2.0.0.dylib /usr/local/lib
sudo chmod 755 /usr/local/lib/libyices.2.0.0.dylib
2) add two symbolic links:
sudo ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.dylib
sudo ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.2.dylib
For more information, please visit http://yices.csl.sri.com.
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cd lib/
Mukeshs-MacBook-Pro:lib mukeshtiwari$ ls
libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo cp libyices.2.1.0.dylib
/usr/local/lib
Password:
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo chmod 755
/usr/local/lib/libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo ln -sf libyices.2.1.0.dylib
/usr/local/lib/libyices.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo ln -sf libyices.2.1.0.dylib
/usr/local/lib/libyices.2.dylib
Mukeshs-MacBook-Pro:~ mukeshtiwari$ ghci -XScopedTypeVariables
GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :m Data.SBV.Bridge.Yices
Prelude Data.SBV.Bridge.Yices> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package array-0.4.0.1 ... linking ... done.
Loading package deepseq-1.3.0.1 ... linking ... done.
Loading package filepath-1.3.0.1 ... linking ... done.
Loading package old-locale-1.0.0.5 ... linking ... done.
Loading package time-1.4.0.1 ... linking ... done.
Loading package bytestring-0.10.0.0 ... linking ... done.
Loading package unix-2.6.0.0 ... linking ... done.
Loading package directory-1.2.0.0 ... linking ... done.
Loading package process-1.1.0.2 ... linking ... done.
Loading package old-time-1.1.0.1 ... linking ... done.
Loading package containers-0.5.0.0 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
Loading package transformers-0.3.0.0 ... linking ... done.
Loading package mtl-2.1.2 ... linking ... done.
Loading package syb-0.3.7 ... linking ... done.
Loading package sbv-2.10 ... linking ... done.
*** An error occurred.
*** Unable to locate executable for Yices
*** Executable specified: "yices-smt"
Regards,
Mukesh Tiwari
[1] http://yices.csl.sri.com/download-yices2.shtml
On Mon, Jul 1, 2013 at 2:57 PM, mukesh tiwari
<mukeshtiwari.iiitm at gmail.com>wrote:
> Hello all,
> Not directly related to Haskell but I am trying to install Z3 to use SBV
> package[1]. I followed the instructions[2] to install it.
>
> *Mukeshs-MacBook-Pro:SMT mukeshtiwari$ git clone
> https://git01.codeplex.com/z3 -b unstable
> Cloning into 'z3'...
> remote: Counting objects: 16070, done.
> remote: Compressing objects: 100% (3928/3928), done.
> remote: Total 16070 (delta 12057), reused 16070 (delta 12057)
> Receiving objects: 100% (16070/16070), 7.62 MiB | 287 KiB/s, done.
> Resolving deltas: 100% (12057/12057), done.*
>
> After installing Z3
> *Running python example.py in z3/examples/python gives this result.
> *
> *Mukeshs-MacBook-Pro:python mukeshtiwari$ python example.py
> sat
> [y = 4, x = 2]*
>
> but when I am running sbv package, I am getting this error.
>
> *Mukeshs-MacBook-Pro:site-packages mukeshtiwari$ ghci
> -XScopedTypeVariables
> GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Prelude> :m Data.SBV.Bridge.Z3
> Prelude Data.SBV.Bridge.Z3> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
> Loading package pretty-1.1.1.0 ... linking ... done.
> Loading package array-0.4.0.1 ... linking ... done.
> Loading package deepseq-1.3.0.1 ... linking ... done.
> Loading package filepath-1.3.0.1 ... linking ... done.
> Loading package old-locale-1.0.0.5 ... linking ... done.
> Loading package time-1.4.0.1 ... linking ... done.
> Loading package bytestring-0.10.0.0 ... linking ... done.
> Loading package unix-2.6.0.0 ... linking ... done.
> Loading package directory-1.2.0.0 ... linking ... done.
> Loading package process-1.1.0.2 ... linking ... done.
> Loading package old-time-1.1.0.1 ... linking ... done.
> Loading package containers-0.5.0.0 ... linking ... done.
> Loading package random-1.0.1.1 ... linking ... done.
> Loading package template-haskell ... linking ... done.
> Loading package QuickCheck-2.5.1.1 ... linking ... done.
> Loading package transformers-0.3.0.0 ... linking ... done.
> Loading package mtl-2.1.2 ... linking ... done.
> Loading package syb-0.3.7 ... linking ... done.
> Loading package sbv-2.10 ... linking ... done.
> *** An error occurred.
> *** Unable to locate executable for z3
> *** Executable specified: "z3"
> Prelude Data.SBV.Bridge.Z3> *
>
> I have posted every details on installation on pastebin[3]. The
> documentation file says that[4] it will install
>
> *2) Building Z3 using make/g++ and Python
> Execute:
>
> autconf
> ./configure
> python scripts/mk_make.py
> cd build
> make
> sudo make install
>
> It will install z3 executable at /usr/bin, libraries at /usr/lib, and
> include files at /usr/include.*
>
> Mukeshs-MacBook-Pro:z3 mukeshtiwari$ echo $PATH
>
> /usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin:/Users/mukeshtiwari/.cabal/bin:/Users/mukeshtiwari/Erlang/bin:/Users/mukeshtiwari/Programming/Scala/scala-2.10.0/bin:/usr/local/smlnj-110.75/bin:/Users/mukeshtiwari/.rvm/bin
>
> Could some one please tell me how to solve this problem.
>
> Regards,
> Mukesh Tiwari
>
>
> [1] http://hackage.haskell.org/package/sbv
> [2]
> http://z3.codeplex.com/wikipage?title=Building%20the%20unstable%20%28working-in-progress%29%20branch&referringTitle=Documentation
> [3] http://pastebin.com/K5rq3jCF
> [4] http://z3.codeplex.com/SourceControl/latest#README
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130701/351c79ff/attachment.htm>
More information about the Haskell-Cafe
mailing list