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.
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.