Search code examples
z3

avoid using sudo to use z3++.h as a lib


I am using the z3prover first time, after reading most of related answers, I have noticed that I need to try: sudo make install .How could I skip the link z3 in /usr/bin and /usr/lib to use z3++.h in my own c++ project. (bcs I have noticed not everyone has the sudoer, I hope my code would goes well without sudoer.


Solution

  • You do need to compile the z3 source code if you want to be able to use it in your C/C++ projects. Compiling it will give you the library to link against. If you just download the source code, you can find the headers but you cannot link and hence cannot create your own executables.

    But doing so does not require sudo access at all. The proper way to do so is actually explained in the https://github.com/Z3Prover/z3 page, right in the README. Roughly, they go like this:

    python scripts/mk_make.py --prefix=/home/leo
    cd build
    make
    make install
    

    Note in the prefix parameter of the first line you tell z3 where to install everything. Change that path to a place where you have write-access. This way you do not need sudo access.

    In order to compile your project successfully, you need to tell your compiler where to look for dynamic libraries and header files. Ask separately if you run into issues.