[Haskell-cafe] Installing Z3 on OS X 10.8.4 ( Off topic )
mukesh tiwari
mukeshtiwari.iiitm at gmail.com
Mon Jul 1 12:47:04 CEST 2013
Finally I got the Yices working by adding yices-2.1.0/bin to my path. Still
looking to resolve Z3.
Regards,
Mukesh Tiwari
On Mon, Jul 1, 2013 at 3:42 PM, mukesh tiwari
<mukeshtiwari.iiitm at gmail.com>wrote:
> 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/497f42a2/attachment.htm>
More information about the Haskell-Cafe
mailing list