<div dir="ltr">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. <br><div>
<br>Mukeshs-MacBook-Pro:SMT mukeshtiwari$ cd yices-2.1.0/<br>Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls<br>LICENSE NOTICES README bin doc etc examples include lib<br>
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls<br>LICENSE NOTICES README bin doc etc examples include lib<br>Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cat README <br>
Yices SMT Solver, Copyright SRI International, 2012<br>===================================================<br><br>This file is part of the Yices 2.0 binary distribution for MacOS X.<br>Yices is distributed free-of-charge for personal use under the terms<br>
of the Yices license (see LICENSE).<br><br><br>Content<br>-------<br><br>This distribution includes three solvers<br><br> bin/yices (for the Yices 2 language)<br> bin/yices-smt (for SMT-LIB 1.2)<br> bin/yices-sat (sat solver, DIMACS format)<br>
<br>and the Yices libraries and header files<br><br> lib/libyices.2.0.0.dylib<br> include/yices.h<br> include/yices_types.h<br> include/yices_limits.h<br> include/yices_exit_codes.h<br><br><br>Examples and documentation are in the examples and doc directories.<br>
<br><br>The binaries and library were linked statically against GMP version 5.0.4,<br>copyright Free Software Foundation (see NOTICES).<br><br><br><br>Recommended Library Installation on MacOS X<br>-------------------------------------------<br>
<br>The library's install name is '/usr/local/lib/libyices.2.dylib' so<br>the following procedure should be used to install it.<br><br>1) copy libyices.2.0.0.dylib in /usr/local/lib (this requires<br> administrative privileges):<br>
<br> sudo cp libyices.2.0.0.dylib /usr/local/lib<br> sudo chmod 755 /usr/local/lib/libyices.2.0.0.dylib<br><br><br>2) add two symbolic links:<br><br> sudo ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.dylib<br>
sudo ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.2.dylib<br><br><br><br><br>For more information, please visit <a href="http://yices.csl.sri.com">http://yices.csl.sri.com</a>.<br>Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cd lib/<br>
Mukeshs-MacBook-Pro:lib mukeshtiwari$ ls<br>libyices.2.1.0.dylib<br>Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo cp libyices.2.1.0.dylib /usr/local/lib<br>Password:<br>Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo chmod 755 /usr/local/lib/libyices.2.1.0.dylib<br>
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.dylib<br>Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.2.dylib<br><br>Mukeshs-MacBook-Pro:~ mukeshtiwari$ ghci -XScopedTypeVariables<br>
GHCi, version 7.6.1: <a href="http://www.haskell.org/ghc/">http://www.haskell.org/ghc/</a> :? for help<br>Loading package ghc-prim ... linking ... done.<br>Loading package integer-gmp ... linking ... done.<br>Loading package base ... linking ... done.<br>
Prelude> :m Data.SBV.Bridge.Yices <br>Prelude Data.SBV.Bridge.Yices> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x<br>Loading package pretty-1.1.1.0 ... linking ... done.<br>Loading package array-0.4.0.1 ... linking ... done.<br>
Loading package deepseq-1.3.0.1 ... linking ... done.<br>Loading package filepath-1.3.0.1 ... linking ... done.<br>Loading package old-locale-1.0.0.5 ... linking ... done.<br>Loading package time-1.4.0.1 ... linking ... done.<br>
Loading package bytestring-0.10.0.0 ... linking ... done.<br>Loading package unix-2.6.0.0 ... linking ... done.<br>Loading package directory-1.2.0.0 ... linking ... done.<br>Loading package process-1.1.0.2 ... linking ... done.<br>
Loading package old-time-1.1.0.1 ... linking ... done.<br>Loading package containers-0.5.0.0 ... linking ... done.<br>Loading package random-1.0.1.1 ... linking ... done.<br>Loading package template-haskell ... linking ... done.<br>
Loading package QuickCheck-2.5.1.1 ... linking ... done.<br>Loading package transformers-0.3.0.0 ... linking ... done.<br>Loading package mtl-2.1.2 ... linking ... done.<br>Loading package syb-0.3.7 ... linking ... done.<br>
Loading package sbv-2.10 ... linking ... done.<br>*** An error occurred.<br>*** Unable to locate executable for Yices<br>*** Executable specified: "yices-smt"<br><br><br>Regards,<br>Mukesh Tiwari<br><br>[1] <a href="http://yices.csl.sri.com/download-yices2.shtml">http://yices.csl.sri.com/download-yices2.shtml</a><br>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jul 1, 2013 at 2:57 PM, mukesh tiwari <span dir="ltr"><<a href="mailto:mukeshtiwari.iiitm@gmail.com" target="_blank">mukeshtiwari.iiitm@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello all, <br>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.<br>
<br><i>Mukeshs-MacBook-Pro:SMT mukeshtiwari$ git clone <a href="https://git01.codeplex.com/z3" target="_blank">https://git01.codeplex.com/z3</a> -b unstable<br>
Cloning into 'z3'...<br>remote: Counting objects: 16070, done.<br>remote: Compressing objects: 100% (3928/3928), done.<br>remote: Total 16070 (delta 12057), reused 16070 (delta 12057)<br>Receiving objects: 100% (16070/16070), 7.62 MiB | 287 KiB/s, done.<br>
Resolving deltas: 100% (12057/12057), done.</i><br><br></div><div>After installing Z3<br></div><div><i>Running python example.py in z3/examples/python gives this result.<br></i></div><div><i>Mukeshs-MacBook-Pro:python mukeshtiwari$ python example.py <br>
sat<br>[y = 4, x = 2]</i><br></div><div><br></div><div>but when I am running sbv package, I am getting this error.<br><br><i>Mukeshs-MacBook-Pro:site-packages mukeshtiwari$ ghci -XScopedTypeVariables<br>GHCi, version 7.6.1: <a href="http://www.haskell.org/ghc/" target="_blank">http://www.haskell.org/ghc/</a> :? for help<br>
Loading package ghc-prim ... linking ... done.<br>Loading package integer-gmp ... linking ... done.<br>Loading package base ... linking ... done.<br>Prelude> :m Data.SBV.Bridge.Z3 <br>Prelude Data.SBV.Bridge.Z3> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x<br>
Loading package pretty-1.1.1.0 ... linking ... done.<br>Loading package array-0.4.0.1 ... linking ... done.<br>Loading package deepseq-1.3.0.1 ... linking ... done.<br>Loading package filepath-1.3.0.1 ... linking ... done.<br>
Loading package old-locale-1.0.0.5 ... linking ... done.<br>Loading package time-1.4.0.1 ... linking ... done.<br>Loading package bytestring-0.10.0.0 ... linking ... done.<br>Loading package unix-2.6.0.0 ... linking ... done.<br>
Loading package directory-1.2.0.0 ... linking ... done.<br>Loading package process-1.1.0.2 ... linking ... done.<br>Loading package old-time-1.1.0.1 ... linking ... done.<br>Loading package containers-0.5.0.0 ... linking ... done.<br>
Loading package random-1.0.1.1 ... linking ... done.<br>Loading package template-haskell ... linking ... done.<br>Loading package QuickCheck-2.5.1.1 ... linking ... done.<br>Loading package transformers-0.3.0.0 ... linking ... done.<br>
Loading package mtl-2.1.2 ... linking ... done.<br>Loading package syb-0.3.7 ... linking ... done.<br>Loading package sbv-2.10 ... linking ... done.<br>*** An error occurred.<br>*** Unable to locate executable for z3<br>
*** Executable specified: "z3"<br>Prelude Data.SBV.Bridge.Z3> </i><br><br></div><div>I have posted every details on installation on pastebin[3]. The documentation file says that[4] it will install <br><br><i><span>2) Building Z3 using make/g++ and Python<br>
Execute:<br><br> autconf<br> ./configure<br> python scripts/mk_make.py<br> cd build<br> make<br> sudo make install<br><br>It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include.</span></i><br>
<br>Mukeshs-MacBook-Pro:z3 mukeshtiwari$ echo $PATH<br>/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<br>
<br></div><div>Could some one please tell me how to solve this problem. <br><br></div><div>Regards,<br></div><div>Mukesh Tiwari<br><br></div><div><br>[1] <a href="http://hackage.haskell.org/package/sbv" target="_blank">http://hackage.haskell.org/package/sbv</a><br>
[2] <a href="http://z3.codeplex.com/wikipage?title=Building%20the%20unstable%20%28working-in-progress%29%20branch&referringTitle=Documentation" target="_blank">http://z3.codeplex.com/wikipage?title=Building%20the%20unstable%20%28working-in-progress%29%20branch&referringTitle=Documentation</a><br>
[3] <a href="http://pastebin.com/K5rq3jCF" target="_blank">http://pastebin.com/K5rq3jCF</a><br>[4] <a href="http://z3.codeplex.com/SourceControl/latest#README" target="_blank">http://z3.codeplex.com/SourceControl/latest#README</a><br>
<br></div></div>
</blockquote></div><br></div>