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.ii...@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.ii...@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 >> >> >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe